Fix to bug449. Adds shared constants to the set of DeltaRationals that must be in...

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 1d89c02d4f4230ba5904246b83e895ed10992043..74e0ad2963e8ab86e2ff2b492908ee0ee6c54ff7 100644 (file)
--- 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 86a1a943134d6858fe9c3031ee8c063a5a4031ce..352161466783a0c71401622b0394311c2dc9b763 100644 (file)
--- 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 (file)
index 0000000..91bb5fb
--- /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)))
+))