diff options
Diffstat (limited to 'test/regress/regress0/decision/bitvec0.smtv1.smt2')
| -rw-r--r-- | test/regress/regress0/decision/bitvec0.smtv1.smt2 | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/regress0/decision/bitvec0.smtv1.smt2 b/test/regress/regress0/decision/bitvec0.smtv1.smt2 new file mode 100644 index 000000000..0739cc754 --- /dev/null +++ b/test/regress/regress0/decision/bitvec0.smtv1.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat +(set-option :incremental false) +(set-info :source "Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. +Contributed by Vijay Ganesh (vganesh@stanford.edu). Translated into SMT-LIB +format by Clark Barrett using CVC3.") +(set-info :status unsat) +(set-info :difficulty "0") +(set-info :category "crafted") +(set-logic QF_BV) +(declare-fun a () (_ BitVec 32)) +(declare-fun t () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) +(declare-fun aa () (_ BitVec 32)) +(declare-fun c () (_ BitVec 32)) +(declare-fun d () (_ BitVec 32)) +(declare-fun aaaa () (_ BitVec 32)) +(declare-fun bbb () (_ BitVec 32)) +(declare-fun aaa () (_ BitVec 32)) +(declare-fun z () (_ BitVec 32)) +(check-sat-assuming ( (let ((_let_0 ((_ extract 6 2) a))) (let ((_let_1 ((_ extract 2 2) t))) (let ((_let_2 ((_ extract 6 6) t))) (let ((_let_3 ((_ extract 2 0) b))) (let ((_let_4 ((_ extract 2 0) c))) (not (and (and (and (ite (= (concat (concat (_ bv0 1) ((_ extract 3 2) a)) ((_ extract 6 5) a)) _let_0) (= _let_0 (_ bv0 5)) (ite (or (or (= (_ bv2 3) (_ bv6 3)) (= (_ bv0 3) (_ bv6 3))) (= (_ bv7 3) (_ bv6 3))) false true)) (and (ite (= (concat ((_ extract 3 2) t) ((_ extract 6 5) t)) ((_ extract 5 2) t)) (= _let_1 _let_2) true) (ite (= ((_ extract 4 0) t) ((_ extract 6 2) t)) (and (and (= _let_1 ((_ extract 4 4) t)) (= ((_ extract 0 0) t) _let_2)) (= ((_ extract 1 1) t) ((_ extract 5 5) t))) true))) (=> (and (and (= _let_3 ((_ extract 2 0) aa)) (= _let_4 _let_3)) (= _let_4 ((_ extract 2 0) d))) (= ((_ extract 1 1) d) ((_ extract 1 1) aa)))) (and (and (and (ite (= (_ bv7 3) ((_ extract 2 0) aaaa)) (= (_ bv1 1) ((_ extract 1 1) aaaa)) true) (ite (= ((_ extract 2 0) bbb) ((_ extract 2 0) aaa)) (= ((_ extract 1 1) bbb) ((_ extract 1 1) aaa)) true)) (= (concat (concat (concat (_ bv4 3) (_ bv1 1)) (_ bv1 1)) (_ bv2 2)) (concat (concat (_ bv1 1) (_ bv7 5)) (_ bv0 1)))) (ite (= (_ bv3 2) ((_ extract 1 0) z)) (= (_ bv1 1) ((_ extract 0 0) z)) true))))))))) )) |