diff options
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 12 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/bug449.smt | 11 |
3 files changed, 24 insertions, 0 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1d89c02d4..74e0ad296 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -674,6 +674,10 @@ bool TheoryArith::AssertDisequality(Constraint constraint){ void TheoryArith::addSharedTerm(TNode n){ Debug("arith::addSharedTerm") << "addSharedTerm: " << n << endl; + if(n.isConst()){ + d_partialModel.invalidateDelta(); + } + d_congruenceManager.addSharedTerm(n); if(!n.isConst() && !isSetup(n)){ Polynomial poly = Polynomial::parsePolynomial(n); @@ -2102,6 +2106,14 @@ Rational TheoryArith::deltaValueForTotalOrder() const{ relevantDeltaValues.insert(rhsValue); } + for(shared_terms_iterator shared_iter = shared_terms_begin(), + shared_end = shared_terms_end(); shared_iter != shared_end; ++shared_iter){ + Node sharedCurr = *shared_iter; + if(sharedCurr.getKind() == CONST_RATIONAL){ + relevantDeltaValues.insert(sharedCurr.getConst<Rational>());: + } + } + for(ArithVar v = 0; v < d_variables.size(); ++v){ const DeltaRational& value = d_partialModel.getAssignment(v); relevantDeltaValues.insert(value); diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 86a1a9431..352161466 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -23,6 +23,7 @@ SMT_TESTS = \ simple.03.cvc \ simple.04.cvc \ bug293.cvc \ + bug449.smt \ pb_real_10_0100_10_10.smt \ pb_real_10_0100_10_11.smt \ pb_real_10_0100_10_15.smt \ diff --git a/test/regress/regress0/uflra/bug449.smt b/test/regress/regress0/uflra/bug449.smt new file mode 100644 index 000000000..91bb5fb48 --- /dev/null +++ b/test/regress/regress0/uflra/bug449.smt @@ -0,0 +1,11 @@ +(benchmark fuzzsmt +:logic QF_UFLRA +:extrapreds ((p0 Real)) +:extrafuns ((v0 Real)) +:status sat +:formula +(and + (p0 v0) + (< v0 0) + (not (p0 (- 1))) +)) |