diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-13 14:00:35 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-13 14:00:35 +0000 |
commit | be5c0f29e6be61edf6a197bd8e96cdeffaaffbc4 (patch) | |
tree | 5a53b4dab644ae284b1eccc6440606973463c400 /test/regress/regress0/decision/bitvec0.smt | |
parent | c6aecebe573aeed87ef0661b38af7c3cbc7d641f (diff) |
decision regressions, all but one fail
Diffstat (limited to 'test/regress/regress0/decision/bitvec0.smt')
-rw-r--r-- | test/regress/regress0/decision/bitvec0.smt | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/regress0/decision/bitvec0.smt b/test/regress/regress0/decision/bitvec0.smt new file mode 100644 index 000000000..12766375f --- /dev/null +++ b/test/regress/regress0/decision/bitvec0.smt @@ -0,0 +1,24 @@ +(benchmark bitvec0.smt + :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. + +} + :status unsat + :difficulty { 0 } + :category { crafted } + :logic QF_BV + :extrafuns ((a BitVec[32])) + :extrafuns ((t BitVec[32])) + :extrafuns ((b BitVec[32])) + :extrafuns ((aa BitVec[32])) + :extrafuns ((c BitVec[32])) + :extrafuns ((d BitVec[32])) + :extrafuns ((aaaa BitVec[32])) + :extrafuns ((bbb BitVec[32])) + :extrafuns ((aaa BitVec[32])) + :extrafuns ((z BitVec[32])) + :formula +(let (?cvc_0 (extract[6:2] a)) (let (?cvc_1 (extract[2:2] t)) (let (?cvc_2 (extract[6:6] t)) (let (?cvc_3 (extract[2:0] b)) (let (?cvc_4 (extract[2:0] c)) (not (and (and (and (if_then_else (= (concat (concat bv0[1] (extract[3:2] a)) (extract[6:5] a)) ?cvc_0) (= ?cvc_0 bv0[5]) (if_then_else (or (or (= bv2[3] bv6[3]) (= bv0[3] bv6[3]) ) (= bv7[3] bv6[3]) ) false true)) (and (if_then_else (= (concat (extract[3:2] t) (extract[6:5] t)) (extract[5:2] t)) (= ?cvc_1 ?cvc_2) true) (if_then_else (= (extract[4:0] t) (extract[6:2] t)) (and (and (= ?cvc_1 (extract[4:4] t)) (= (extract[0:0] t) ?cvc_2)) (= (extract[1:1] t) (extract[5:5] t))) true))) (implies (and (and (= ?cvc_3 (extract[2:0] aa)) (= ?cvc_4 ?cvc_3)) (= ?cvc_4 (extract[2:0] d))) (= (extract[1:1] d) (extract[1:1] aa)))) (and (and (and (if_then_else (= bv7[3] (extract[2:0] aaaa)) (= bv1[1] (extract[1:1] aaaa)) true) (if_then_else (= (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]))) (if_then_else (= bv3[2] (extract[1:0] z)) (= bv1[1] (extract[0:0] z)) true))))))))) +) |