From aa4b06d4f1db1942d7ad3833e071baa356cefd60 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 14 Nov 2012 22:43:57 +0000
Subject: [PATCH] Fix to bug449. Adds shared constants to the set of
 DeltaRationals that must be in the final total order.

---
 src/theory/arith/theory_arith.cpp       | 12 ++++++++++++
 test/regress/regress0/uflra/Makefile.am |  1 +
 test/regress/regress0/uflra/bug449.smt  | 11 +++++++++++
 3 files changed, 24 insertions(+)
 create mode 100644 test/regress/regress0/uflra/bug449.smt

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)))
+))
-- 
2.30.2