Fixed arithmetic consistency issue. The simplex conflict variable had to be reenqueued so that the queue was a superset of the failing assertions. This adds a super expensive debug routine unenqueuedVariablesAreConsistent() that catches this bug. This is enabled when -d arith::consistency is turned on. make check passes with this flag enabled.

7 files changed, 145 insertions, 32 deletions

diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h
index a4f30e18b..fb80e599e 100644
--- a/src/theory/arith/arith_priority_queue.h
+++ b/src/theory/arith/arith_priority_queue.h
@@ -217,6 +217,11 @@ public:
   void clear();
 
 
+  bool collectionModeContains(ArithVar v) const {
+    Assert(inCollectionMode());
+    return d_varSet.isMember(v);
+  }
+
   class const_iterator {
   private:
     Mode d_mode;
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index ee71dea74..63bb42e7a 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -241,6 +241,7 @@ bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) {
 
 Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){
   Assert(d_conflictVariable == ARITHVAR_SENTINEL);
+  Assert(d_queue.inCollectionMode());
 
   if(d_queue.empty()){
     return Result::SAT;
@@ -352,6 +353,10 @@ Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){
 
 
   d_pivotsInRound.purge();
+  // ensure that the conflict variable is still in the queue.
+  if(d_conflictVariable != ARITHVAR_SENTINEL){
+    d_queue.enqueueIfInconsistent(d_conflictVariable);
+  }
   d_conflictVariable = ARITHVAR_SENTINEL;
 
   d_queue.transitionToCollectionMode();
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index d260ff9b4..a1c69548c 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -224,6 +224,12 @@ public:
     d_queue.clear();
   }
 
+
+  bool debugIsInCollectionQueue(ArithVar var) const{
+    Assert(d_queue.inCollectionMode());
+    return d_queue.collectionModeContains(var);
+  }
+
 private:
 
   /** Reports a conflict to on the output channel. */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index a48a13720..4bc066e08 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -678,7 +678,7 @@ Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubst
       Assert(elim == Rewriter::rewrite(elim));
 
 
-      static const int MAX_SUB_SIZE = 20;
+      static const unsigned MAX_SUB_SIZE = 20;
       if(false && right.size() > MAX_SUB_SIZE){
         Debug("simplify") << "TheoryArith::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl;
         Debug("simplify") << right.size() << endl;
@@ -1384,7 +1384,13 @@ void TheoryArith::check(Effort effortLevel){
   Debug("effortlevel") << "TheoryArith::check " << effortLevel << std::endl;
   Debug("arith") << "TheoryArith::check begun " << effortLevel << std::endl;
 
+  if(Debug.isOn("arith::consistency")){
+    Assert(unenqueuedVariablesAreConsistent());
+  }
+
   bool newFacts = !done();
+  //If previous == SAT, then reverts on conflicts are safe
+  //Otherwise, they are not and must be committed.
   Result::Sat previous = d_qflraStatus;
   if(newFacts){
     d_qflraStatus = Result::SAT_UNKNOWN;
@@ -1397,28 +1403,36 @@ void TheoryArith::check(Effort effortLevel){
       bool res = assertionCases(curr);
       Assert(!res || inConflict());
     }
-    if(inConflict()){
-      revertOutOfConflict();
-      outputConflicts();
-      d_qflraStatus = Result::UNSAT;
-      return;
+    if(inConflict()){ break; }
+  }
+  if(!inConflict()){
+    while(!d_learnedBounds.empty()){
+      // we may attempt some constraints twice.  this is okay!
+      Constraint curr = d_learnedBounds.front();
+      d_learnedBounds.pop();
+      Debug("arith::learned") << curr << endl;
+
+      bool res = assertionCases(curr);
+      Assert(!res || inConflict());
+
+      if(inConflict()){ break; }
     }
   }
-  while(!d_learnedBounds.empty()){
-    // we may attempt some constraints twice.  this is okay!
-    Constraint curr = d_learnedBounds.front();
-    d_learnedBounds.pop();
-    Debug("arith::learned") << curr << endl;
 
-    bool res = assertionCases(curr);
-    Assert(!res || inConflict());
+  if(inConflict()){
+    d_qflraStatus = Result::UNSAT;
+    if(previous == Result::SAT){
+      ++d_statistics.d_revertsOnConflicts;
+      revertOutOfConflict();
+      d_simplex.clearQueue();
+    }else{
+      ++d_statistics.d_commitsOnConflicts;
 
-    if(inConflict()){
-      d_qflraStatus = Result::UNSAT;
+      d_partialModel.commitAssignmentChanges();
       revertOutOfConflict();
-      outputConflicts();
-      return;
     }
+    outputConflicts();
+    return;
   }
 
 
@@ -1427,8 +1441,6 @@ void TheoryArith::check(Effort effortLevel){
   }
 
   bool emmittedConflictOrSplit = false;
-
-
   Assert(d_conflicts.empty());
 
   d_qflraStatus = d_simplex.findModel(fullEffort(effortLevel));
@@ -1439,6 +1451,9 @@ void TheoryArith::check(Effort effortLevel){
     }
     d_partialModel.commitAssignmentChanges();
     d_unknownsInARow = 0;
+    if(Debug.isOn("arith::consistency")){
+      Assert(entireStateIsConsistent());
+    }
     break;
   case Result::SAT_UNKNOWN:
     ++d_unknownsInARow;
@@ -1451,7 +1466,6 @@ void TheoryArith::check(Effort effortLevel){
     d_unknownsInARow = 0;
     if(previous == Result::SAT){
       ++d_statistics.d_revertsOnConflicts;
-
       revertOutOfConflict();
       d_simplex.clearQueue();
     }else{
@@ -1515,8 +1529,9 @@ void TheoryArith::check(Effort effortLevel){
     if(inConflict()){
       Debug("arith::unate") << "unate conflict" << endl;
       revertOutOfConflict();
+      d_qflraStatus = Result::UNSAT;
       outputConflicts();
-      return;
+      emmittedConflictOrSplit = true;
     }
   }else{
     TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
@@ -1720,15 +1735,15 @@ void TheoryArith::propagate(Effort e) {
 
   while(d_constraintDatabase.hasMorePropagations()){
     Constraint c = d_constraintDatabase.nextPropagation();
+    Debug("arith::prop") << "next prop" << getSatContext()->getLevel() << ": " << c << endl;
 
     if(c->negationHasProof()){
-      Node conflict = ConstraintValue::explainConflict(c, c->getNegation());
-      Message() << "tears " << conflict << endl;
-      Debug("arith::prop") << "propagate conflict" << conflict << endl;
-      d_out->conflict(conflict);
-      return;
-    }else if(!c->assertedToTheTheory()){
+      Debug("arith::prop") << "negation has proof " << c->getNegation() << endl
+                           << c->getNegation()->explainForConflict() << endl;
+    }
+    Assert(!c->negationHasProof(), "A constraint has been propagated on the constraint propagation queue, but the negation has been set to true.  Contact Tim now!");
 
+    if(!c->assertedToTheTheory()){
       Node literal = c->getLiteral();
       Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal << endl;
 
@@ -1845,6 +1860,8 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
 Node TheoryArith::getValue(TNode n) {
   NodeManager* nodeManager = NodeManager::currentNM();
 
+  Assert(d_qflraStatus == Result::SAT);
+
   switch(n.getKind()) {
   case kind::VARIABLE: {
     ArithVar var = d_arithvarNodeMap.asArithVar(n);
@@ -1946,15 +1963,40 @@ void TheoryArith::notifyRestart(){
 
 bool TheoryArith::entireStateIsConsistent(){
   typedef std::vector<Node>::const_iterator VarIter;
+  bool result = true;
   for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
     ArithVar var = d_arithvarNodeMap.asArithVar(*i);
     if(!d_partialModel.assignmentIsConsistent(var)){
       d_partialModel.printModel(var);
-      Warning() << "Assignment is not consistent for " << var << *i << endl;
-      return false;
+      Warning() << "Assignment is not consistent for " << var << *i;
+      if(d_tableau.isBasic(var)){
+        Warning() << " (basic)";
+      }
+      Warning() << endl;
+      result = false;
     }
   }
-  return true;
+  return result;
+}
+
+bool TheoryArith::unenqueuedVariablesAreConsistent(){
+  typedef std::vector<Node>::const_iterator VarIter;
+  bool result = true;
+  for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
+    ArithVar var = d_arithvarNodeMap.asArithVar(*i);
+    if(!d_partialModel.assignmentIsConsistent(var) &&
+       !d_simplex.debugIsInCollectionQueue(var)){
+
+      d_partialModel.printModel(var);
+      Warning() << "Unenqueued var is not consistent for " << var << *i;
+      if(d_tableau.isBasic(var)){
+        Warning() << " (basic)";
+      }
+      Warning() << endl;
+      result = false;
+    }
+  }
+  return result;
 }
 
 void TheoryArith::presolve(){
@@ -2066,12 +2108,17 @@ bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){
       bool hasProof = bestImplied->hasProof();
 
       Debug("arith::prop") << "arith::prop" << basic
-        //<< " " << assertedValuation
                            << " " << assertedToTheTheory
                            << " " << canBePropagated
                            << " " << hasProof
                            << endl;
 
+      if(bestImplied->negationHasProof()){
+        Warning() << "the negation of " <<  bestImplied << " : " << endl
+                  << "has proof " << bestImplied->getNegation() << endl
+                  << bestImplied->getNegation()->explainForConflict() << endl;
+      }
+
       if(!assertedToTheTheory && canBePropagated && !hasProof ){
         if(upperBound){
           Assert(bestImplied != d_partialModel.getUpperBoundConstraint(basic));
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 556495c97..4983b0557 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -460,6 +460,7 @@ private:
    * Returns true iff every variable is consistent in the partial model.
    */
   bool entireStateIsConsistent();
+  bool unenqueuedVariablesAreConsistent();
 
   bool isImpliedUpperBound(ArithVar var, Node exp);
   bool isImpliedLowerBound(ArithVar var, Node exp);
diff --git a/test/regress/regress0/arith/DTP_k2_n35_c175_s15.smt2 b/test/regress/regress0/arith/DTP_k2_n35_c175_s15.smt2
new file mode 100644
index 000000000..20f4bf5a9
--- /dev/null
+++ b/test/regress/regress0/arith/DTP_k2_n35_c175_s15.smt2
@@ -0,0 +1,48 @@
+(set-logic QF_IDL)
+(set-info :source |
+Randomly generated benchmarks. Contact TSAT++ group at 
+http://www.ai.dist.unige.it/Tsat for more information.
+
+Translated into SMT-LIB format by Albert Oliveras.
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "random")
+(set-info :status sat)
+(declare-fun x10 () Int)
+(declare-fun x0 () Int)
+(declare-fun x1 () Int)
+(declare-fun x27 () Int)
+(declare-fun x21 () Int)
+(declare-fun x20 () Int)
+(declare-fun x15 () Int)
+(declare-fun x13 () Int)
+(declare-fun x12 () Int)
+(declare-fun x11 () Int)
+(declare-fun x14 () Int)
+(declare-fun x17 () Int)
+(declare-fun x16 () Int)
+(declare-fun x19 () Int)
+(declare-fun x18 () Int)
+(declare-fun x2 () Int)
+(declare-fun x23 () Int)
+(declare-fun x22 () Int)
+(declare-fun x25 () Int)
+(declare-fun x24 () Int)
+(declare-fun x26 () Int)
+(declare-fun x7 () Int)
+(declare-fun x6 () Int)
+(declare-fun x31 () Int)
+(declare-fun x28 () Int)
+(declare-fun x29 () Int)
+(declare-fun x3 () Int)
+(declare-fun x30 () Int)
+(declare-fun x5 () Int)
+(declare-fun x34 () Int)
+(declare-fun x32 () Int)
+(declare-fun x33 () Int)
+(declare-fun x4 () Int)
+(declare-fun x9 () Int)
+(declare-fun x8 () Int)
+(assert (let ((?v_1 (- x10 x27)) (?v_3 (- x25 x24)) (?v_4 (- x24 x22)) (?v_2 (- x3 x27)) (?v_0 (- x34 x28)) (?v_23 (- x12 x27)) (?v_6 (- x29 x24)) (?v_11 (- x24 x12)) (?v_10 (- x1 x7)) (?v_5 (- x30 x27)) (?v_9 (- x24 x18)) (?v_18 (- x31 x13)) (?v_16 (- x15 x2)) (?v_8 (- x33 x7)) (?v_27 (- x3 x5)) (?v_7 (- x0 x33)) (?v_12 (- x22 x19)) (?v_22 (- x33 x32)) (?v_30 (- x22 x11)) (?v_24 (- x7 x19)) (?v_21 (- x30 x33)) (?v_15 (- x17 x6)) (?v_35 (- x21 x9)) (?v_28 (- x7 x3)) (?v_32 (- x1 x6)) (?v_13 (- x10 x24)) (?v_19 (- x6 x13)) (?v_14 (- x11 x12)) (?v_25 (- x5 x32)) (?v_20 (- x29 x4)) (?v_31 (- x19 x23)) (?v_29 (- x2 x3)) (?v_17 (- x18 x25)) (?v_37 (- x22 x13)) (?v_36 (- x6 x25)) (?v_26 (- x31 x12)) (?v_34 (- x17 x21)) (?v_33 (- x8 x23)) (?v_38 (- x14 x28))) (and (or (not (>= ?v_1 2)) (>= (- x21 x7) 66)) (or (>= (- x6 x23) 53) (not (>= ?v_3 40))) (or (>= (- x9 x31) 17) (not (>= (- x20 x25) 61))) (or (>= (- x28 x15) 55) (>= (- x25 x27) 57)) (or (not (>= (- x23 x29) 39)) (>= (- x27 x17) 57)) (or (not (>= ?v_4 9)) (>= (- x0 x5) 86)) (or (not (>= (- x13 x1) 32)) (>= ?v_2 12)) (or (>= (- x34 x31) 29) (not (>= (- x10 x14) 76))) (or (not (>= (- x32 x9) 30)) (not (>= (- x19 x25) 28))) (or (>= (- x29 x23) 1) (>= ?v_0 13)) (or (not (>= (- x20 x1) 59)) (not (>= (- x23 x18) 65))) (or (>= (- x3 x2) 55) (>= (- x16 x23) 58)) (or (not (>= (- x9 x12) 43)) (not (>= ?v_23 95))) (or (>= (- x5 x29) 23) (not (>= (- x3 x10) 77))) (or (>= ?v_6 49) (not (>= ?v_11 70))) (or (not (>= ?v_10 66)) (>= (- x30 x10) 6)) (or (not (>= (- x7 x20) 46)) (not (>= ?v_0 22))) (or (>= ?v_5 16) (>= (- x13 x17) 16)) (or (>= (- x33 x1) 41) (not (>= (- x4 x26) 8))) (or (not (>= (- x20 x26) 1)) (>= (- x10 x20) 55)) (or (>= (- x20 x10) 70) (not (>= (- x23 x15) 64))) (or (>= ?v_1 1) (not (>= (- x18 x11) 1))) (or (>= (- x14 x25) 24) (>= (- x34 x10) 34)) (or (not (>= (- x31 x26) 89)) (not (>= ?v_9 48))) (or (not (>= ?v_18 42)) (not (>= (- x2 x16) 86))) (or (>= (- x4 x27) 51) (not (>= (- x2 x29) 99))) (or (>= ?v_16 12) (not (>= (- x11 x27) 27))) (or (>= (- x2 x9) 75) (>= (- x5 x15) 58)) (or (not (>= (- x7 x23) 53)) (not (>= (- x34 x14) 91))) (or (>= ?v_8 58) (not (>= ?v_2 23))) (or (>= ?v_3 70) (not (>= (- x21 x19) 57))) (or (not (>= ?v_4 80)) (>= (- x0 x12) 24)) (or (not (>= (- x32 x3) 9)) (>= (- x11 x5) 6)) (or (>= ?v_27 34) (>= (- x26 x4) 94)) (or (>= (- x27 x20) 49) (not (>= (- x27 x18) 53))) (or (not (>= (- x7 x30) 17)) (>= (- x0 x2) 12)) (or (>= (- x1 x11) 8) (not (>= ?v_5 84))) (or (not (>= (- x13 x25) 17)) (>= (- x6 x24) 89)) (or (not (>= (- x19 x2) 67)) (not (>= (- x2 x30) 1))) (or (not (>= (- x16 x28) 41)) (>= (- x27 x25) 92)) (or (>= ?v_7 97) (>= (- x32 x11) 59)) (or (not (>= (- x0 x7) 7)) (not (>= ?v_6 1))) (or (>= (- x11 x1) 68) (not (>= (- x9 x22) 74))) (or (>= (- x17 x15) 80) (>= (- x12 x21) 74)) (or (>= (- x29 x22) 75) (>= (- x11 x10) 72)) (or (>= (- x28 x3) 43) (not (>= (- x26 x28) 21))) (or (>= (- x9 x18) 30) (>= (- x3 x9) 17)) (or (not (>= (- x33 x9) 96)) (not (>= (- x19 x11) 84))) (or (not (>= (- x34 x20) 71)) (>= (- x7 x26) 57)) (or (not (>= (- x2 x15) 53)) (>= (- x32 x30) 77)) (or (not (>= (- x22 x12) 47)) (>= ?v_12 83)) (or (not (>= (- x5 x14) 21)) (not (>= (- x10 x17) 62))) (or (not (>= (- x34 x6) 70)) (not (>= (- x8 x12) 75))) (or (not (>= (- x8 x25) 69)) (>= (- x8 x18) 11)) (or (>= (- x16 x21) 45) (not (>= ?v_22 68))) (or (not (>= ?v_7 29)) (not (>= (- x6 x9) 62))) (or (not (>= (- x15 x28) 15)) (>= ?v_30 51)) (or (>= ?v_24 20) (>= (- x17 x7) 63)) (or (not (>= (- x14 x15) 67)) (not (>= (- x23 x16) 21))) (or (not (>= ?v_8 14)) (>= (- x20 x16) 63)) (or (>= (- x33 x3) 74) (>= (- x15 x9) 27)) (or (>= (- x12 x18) 42) (>= (- x10 x26) 12)) (or (>= (- x17 x20) 75) (not (>= (- x3 x13) 41))) (or (not (>= ?v_21 76)) (>= (- x20 x19) 60)) (or (not (>= ?v_15 100)) (not (>= ?v_35 85))) (or (not (>= (- x31 x14) 76)) (not (>= (- x8 x22) 89))) (or (>= (- x8 x29) 11) (not (>= ?v_28 18))) (or (not (>= ?v_9 6)) (not (>= (- x22 x8) 80))) (or (not (>= (- x5 x17) 30)) (>= (- x25 x10) 76)) (or (>= (- x23 x30) 92) (not (>= ?v_32 51))) (or (>= (- x24 x11) 22) (not (>= (- x21 x20) 98))) (or (not (>= (- x9 x27) 14)) (>= ?v_10 73)) (or (>= (- x4 x21) 12) (>= (- x9 x33) 90)) (or (not (>= (- x1 x14) 1)) (>= (- x5 x20) 65)) (or (not (>= (- x3 x26) 29)) (>= (- x27 x7) 13)) (or (not (>= (- x25 x34) 58)) (not (>= ?v_13 40))) (or (not (>= (- x23 x0) 83)) (not (>= ?v_11 1))) (or (>= (- x22 x4) 50) (not (>= (- x17 x4) 28))) (or (not (>= (- x29 x32) 73)) (not (>= (- x10 x23) 21))) (or (>= (- x21 x8) 7) (>= ?v_12 20)) (or (not (>= (- x16 x20) 36)) (>= (- x16 x10) 63)) (or (not (>= ?v_19 31)) (>= (- x10 x7) 96)) (or (>= (- x10 x30) 97) (>= (- x9 x21) 9)) (or (>= (- x2 x11) 21) (not (>= (- x27 x24) 26))) (or (not (>= (- x32 x10) 84)) (not (>= (- x17 x14) 100))) (or (not (>= (- x22 x24) 71)) (not (>= ?v_13 73))) (or (not (>= (- x19 x30) 18)) (>= (- x16 x24) 25)) (or (not (>= ?v_14 51)) (>= ?v_14 91)) (or (not (>= (- x33 x15) 10)) (not (>= ?v_25 90))) (or (not (>= (- x8 x9) 83)) (not (>= (- x30 x3) 93))) (or (>= ?v_20 2) (not (>= ?v_31 60))) (or (not (>= ?v_15 27)) (>= (- x9 x8) 71)) (or (not (>= ?v_29 89)) (>= (- x15 x4) 70)) (or (not (>= (- x21 x28) 78)) (>= (- x7 x9) 74)) (or (not (>= (- x3 x18) 66)) (>= (- x18 x6) 91)) (or (not (>= (- x11 x6) 25)) (>= ?v_17 36)) (or (not (>= ?v_16 49)) (not (>= (- x15 x29) 17))) (or (>= (- x11 x19) 38) (>= (- x34 x30) 55)) (or (not (>= (- x0 x6) 62)) (not (>= (- x18 x10) 45))) (or (not (>= (- x7 x11) 24)) (>= (- x10 x34) 22)) (or (not (>= (- x32 x4) 4)) (not (>= ?v_17 44))) (or (>= (- x15 x18) 48) (not (>= (- x16 x3) 45))) (or (not (>= (- x14 x18) 76)) (not (>= ?v_37 1))) (or (>= (- x18 x12) 95) (>= (- x7 x21) 36)) (or (>= (- x1 x27) 68) (not (>= (- x16 x29) 2))) (or (not (>= (- x31 x21) 72)) (not (>= (- x26 x9) 68))) (or (not (>= (- x12 x28) 98)) (not (>= ?v_18 93))) (or (not (>= (- x3 x31) 96)) (not (>= (- x6 x12) 10))) (or (>= (- x28 x27) 88) (not (>= (- x23 x8) 69))) (or (>= (- x12 x14) 31) (not (>= (- x11 x31) 23))) (or (>= (- x12 x26) 1) (>= ?v_19 38)) (or (>= (- x32 x13) 60) (>= (- x18 x20) 44)) (or (>= ?v_20 13) (not (>= (- x18 x13) 16))) (or (not (>= (- x31 x8) 42)) (not (>= (- x17 x22) 33))) (or (not (>= (- x20 x28) 87)) (not (>= (- x34 x33) 57))) (or (not (>= (- x27 x3) 98)) (not (>= (- x16 x5) 86))) (or (>= (- x29 x14) 48) (>= (- x12 x33) 15)) (or (>= ?v_21 78) (not (>= ?v_22 46))) (or (not (>= (- x1 x0) 82)) (not (>= (- x3 x22) 67))) (or (not (>= (- x31 x3) 80)) (>= (- x9 x25) 29)) (or (not (>= (- x31 x25) 32)) (>= ?v_23 29)) (or (not (>= (- x24 x5) 82)) (not (>= ?v_36 36))) (or (not (>= (- x21 x5) 88)) (not (>= ?v_26 81))) (or (not (>= (- x13 x9) 92)) (not (>= (- x10 x21) 12))) (or (not (>= ?v_24 87)) (not (>= (- x6 x19) 63))) (or (not (>= (- x14 x7) 81)) (>= ?v_25 86)) (or (>= (- x2 x4) 4) (not (>= (- x14 x4) 27))) (or (not (>= (- x24 x9) 35)) (>= ?v_26 48)) (or (not (>= (- x21 x23) 41)) (>= ?v_27 91)) (or (not (>= ?v_28 83)) (>= (- x13 x19) 23)) (or (not (>= (- x17 x0) 78)) (>= (- x4 x3) 94)) (or (>= (- x33 x12) 63) (>= (- x5 x30) 26)) (or (>= (- x8 x27) 69) (not (>= (- x23 x10) 90))) (or (not (>= (- x11 x16) 69)) (not (>= (- x2 x26) 16))) (or (>= (- x10 x22) 20) (>= ?v_34 46)) (or (>= (- x27 x14) 90) (not (>= ?v_29 90))) (or (>= (- x30 x24) 99) (>= (- x29 x7) 29)) (or (>= (- x23 x5) 82) (not (>= (- x32 x20) 55))) (or (not (>= (- x29 x13) 71)) (>= (- x21 x17) 97)) (or (not (>= (- x14 x3) 80)) (not (>= (- x33 x20) 33))) (or (not (>= (- x5 x19) 74)) (not (>= (- x11 x22) 83))) (or (not (>= (- x9 x29) 25)) (not (>= (- x1 x8) 49))) (or (>= ?v_30 23) (not (>= (- x14 x33) 56))) (or (>= ?v_31 55) (not (>= (- x31 x1) 51))) (or (not (>= (- x27 x28) 34)) (not (>= (- x26 x18) 26))) (or (not (>= (- x31 x34) 83)) (>= (- x15 x25) 33)) (or (>= ?v_33 49) (not (>= (- x27 x0) 20))) (or (not (>= (- x29 x3) 68)) (not (>= (- x12 x9) 1))) (or (>= (- x14 x2) 41) (>= (- x22 x1) 63)) (or (>= (- x17 x5) 87) (not (>= (- x10 x15) 55))) (or (not (>= (- x22 x3) 40)) (not (>= (- x4 x0) 85))) (or (>= (- x19 x6) 22) (>= (- x13 x8) 35)) (or (>= (- x32 x14) 54) (>= (- x24 x23) 49)) (or (not (>= (- x23 x13) 15)) (>= (- x7 x17) 14)) (or (not (>= (- x4 x17) 98)) (>= (- x25 x11) 70)) (or (not (>= (- x32 x12) 91)) (>= (- x19 x3) 68)) (or (not (>= ?v_32 35)) (not (>= (- x14 x24) 23))) (or (not (>= (- x30 x5) 26)) (not (>= (- x0 x24) 1))) (or (>= (- x3 x23) 59) (>= (- x30 x14) 56)) (or (not (>= (- x19 x24) 44)) (not (>= ?v_33 18))) (or (not (>= (- x4 x6) 65)) (not (>= ?v_34 71))) (or (>= (- x28 x25) 96) (not (>= (- x28 x26) 81))) (or (not (>= (- x16 x1) 79)) (>= (- x26 x5) 98)) (or (>= (- x29 x20) 54) (>= (- x30 x31) 60)) (or (not (>= (- x18 x28) 16)) (not (>= ?v_38 24))) (or (>= (- x23 x6) 15) (not (>= (- x26 x10) 68))) (or (>= (- x22 x21) 30) (not (>= (- x15 x33) 60))) (or (not (>= (- x3 x6) 35)) (>= ?v_35 84)) (or (not (>= (- x23 x12) 58)) (not (>= ?v_36 80))) (or (not (>= (- x20 x8) 39)) (>= (- x25 x12) 12)) (or (>= (- x13 x16) 98) (>= (- x30 x0) 61)) (or (not (>= (- x5 x3) 83)) (not (>= (- x2 x25) 61))) (or (>= (- x24 x29) 32) (>= ?v_37 32)) (or (>= ?v_38 57) (not (>= (- x32 x31) 29))) (or (>= (- x8 x10) 15) (>= (- x8 x11) 12)))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index 19837d8f1..ffa52ef56 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -19,7 +19,8 @@ TESTS =	\
 	delta-minimized-row-vector-bug.smt \
 	fuzz_3-eq.smt \
 	leq.01.smt \
-	miplibtrick.smt 
+	miplibtrick.smt \
+	DTP_k2_n35_c175_s15.smt2
 #	problem__003.smt2
 
 EXTRA_DIST = $(TESTS)