Fixes 2 issues with assignments. The first is constructing an initial assignment for slack variables once solving has begun. (They cannot just be 0.) The second has to do with how assignments are backttacked. Assignments are now tracked all of the time, and are frozen once they are known to be consistent, i.e. after a successful updateInconsistentVars(). Also added a fuzz test that shows both of these problems to the regressions.

6 files changed, 302 insertions, 76 deletions

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 4b113257c..33c690276 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -27,21 +27,28 @@ void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){
   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
   if(d_savingAssignments){
-    d_history.push_back(make_pair(x,r));
+    DeltaRational current = getAssignment(x);
+    d_history.push_back(make_pair(x,current));
   }
 
-  DeltaRational* c;
-  if(x.getAttribute(partial_model::Assignment(), c)){
-    *c = r;
-    Debug("partial_model") << "pm: updating the assignment to" << x
-                           << " now " << r <<endl;
-  }else{
-    Debug("partial_model") << "pm: constructing an assignment for " << x
-                           << " initially " << r <<endl;
+  Assert(x.hasAttribute(partial_model::Assignment()));
 
-    c = new DeltaRational(r);
-    x.setAttribute(partial_model::Assignment(), c);
-  }
+  DeltaRational* c = x.getAttribute(partial_model::Assignment());
+  *c = r;
+  Debug("partial_model") << "pm: updating the assignment to" << x
+                         << " now " << r <<endl;
+}
+
+void ArithPartialModel::initialize(TNode x, const DeltaRational& r){
+   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+
+   Assert(!x.hasAttribute(partial_model::Assignment()));
+   DeltaRational* c = new DeltaRational(r);
+   x.setAttribute(partial_model::Assignment(), c);
+
+   Debug("partial_model") << "pm: constructing an assignment for " << x
+                          << " initially " << (*c) <<endl;
 }
 
 /** Must know that the bound exists both calling this! */
@@ -72,6 +79,19 @@ DeltaRational ArithPartialModel::getAssignment(TNode x) const{
   return *assign;
 }
 
+DeltaRational ArithPartialModel::getSavedAssignment(TNode x) const{
+  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+  if(d_savingAssignments){
+    for(HistoryStack::const_iterator i = d_history.begin(); i != d_history.end(); ++i){
+      pair<TNode, DeltaRational> curr = *i;
+      if(curr.first == x){
+        return DeltaRational(curr.second);
+      }
+    }
+  }
+  return getAssignment(x);
+}
+
 
 void ArithPartialModel::setLowerConstraint(TNode x, TNode constraint){
   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 01db59855..57996a510 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -115,7 +115,7 @@ public:
 
   /* */
   void stopRecordingAssignments(bool revert);
-
+  bool isRecording() { return d_savingAssignments;  }
 
   void setUpperBound(TNode x, const DeltaRational& r);
   void setLowerBound(TNode x, const DeltaRational& r);
@@ -144,6 +144,11 @@ public:
   bool assignmentIsConsistent(TNode x);
 
   void printModel(TNode x);
+
+  void initialize(TNode x, const DeltaRational& r);
+  
+  DeltaRational getSavedAssignment(TNode x) const;
+
 };
 
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 1dbf818b3..3ca3245dd 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -43,6 +43,8 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
 {
   uint64_t ass_id = partial_model::Assignment::getId();
   Debug("arithsetup") << "Assignment: " << ass_id << std::endl;
+
+  d_partialModel.beginRecordingAssignments();
 }
 TheoryArith::~TheoryArith(){
   for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){
@@ -66,11 +68,17 @@ void TheoryArith::preRegisterTerm(TNode n) {
 
       d_splits.push_back(eagerSplit);
 
+
       n.setAttribute(EagerlySplitUpon(), true);
       d_out->augmentingLemma(eagerSplit);
     }
   }
 
+  if(n.getMetaKind() == metakind::VARIABLE){
+
+    setupVariable(n);
+  }
+
   Debug("arith_preregister") << "arith: end TheoryArith::preRegisterTerm("
                              << n << ")" << endl;
 }
@@ -90,18 +98,6 @@ bool isBasicSum(TNode n){
   return true;
 }
 
-Kind multKind(Kind k){
-  switch(k){
-  case LT: return GT;
-  case LEQ: return GEQ;
-  case EQUAL: return EQUAL;
-  case GEQ: return LEQ;
-  case GT: return LT;
-  default:
-    Unhandled();
-  }
-  return NULL_EXPR;
-}
 
 
 void registerAtom(TNode rel){
@@ -110,6 +106,72 @@ void registerAtom(TNode rel){
 
 }
 
+/* Requirements:
+ * Variable must have been set to be basic.
+ * For basic variables the row must have been added to the tableau.
+ */
+void TheoryArith::setupVariable(TNode x){
+  Assert(x.getMetaKind() == kind::metakind::VARIABLE);
+  d_variables.push_back(Node(x));
+
+  if(!isBasic(x)){
+    d_partialModel.initialize(x,d_constants.d_ZERO_DELTA);
+  }else{
+    //If the variable is basic, assertions may have already happened and updates
+    //may have occured before setting this variable up.
+
+    //This can go away if the tableau creation is done at preregister
+    //time instead of register
+
+    DeltaRational q = computeRowValueUsingSavedAssignment(x);
+    if(!(q == d_constants.d_ZERO_DELTA)){
+      Debug("arith_setup") << "setup("<<x<< " " <<q<<")"<<std::endl;
+    }
+    d_partialModel.initialize(x,q);
+
+    q = computeRowValueUsingAssignment(x);
+    if(!(q == d_constants.d_ZERO_DELTA)){
+      Debug("arith_setup") << "setup("<<x<< " " <<q<<")"<<std::endl;
+    }
+    d_partialModel.setAssignment(x,q);
+  }
+  Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
+};
+
+/**
+ * Computes the value of a basic variable using the current assignment.
+ */
+DeltaRational TheoryArith::computeRowValueUsingAssignment(TNode x){
+  Assert(isBasic(x));
+  DeltaRational sum = d_constants.d_ZERO_DELTA;
+
+  Row* row = d_tableau.lookup(x);
+  for(std::set<TNode>::iterator i = row->begin(); i != row->end();++i){
+    TNode nonbasic = *i;
+    Rational& coeff = row->lookup(nonbasic);
+    DeltaRational assignment = d_partialModel.getAssignment(nonbasic);
+    sum = sum + (assignment * coeff);
+  }
+  return sum;
+}
+
+/**
+ * Computes the value of a basic variable using the current assignment.
+ */
+DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){
+  Assert(isBasic(x));
+  DeltaRational sum = d_constants.d_ZERO_DELTA;
+
+  Row* row = d_tableau.lookup(x);
+  for(std::set<TNode>::iterator i = row->begin(); i != row->end();++i){
+    TNode nonbasic = *i;
+    Rational& coeff = row->lookup(nonbasic);
+    DeltaRational assignment = d_partialModel.getSavedAssignment(nonbasic);
+    sum = sum + (assignment * coeff);
+  }
+  return sum;
+}
+
 Node TheoryArith::rewrite(TNode n){
   Debug("arith") << "rewrite(" << n << ")" << endl;
 
@@ -126,10 +188,6 @@ void TheoryArith::registerTerm(TNode tn){
 
   if(tn.getKind() == kind::BUILTIN) return;
 
-  if(tn.getMetaKind() == metakind::VARIABLE){
-
-    setupVariable(tn);
-  }
 
   //TODO is an atom
   if(isRelationOperator(tn.getKind())){
@@ -152,11 +210,11 @@ void TheoryArith::registerTerm(TNode tn){
           TypeNode real_type = NodeManager::currentNM()->realType();
           slack = NodeManager::currentNM()->mkVar(real_type);
 
-          setupVariable(slack);
-
           left.setAttribute(Slack(), slack);
           makeBasic(slack);
 
+
+
           Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left);
           slackEqLeft.setAttribute(TheoryArithPropagated(), true);
           //TODO this has to be wrong no? YES (dejan)
@@ -166,6 +224,8 @@ void TheoryArith::registerTerm(TNode tn){
 
           d_tableau.addRow(slackEqLeft);
 
+          setupVariable(slack);
+
           Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right);
           registerAtom(rewritten);
         }else{
@@ -182,7 +242,7 @@ void TheoryArith::registerTerm(TNode tn){
 }
 
 /* procedure AssertUpper( x_i <= c_i) */
-void TheoryArith::AssertUpper(TNode n, TNode original){
+bool TheoryArith::AssertUpper(TNode n, TNode original){
   TNode x_i = n[0];
   Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
   DeltaRational c_i(n[1].getConst<Rational>(), dcoeff);
@@ -192,12 +252,14 @@ void TheoryArith::AssertUpper(TNode n, TNode original){
 
 
   if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){
-    return; //sat
+    return false; //sat
   }
   if(d_partialModel.belowLowerBound(x_i, c_i, true)){
-    Node conflict =  NodeManager::currentNM()->mkNode(AND, d_partialModel.getLowerConstraint(x_i), original);
+    Node lbc = d_partialModel.getLowerConstraint(x_i);
+    Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
+    Debug("arith") << "AssertUpper conflict " << conflict << endl;
     d_out->conflict(conflict);
-    return;
+    return true;
   }
 
   d_partialModel.setUpperConstraint(x_i,original);
@@ -208,10 +270,12 @@ void TheoryArith::AssertUpper(TNode n, TNode original){
       update(x_i, c_i);
     }
   }
+  d_partialModel.printModel(x_i);
+  return false;
 }
 
 /* procedure AssertLower( x_i >= c_i ) */
-void TheoryArith::AssertLower(TNode n, TNode orig){
+bool TheoryArith::AssertLower(TNode n, TNode original){
   TNode x_i = n[0];
   Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
   DeltaRational c_i(n[1].getConst<Rational>(),dcoeff);
@@ -219,15 +283,17 @@ void TheoryArith::AssertLower(TNode n, TNode orig){
   Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
 
   if(d_partialModel.belowLowerBound(x_i, c_i, false)){
-    return; //sat
+    return false; //sat
   }
   if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
-    Node conflict =  NodeManager::currentNM()->mkNode(AND, d_partialModel.getUpperConstraint(x_i), orig);
+    Node ubc = d_partialModel.getUpperConstraint(x_i);
+    Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
     d_out->conflict(conflict);
-    return;
+    Debug("arith") << "AssertLower conflict " << conflict << endl;
+    return true;
   }
 
-  d_partialModel.setLowerConstraint(x_i,orig);
+  d_partialModel.setLowerConstraint(x_i,original);
   d_partialModel.setLowerBound(x_i, c_i);
 
   if(!isBasic(x_i)){
@@ -235,6 +301,9 @@ void TheoryArith::AssertLower(TNode n, TNode orig){
       update(x_i, c_i);
     }
   }
+  //d_partialModel.printModel(x_i);
+
+  return false;
 }
 
 void TheoryArith::update(TNode x_i, DeltaRational& v){
@@ -261,9 +330,15 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
   }
 
   d_partialModel.setAssignment(x_i, v);
+
+  if(debugTagIsOn("paranoid:check_tableau")){
+    checkTableau();
+  }
 }
 
 void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
+  Assert(x_i != x_j);
+
   Row* row_i = d_tableau.lookup(x_i);
   Rational& a_ij = row_i->lookup(x_j);
 
@@ -293,7 +368,10 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
   }
 
   d_tableau.pivot(x_i, x_j);
-  d_tableau.printTableau();
+
+  if(debugTagIsOn("tableau")){
+    d_tableau.printTableau();
+  }
 }
 
 TNode TheoryArith::selectSmallestInconsistentVar(){
@@ -352,13 +430,30 @@ TNode TheoryArith::selectSlackAbove(TNode x_i){ // beta(x_i) > u_i
 Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
   Debug("arith") << "updateInconsistentVars" << endl;
 
-  d_partialModel.beginRecordingAssignments();
+
   while(true){
+    if(debugTagIsOn("paranoid:check_tableau")){
+      checkTableau();
+    }
+
     TNode x_i = selectSmallestInconsistentVar();
     Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
     if(x_i == Node::null()){
       Debug("arith_update") << "No inconsistent variables" << endl;
+
+      if(debugTagIsOn("paranoid:check_tableau")){
+        checkTableau();
+      }
+
       d_partialModel.stopRecordingAssignments(false);
+      d_partialModel.beginRecordingAssignments();
+
+      if(debugTagIsOn("paranoid:check_tableau")){
+        checkTableau();
+      }
+
+
+
       return Node::null(); //sat
     }
     DeltaRational beta_i = d_partialModel.getAssignment(x_i);
@@ -367,21 +462,41 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
       DeltaRational l_i = d_partialModel.getLowerBound(x_i);
       TNode x_j = selectSlackBelow(x_i);
       if(x_j == TNode::null() ){
+        Debug("arith_update") << "conflict below" << endl;
+
+        if(debugTagIsOn("paranoid:check_tableau")){
+          checkTableau();
+        }
+
         d_partialModel.stopRecordingAssignments(true);
+        d_partialModel.beginRecordingAssignments();
+
+        if(debugTagIsOn("paranoid:check_tableau")){
+          checkTableau();
+        }
+
         return generateConflictBelow(x_i); //unsat
       }
-      d_partialModel.printModel(x_i);
-      d_partialModel.printModel(x_j);
       pivotAndUpdate(x_i, x_j, l_i);
+
     }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
       DeltaRational u_i = d_partialModel.getUpperBound(x_i);
       TNode x_j = selectSlackAbove(x_i);
       if(x_j == TNode::null() ){
+        Debug("arith_update") << "conflict above" << endl;
+
+        if(debugTagIsOn("paranoid:check_tableau")){
+          checkTableau();
+        }
+
         d_partialModel.stopRecordingAssignments(true);
+        d_partialModel.beginRecordingAssignments();
+
+        if(debugTagIsOn("paranoid:check_tableau")){
+          checkTableau();
+        }
         return generateConflictAbove(x_i); //unsat
       }
-      d_partialModel.printModel(x_i);
-      d_partialModel.printModel(x_j);
       pivotAndUpdate(x_i, x_j, u_i);
     }
   }
@@ -395,6 +510,7 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){
 
   Debug("arith")  << "generateConflictAbove "
                   << "conflictVar " << conflictVar
+                  << " " << d_partialModel.getAssignment(conflictVar)
                   << " " << bound << endl;
 
   nb << bound;
@@ -409,11 +525,13 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){
 
     if(a_ij < d_constants.d_ZERO){
       bound =  d_partialModel.getUpperConstraint(nonbasic);
-      Debug("arith") << "below 0 "<< nonbasic << " " << bound << endl;
+      Debug("arith") << "below 0 " << nonbasic << " "
+                     << d_partialModel.getAssignment(nonbasic) << " " << bound << endl;
       nb << bound;
     }else{
       bound =  d_partialModel.getLowerConstraint(nonbasic);
-      Debug("arith") << " above 0 "<< nonbasic << " " << bound << endl;
+      Debug("arith") << " above 0 " << nonbasic << " "
+                     << d_partialModel.getAssignment(nonbasic) << " " << bound << endl;
       nb << bound;
     }
   }
@@ -429,6 +547,7 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){
 
   Debug("arith") << "generateConflictBelow "
                  << "conflictVar " << conflictVar
+                 << d_partialModel.getAssignment(conflictVar) << " "
                  << " " << bound << endl;
   nb << bound;
 
@@ -442,12 +561,14 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){
 
     if(a_ij < d_constants.d_ZERO){
       TNode bound = d_partialModel.getLowerConstraint(nonbasic);
-      Debug("arith") << "Lower "<< nonbasic << " " << bound << endl;
+      Debug("arith") << "Lower "<< nonbasic << " "
+                     << d_partialModel.getAssignment(nonbasic) << " "<< bound << endl;
 
       nb << bound;
     }else{
       TNode bound = d_partialModel.getUpperConstraint(nonbasic);
-      Debug("arith") << "Upper "<< nonbasic << " " << bound << endl;
+      Debug("arith") << "Upper "<< nonbasic << " "
+                     << d_partialModel.getAssignment(nonbasic) << " "<< bound << endl;
 
       nb << bound;
     }
@@ -503,11 +624,14 @@ Node TheoryArith::simulatePreprocessing(TNode n){
 void TheoryArith::check(Effort level){
   Debug("arith") << "TheoryArith::check begun" << std::endl;
 
+  bool conflictDuringAnAssert = false;
+
   while(!done()){
+    //checkTableau();
     Node original = get();
     Node assertion = simulatePreprocessing(original);
     Debug("arith_assertions") << "arith assertion(" << original
-                   << " \\-> " << assertion << ")" << std::endl;
+                              << " \\-> " << assertion << ")" << std::endl;
 
     d_preprocessed.push_back(assertion);
 
@@ -516,14 +640,14 @@ void TheoryArith::check(Effort level){
       Warning() << "No bools should be reached dagnabbit" << endl;
       break;
     case LEQ:
-      AssertUpper(assertion, original);
+      conflictDuringAnAssert = AssertUpper(assertion, original);
       break;
     case GEQ:
-      AssertLower(assertion, original);
+      conflictDuringAnAssert = AssertLower(assertion, original);
       break;
     case EQUAL:
-      AssertUpper(assertion, original);
-      AssertLower(assertion, original);
+      conflictDuringAnAssert = AssertUpper(assertion, original);
+      conflictDuringAnAssert |= AssertLower(assertion, original);
       break;
     case NOT:
       {
@@ -532,13 +656,13 @@ void TheoryArith::check(Effort level){
         case LEQ: //(not (LEQ x c)) <=> (GT x c)
           {
             Node pushedin = pushInNegation(assertion);
-            AssertLower(pushedin,original);
+            conflictDuringAnAssert = AssertLower(pushedin,original);
             break;
           }
         case GEQ: //(not (GEQ x c) <=> (LT x c)
           {
             Node pushedin = pushInNegation(assertion);
-            AssertUpper(pushedin,original);
+            conflictDuringAnAssert = AssertUpper(pushedin,original);
             break;
           }
         case EQUAL:
@@ -556,11 +680,20 @@ void TheoryArith::check(Effort level){
       Unhandled();
     }
   }
+  if(conflictDuringAnAssert){
+    //clear the queue;
+    while(!done()) {
+      get();
+    }
+    //return
+    return;
+  }
 
   if(fullEffort(level)){
     Node possibleConflict = updateInconsistentVars();
     if(possibleConflict != Node::null()){
-      Debug("arith_conflict") << "Found a conflict " << possibleConflict << endl;
+      Debug("arith_conflict") << "Found a conflict "
+                              << possibleConflict << endl;
       d_out->conflict(possibleConflict);
     }else{
       Debug("arith_conflict") << "No conflict found" << endl;
@@ -598,15 +731,38 @@ void TheoryArith::check(Effort level){
       //Warning() << "Outstanding case split in theory arith" << endl;
     }
   }
-  if(debugTagIsOn("model")){
-    for(vector<Node>::iterator i=d_variables.begin();
-        i!= d_variables.end();
-        ++i){
-      Node var = *i;
-      d_partialModel.printModel(var);
-    }
-  }
 
   Debug("arith") << "TheoryArith::check end" << std::endl;
 
 }
+
+/**
+ * This check is quite expensive.
+ * It should be wrapped in a debugTagIsOn guard.
+ *   if(debugTagIsOn("paranoid:check_tableau")){
+ *      checkTableau();
+ *   }
+ */
+void TheoryArith::checkTableau(){
+
+  for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+      basicIter != d_tableau.end(); ++basicIter){
+    TNode basic = *basicIter;
+    Row* row_k = d_tableau.lookup(basic);
+    DeltaRational sum;
+    Debug("paranoid:check_tableau") << "starting row" << basic << endl;
+    for(std::set<TNode>::iterator nonbasicIter = row_k->begin();
+        nonbasicIter != row_k->end();
+        ++nonbasicIter){
+      TNode nonbasic = *nonbasicIter;
+      Rational& coeff = row_k->lookup(nonbasic);
+      DeltaRational beta = d_partialModel.getAssignment(nonbasic);
+      Debug("paranoid:check_tableau") << nonbasic << beta << coeff<<endl;
+      sum = sum + (beta*coeff);
+    }
+    DeltaRational shouldBe = d_partialModel.getAssignment(basic);
+    Debug("paranoid:check_tableau") << "ending row" << sum << "," << shouldBe << endl;
+
+    Assert(sum == shouldBe);
+  }
+}
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 1d6cca5cc..ade63b6c9 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -76,8 +76,8 @@ public:
   void explain(TNode n, Effort e) { Unimplemented(); }
 
 private:
-  void AssertLower(TNode n, TNode orig);
-  void AssertUpper(TNode n, TNode orig);
+  bool AssertLower(TNode n, TNode orig);
+  bool AssertUpper(TNode n, TNode orig);
   void update(TNode x_i, DeltaRational& v);
   void pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v);
 
@@ -90,15 +90,13 @@ private:
   Node generateConflictAbove(TNode conflictVar);
   Node generateConflictBelow(TNode conflictVar);
 
+  void setupVariable(TNode x);
+  DeltaRational computeRowValueUsingAssignment(TNode x);
+  DeltaRational computeRowValueUsingSavedAssignment(TNode x);
+  void checkTableau();
+
   //TODO get rid of this!
   Node simulatePreprocessing(TNode n);
-  void setupVariable(TNode x){
-    Assert(x.getMetaKind() == kind::metakind::VARIABLE);
-    d_partialModel.setAssignment(x,d_constants.d_ZERO_DELTA);
-    d_variables.push_back(Node(x));
-
-    Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
-  };
 
 };
 
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 515d496f5..0b8a60495 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -55,7 +55,8 @@ TESTS =	\
 	wiki.18.cvc \
 	wiki.19.cvc \
 	wiki.20.cvc \
-	wiki.21.cvc
+	wiki.21.cvc \
+	fuzz_3.smt
 
 if CVC4_BUILD_PROFILE_COMPETITION
 else
diff --git a/test/regress/regress0/fuzz_3.smt b/test/regress/regress0/fuzz_3.smt
new file mode 100644
index 000000000..e1c53d2c3
--- /dev/null
+++ b/test/regress/regress0/fuzz_3.smt
@@ -0,0 +1,46 @@
+(benchmark fuzzsmt
+:logic QF_LRA
+:extrafuns ((v0 Real))
+:extrafuns ((v2 Real))
+:extrafuns ((v1 Real))
+:status sat
+:formula
+(let (?n1 2)
+(let (?n2 (* ?n1 ?n1))
+(let (?n3 (~ v0))
+(let (?n4 (* ?n1 ?n3))
+(let (?n5 (- ?n1 ?n1))
+(let (?n6 (- ?n5 v0))
+(let (?n7 (- ?n4 ?n6))
+(flet ($n8 (= ?n2 ?n7))
+(flet ($n9 false)
+(let (?n10 (ite $n9 ?n1 v1))
+(let (?n11 (+ ?n1 v2))
+(flet ($n12 (<= ?n10 ?n11))
+(let (?n13 (ite $n9 v0 ?n2))
+(let (?n14 (~ ?n1))
+(let (?n15 (ite $n9 ?n14 ?n1))
+(flet ($n16 (< ?n13 ?n15))
+(flet ($n17 (= ?n1 ?n7))
+(let (?n18 (+ ?n1 ?n1))
+(flet ($n19 (= v2 ?n18))
+(let (?n20 (ite $n19 v2 ?n1))
+(let (?n21 (ite $n17 ?n18 ?n20))
+(flet ($n22 (>= ?n21 ?n2))
+(let (?n23 (ite $n9 ?n21 ?n2))
+(flet ($n24 (<= ?n23 ?n1))
+(flet ($n25 (> ?n7 ?n2))
+(flet ($n26 (iff $n24 $n25))
+(let (?n27 (~ ?n7))
+(flet ($n28 (<= ?n27 ?n1))
+(let (?n29 (ite $n28 ?n1 ?n1))
+(flet ($n30 (< ?n1 ?n29))
+(flet ($n31 (implies $n26 $n30))
+(flet ($n32 (implies $n9 $n9))
+(flet ($n33 (if_then_else $n22 $n31 $n32))
+(flet ($n34 (and $n9 $n33))
+(flet ($n35 (if_then_else $n16 $n34 $n9))
+(flet ($n36 (iff $n12 $n35))
+(flet ($n37 (and $n8 $n36))
+$n37
+))))))))))))))))))))))))))))))))))))))