diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 21:48:42 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 21:48:42 +0000 |
| commit | 1f8c6509afb1d7d99f2e4c0ef2df91b25be31bec (patch) | |
| tree | dd2f81ff963ed8ccdf70d27ba68aaf8e1a939444 /src/theory/arith/theory_arith.cpp | |
| parent | dcb2ad496607e2f3821ee84a175a1b412f2f9a20 (diff) | |
tim's fixes for context-dependent pre-registration
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
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); |