diff options
Diffstat (limited to 'test/regress/regress0/decision/bitvec5.smt')
| -rw-r--r-- | test/regress/regress0/decision/bitvec5.smt | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/test/regress/regress0/decision/bitvec5.smt b/test/regress/regress0/decision/bitvec5.smt deleted file mode 100644 index 6bf931bb5..000000000 --- a/test/regress/regress0/decision/bitvec5.smt +++ /dev/null @@ -1,22 +0,0 @@ -; COMMAND-LINE: --decision=justification -; EXPECT: unsat - -(benchmark bitvec5.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 ((b BitVec[32])) - :extrafuns ((c BitVec[32])) - :extrafuns ((d BitVec[32])) - :extrafuns ((e BitVec[32])) - :formula -(not (and (implies (and (and (= (extract[31:0] a) (extract[31:0] b)) (= (extract[31:16] a) (extract[15:0] c))) (= (extract[31:8] b) (extract[23:0] d))) (= (extract[11:8] c) (extract[19:16] d))) (implies (= (extract[30:0] e) (extract[31:1] e)) (= (extract[0:0] e) (extract[31:31] e))))) -) |