diff options
| -rw-r--r-- | src/theory/arith/atom_database.h | 7 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 |
2 files changed, 5 insertions, 6 deletions
diff --git a/src/theory/arith/atom_database.h b/src/theory/arith/atom_database.h index af7068ada..4da8d7975 100644 --- a/src/theory/arith/atom_database.h +++ b/src/theory/arith/atom_database.h @@ -96,9 +96,11 @@ public: bool containsLeq(TNode atom) const; bool containsGeq(TNode atom) const; - + /** Check to make sure an lhs has been properly set-up. */ + bool leftIsSetup(TNode left) const; private: + VariablesSets& getVariablesSets(TNode left); BoundValueSet& getBoundValueSet(TNode left); EqualValueSet& getEqualValueSet(TNode left); @@ -110,9 +112,6 @@ private: /** Sends an implication (=> a b) to the PropEngine via d_arithOut. */ void addImplication(TNode a, TNode b); - /** Check to make sure an lhs has been properly set-up. */ - bool leftIsSetup(TNode left) const; - /** Initializes the lists associated with a unique lhs. */ void setupLefthand(TNode left); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1b13b9ee6..be8feb245 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -286,13 +286,13 @@ void TheoryArith::preRegisterTerm(TNode n) { d_out->setIncomplete(); } - if(Variable::isMember(n) || isStrictlyVarList){ + if((Variable::isMember(n) || isStrictlyVarList) && !d_arithvarNodeMap.hasArithVar(n)){ ++(d_statistics.d_statUserVariables); ArithVar varN = requestArithVar(n,false); setupInitialValue(varN); } - if(isRelationOperator(k)){ + if(isRelationOperator(k) && (!d_atomDatabase.leftIsSetup(n[0]) || !d_atomDatabase.containsAtom(n))) { Assert(Comparison::isNormalAtom(n)); d_atomDatabase.addAtom(n); |