From b1cb97e9a76bb018e4c9cb7e2d6781dc0412ddad Mon Sep 17 00:00:00 2001 From: lianah Date: Thu, 28 Aug 2014 17:05:49 -0400 Subject: [PATCH] fixing bug580 caused by bad bv inequality explanation --- src/theory/bv/bv_inequality_graph.cpp | 2 +- test/regress/regress0/aufbv/Makefile.am | 2 + test/regress/regress0/aufbv/bug580.delta.smt2 | 10 ++ test/regress/regress0/aufbv/bug580.smt2 | 116 ++++++++++++++++++ 4 files changed, 129 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/aufbv/bug580.delta.smt2 create mode 100644 test/regress/regress0/aufbv/bug580.smt2 diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index aa605de04..f29b8d467 100644 --- 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 e45358a8a..38b58cedd 100644 --- 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 index 000000000..bc9a66f9c --- /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 index 000000000..2f2074385 --- /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) -- 2.30.2