fixing bug580 caused by bad bv inequality explanation

diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index aa605de0488014ee5311f71a3045688eee712552..f29b8d467da3a8e7a93ed62735abf411f7d05566 100644 (file)
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -146,7 +146,7 @@ bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) {
         if (start_reason != UndefinedReasonId) {
           conflict.push_back(start_reason);
         }
-        computeExplanation(start, current, conflict);
+        computeExplanation(UndefinedTermId, current, conflict);
         Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n"; 
         setConflict(conflict); 
         return false; 

diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am
index e45358a8a2251fc201236131e550dad0686e490f..38b58cedde34f50719344176d111eeac6feaea8c 100644 (file)
--- a/test/regress/regress0/aufbv/Makefile.am
+++ b/test/regress/regress0/aufbv/Makefile.am
@@ -25,6 +25,8 @@ TESTS =       \
        bug348.smt \
        bug451.smt \
        bug509.smt \
+       bug580.smt2 \
+       bug580.delta.smt2 \
        try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \
        try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smt \
        diseqprop.01.smt \

diff --git a/test/regress/regress0/aufbv/bug580.delta.smt2 b/test/regress/regress0/aufbv/bug580.delta.smt2
new file mode 100644 (file)
index 0000000..bc9a66f
--- /dev/null
+++ b/test/regress/regress0/aufbv/bug580.delta.smt2
@@ -0,0 +1,10 @@
+(set-info :source |fuzzsmt|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "random")
+(set-info :status sat)
+(set-logic QF_AUFBV)
+(declare-fun _substvar_43_ () (_ BitVec 3))
+(declare-fun a2 () (Array (_ BitVec 8) (_ BitVec 1)))
+(assert (let ((e5 (_ bv53513 16))) (let ((e7 (ite (bvult e5 ((_ zero_extend 13) _substvar_43_)) (_ bv1 1) (_ bv0 1)))) (let ((e8 a2)) (let ((e9 (store e8 ((_ zero_extend 5) _substvar_43_) (_ bv0 1)))) (let ((e11 (select a2 (_ bv0 8)))) (let ((e12 (select e9 ((_ sign_extend 5) _substvar_43_)))) (let ((e14 (select e8 ((_ sign_extend 7) e7)))) (let ((e28 (bvult e11 e12))) (let ((e30 (bvslt e12 e7))) (let ((e32 (bvult (_ bv0 1) e14))) (let ((e38 (bvslt (_ bv0 1) e12))) (let ((e60 (bvslt e14 e11))) (let ((e65 (=> true e60))) (let ((e74 e38)) (let ((e76 e65)) (let ((e79 (and e74 e74))) (let ((e82 (ite e79 true false))) (let ((e84 (=> true e32))) (let ((e86 (ite e76 false true))) (let ((e90 (=> e82 false))) (let ((e94 (= e84 true))) (let ((e97 e30)) (let ((e98 (not e94))) (let ((e99 (= e98 false))) (let ((e100 (and e97 e97))) (let ((e102 (= true e99))) (let ((e103 e86)) (let ((e104 (= e103 e90))) (let ((e105 (and e102 e100))) (let ((e106 (ite e104 e28 e105))) (let ((e107 e106)) e107))))))))))))))))))))))))))))))))
+(check-sat)
+

diff --git a/test/regress/regress0/aufbv/bug580.smt2 b/test/regress/regress0/aufbv/bug580.smt2
new file mode 100644 (file)
index 0000000..2f20743
--- /dev/null
+++ b/test/regress/regress0/aufbv/bug580.smt2
@@ -0,0 +1,116 @@
+(set-info :source |fuzzsmt|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "random")
+(set-info :status sat)
+(set-logic QF_AUFBV)
+(declare-fun v0 () (_ BitVec 3))
+(declare-fun a1 () (Array  (_ BitVec 3)  (_ BitVec 2)))
+(declare-fun a2 () (Array  (_ BitVec 8)  (_ BitVec 1)))
+(declare-fun a3 () (Array  (_ BitVec 5)  (_ BitVec 15)))
+(assert (let ((e4(_ bv230 8)))
+(let ((e5(_ bv53513 16)))
+(let ((e6 (bvurem ((_ zero_extend 8) e4) e5)))
+(let ((e7 (ite (bvult e5 ((_ zero_extend 13) v0)) (_ bv1 1) (_ bv0 1))))
+(let ((e8 (store a2 ((_ extract 10 3) e6) ((_ extract 0 0) v0))))
+(let ((e9 (store e8 ((_ zero_extend 5) v0) ((_ extract 13 13) e5))))
+(let ((e10 (store a1 ((_ extract 12 10) e6) ((_ extract 9 8) e6))))
+(let ((e11 (select a2 ((_ zero_extend 7) e7))))
+(let ((e12 (select e9 ((_ sign_extend 5) v0))))
+(let ((e13 (store a3 ((_ zero_extend 2) v0) ((_ extract 14 0) e5))))
+(let ((e14 (select e8 ((_ sign_extend 7) e7))))
+(let ((e15 (store e13 ((_ zero_extend 4) e14) ((_ zero_extend 12) v0))))
+(let ((e16 (ite (= e6 e5) (_ bv1 1) (_ bv0 1))))
+(let ((e17 ((_ sign_extend 15) e16)))
+(let ((e18 (ite (bvsle ((_ zero_extend 7) e16) e4) (_ bv1 1) (_ bv0 1))))
+(let ((e19 ((_ rotate_right 0) v0)))
+(let ((e20 (bvshl e12 e7)))
+(let ((e21 (bvnand e14 e14)))
+(let ((e22 (ite (bvugt e7 e18) (_ bv1 1) (_ bv0 1))))
+(let ((e23 ((_ extract 0 0) e11)))
+(let ((e24 (distinct ((_ zero_extend 2) e16) e19)))
+(let ((e25 (bvslt ((_ zero_extend 13) v0) e5)))
+(let ((e26 (bvule e19 ((_ zero_extend 2) e20))))
+(let ((e27 (bvult e17 ((_ zero_extend 15) e11))))
+(let ((e28 (bvult e11 e12)))
+(let ((e29 (= e19 ((_ zero_extend 2) e21))))
+(let ((e30 (bvslt e12 e7)))
+(let ((e31 (= e21 e7)))
+(let ((e32 (bvult e16 e14)))
+(let ((e33 (= ((_ sign_extend 7) e23) e4)))
+(let ((e34 (bvult ((_ sign_extend 15) e7) e6)))
+(let ((e35 (bvsge e14 e23)))
+(let ((e36 (bvsgt e17 ((_ zero_extend 15) e23))))
+(let ((e37 (bvult ((_ sign_extend 15) e12) e6)))
+(let ((e38 (bvslt e23 e12)))
+(let ((e39 (bvule e17 ((_ sign_extend 13) e19))))
+(let ((e40 (distinct ((_ sign_extend 5) e19) e4)))
+(let ((e41 (distinct ((_ sign_extend 15) e21) e6)))
+(let ((e42 (bvsle ((_ zero_extend 15) e16) e6)))
+(let ((e43 (bvsle e12 e23)))
+(let ((e44 (bvult e22 e20)))
+(let ((e45 (bvule e14 e20)))
+(let ((e46 (bvsge ((_ sign_extend 15) e23) e6)))
+(let ((e47 (bvugt e6 ((_ zero_extend 15) e20))))
+(let ((e48 (= e17 e17)))
+(let ((e49 (bvule ((_ zero_extend 15) e20) e6)))
+(let ((e50 (bvsle ((_ sign_extend 15) e11) e17)))
+(let ((e51 (distinct ((_ zero_extend 15) e20) e6)))
+(let ((e52 (bvsge e23 e7)))
+(let ((e53 (bvuge e17 e5)))
+(let ((e54 (distinct e12 e23)))
+(let ((e55 (bvugt ((_ sign_extend 2) e16) v0)))
+(let ((e56 (bvuge e5 e5)))
+(let ((e57 (distinct e17 ((_ zero_extend 15) e14))))
+(let ((e58 (distinct ((_ sign_extend 8) e4) e6)))
+(let ((e59 (bvugt ((_ sign_extend 15) e12) e6)))
+(let ((e60 (bvslt e14 e11)))
+(let ((e61 (bvult ((_ sign_extend 13) v0) e17)))
+(let ((e62 (bvslt e19 ((_ zero_extend 2) e20))))
+(let ((e63 (= v0 ((_ zero_extend 2) e11))))
+(let ((e64 (bvugt ((_ zero_extend 15) e18) e6)))
+(let ((e65 (=> e62 e60)))
+(let ((e66 (xor e27 e26)))
+(let ((e67 (xor e42 e31)))
+(let ((e68 (or e29 e50)))
+(let ((e69 (=> e24 e46)))
+(let ((e70 (not e54)))
+(let ((e71 (=> e58 e55)))
+(let ((e72 (and e63 e45)))
+(let ((e73 (and e37 e36)))
+(let ((e74 (ite e39 e70 e38)))
+(let ((e75 (and e64 e34)))
+(let ((e76 (or e65 e61)))
+(let ((e77 (=> e47 e66)))
+(let ((e78 (=> e56 e33)))
+(let ((e79 (and e74 e74)))
+(let ((e80 (=> e52 e67)))
+(let ((e81 (not e41)))
+(let ((e82 (ite e79 e69 e43)))
+(let ((e83 (and e48 e51)))
+(let ((e84 (=> e68 e32)))
+(let ((e85 (not e40)))
+(let ((e86 (ite e76 e75 e85)))
+(let ((e87 (xor e49 e44)))
+(let ((e88 (ite e35 e57 e59)))
+(let ((e89 (= e25 e87)))
+(let ((e90 (=> e82 e73)))
+(let ((e91 (=> e78 e72)))
+(let ((e92 (= e80 e89)))
+(let ((e93 (not e53)))
+(let ((e94 (= e84 e77)))
+(let ((e95 (and e91 e81)))
+(let ((e96 (xor e95 e88)))
+(let ((e97 (ite e93 e30 e83)))
+(let ((e98 (not e94)))
+(let ((e99 (= e98 e96)))
+(let ((e100 (and e97 e97)))
+(let ((e101 (not e71)))
+(let ((e102 (= e92 e99)))
+(let ((e103 (and e101 e86)))
+(let ((e104 (= e103 e90)))
+(let ((e105 (and e102 e100)))
+(let ((e106 (ite e104 e28 e105)))
+(let ((e107 (and e106 (not (= e5 (_ bv0 16))))))
+e107
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)