diff options
-rw-r--r-- | src/theory/arith/arith_priority_queue.h | 5 | ||||
-rw-r--r-- | src/theory/arith/simplex.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/simplex.h | 6 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 109 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 1 | ||||
-rw-r--r-- | test/regress/regress0/arith/DTP_k2_n35_c175_s15.smt2 | 48 | ||||
-rw-r--r-- | test/regress/regress0/arith/Makefile.am | 3 |
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) |