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.

2 files changed, 50 insertions, 1 deletions

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)