From 52d6dc20c61007a5c066590aa1fd0b95ed3c2527 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Wed, 4 Apr 2012 02:02:06 +0000 Subject: * added propagation as lemmas to TheoryBV: * modified BVMinisat to work incrementally * added more bv regressions --- test/regress/regress0/bv/fuzz02.smt | 122 ++++++++++++++++++++++++++++++++++++ 1 file changed, 122 insertions(+) create mode 100644 test/regress/regress0/bv/fuzz02.smt (limited to 'test/regress/regress0/bv/fuzz02.smt') diff --git a/test/regress/regress0/bv/fuzz02.smt b/test/regress/regress0/bv/fuzz02.smt new file mode 100644 index 000000000..41b616ef0 --- /dev/null +++ b/test/regress/regress0/bv/fuzz02.smt @@ -0,0 +1,122 @@ +(benchmark fuzzsmt +:logic QF_BV +:status sat +:extrafuns ((v0 BitVec[3])) +:extrafuns ((v1 BitVec[12])) +:extrafuns ((v2 BitVec[9])) +:formula +(let (?e3 bv10[9]) +(let (?e4 (extract[6:6] ?e3)) +(let (?e5 (ite (bvult v2 v2) bv1[1] bv0[1])) +(let (?e6 (ite (bvsgt ?e4 ?e4) bv1[1] bv0[1])) +(let (?e7 (sign_extend[5] ?e6)) +(let (?e8 (concat ?e7 ?e5)) +(let (?e9 (bvcomp ?e8 (zero_extend[1] ?e7))) +(let (?e10 (ite (bvule ?e7 (zero_extend[5] ?e9)) bv1[1] bv0[1])) +(let (?e11 (bvadd (sign_extend[2] ?e10) v0)) +(let (?e12 (extract[1:0] v0)) +(let (?e13 (ite (bvslt ?e12 ?e12) bv1[1] bv0[1])) +(let (?e14 (ite (bvult ?e7 (sign_extend[4] ?e12)) bv1[1] bv0[1])) +(let (?e15 (bvlshr (sign_extend[8] ?e4) v2)) +(let (?e16 (repeat[2] v0)) +(let (?e17 (rotate_right[4] ?e15)) +(let (?e18 (bvxor ?e14 ?e14)) +(let (?e19 (bvand v2 (sign_extend[7] ?e12))) +(let (?e20 (bvnot v1)) +(flet ($e21 (= ?e15 ?e3)) +(flet ($e22 (= (sign_extend[6] ?e9) ?e8)) +(flet ($e23 (= ?e6 ?e4)) +(flet ($e24 (= ?e11 (zero_extend[2] ?e13))) +(flet ($e25 (= v0 (zero_extend[2] ?e13))) +(flet ($e26 (= (sign_extend[1] ?e4) ?e12)) +(flet ($e27 (= ?e15 ?e3)) +(flet ($e28 (= ?e3 ?e19)) +(flet ($e29 (= (zero_extend[8] ?e14) ?e15)) +(flet ($e30 (= v0 (sign_extend[2] ?e6))) +(flet ($e31 (= ?e11 (sign_extend[2] ?e4))) +(flet ($e32 (= ?e7 (zero_extend[5] ?e6))) +(flet ($e33 (= ?e5 ?e5)) +(flet ($e34 (= (zero_extend[8] ?e6) v2)) +(flet ($e35 (= ?e20 (zero_extend[3] ?e3))) +(flet ($e36 (= (zero_extend[8] ?e4) ?e15)) +(flet ($e37 (= ?e3 (sign_extend[8] ?e5))) +(flet ($e38 (= (sign_extend[11] ?e9) v1)) +(flet ($e39 (= (zero_extend[1] ?e9) ?e12)) +(flet ($e40 (= (sign_extend[6] v0) ?e15)) +(flet ($e41 (= ?e7 (zero_extend[5] ?e14))) +(flet ($e42 (= ?e6 ?e14)) +(flet ($e43 (= ?e16 (zero_extend[5] ?e4))) +(flet ($e44 (= (zero_extend[8] ?e9) v2)) +(flet ($e45 (= v1 (zero_extend[11] ?e5))) +(flet ($e46 (= ?e8 (zero_extend[6] ?e4))) +(flet ($e47 (= (sign_extend[1] ?e13) ?e12)) +(flet ($e48 (= (zero_extend[11] ?e18) v1)) +(flet ($e49 (= (zero_extend[11] ?e5) v1)) +(flet ($e50 (= ?e15 (sign_extend[8] ?e4))) +(flet ($e51 (= ?e13 ?e14)) +(flet ($e52 (= (zero_extend[2] ?e5) ?e11)) +(flet ($e53 (= (sign_extend[11] ?e9) v1)) +(flet ($e54 (= ?e8 (sign_extend[6] ?e5))) +(flet ($e55 (= (sign_extend[7] ?e12) v2)) +(flet ($e56 (= ?e20 (sign_extend[3] ?e15))) +(flet ($e57 (= ?e15 (sign_extend[6] ?e11))) +(flet ($e58 (= ?e6 ?e4)) +(flet ($e59 (= (sign_extend[8] ?e10) v2)) +(flet ($e60 (= (zero_extend[8] ?e10) ?e19)) +(flet ($e61 (= ?e9 ?e6)) +(flet ($e62 (= ?e11 (sign_extend[2] ?e9))) +(flet ($e63 (= v2 (zero_extend[8] ?e18))) +(flet ($e64 (= (sign_extend[2] ?e10) ?e11)) +(flet ($e65 (= ?e5 ?e5)) +(flet ($e66 (= (zero_extend[3] ?e16) ?e17)) +(flet ($e67 (if_then_else $e34 $e37 $e22)) +(flet ($e68 (xor $e61 $e63)) +(flet ($e69 (iff $e55 $e53)) +(flet ($e70 (not $e51)) +(flet ($e71 (or $e70 $e56)) +(flet ($e72 (or $e23 $e54)) +(flet ($e73 (or $e43 $e39)) +(flet ($e74 (implies $e58 $e32)) +(flet ($e75 (and $e21 $e59)) +(flet ($e76 (implies $e33 $e38)) +(flet ($e77 (and $e41 $e57)) +(flet ($e78 (if_then_else $e77 $e74 $e64)) +(flet ($e79 (iff $e36 $e52)) +(flet ($e80 (or $e29 $e25)) +(flet ($e81 (iff $e68 $e62)) +(flet ($e82 (xor $e78 $e76)) +(flet ($e83 (xor $e66 $e69)) +(flet ($e84 (or $e45 $e27)) +(flet ($e85 (xor $e83 $e79)) +(flet ($e86 (if_then_else $e72 $e72 $e65)) +(flet ($e87 (iff $e28 $e75)) +(flet ($e88 (if_then_else $e26 $e73 $e47)) +(flet ($e89 (xor $e60 $e60)) +(flet ($e90 (xor $e49 $e42)) +(flet ($e91 (iff $e44 $e48)) +(flet ($e92 (and $e71 $e80)) +(flet ($e93 (not $e88)) +(flet ($e94 (iff $e35 $e35)) +(flet ($e95 (iff $e81 $e90)) +(flet ($e96 (xor $e89 $e85)) +(flet ($e97 (xor $e82 $e94)) +(flet ($e98 (or $e92 $e40)) +(flet ($e99 (implies $e93 $e24)) +(flet ($e100 (if_then_else $e46 $e31 $e50)) +(flet ($e101 (or $e86 $e97)) +(flet ($e102 (and $e101 $e67)) +(flet ($e103 (if_then_else $e87 $e96 $e30)) +(flet ($e104 (not $e100)) +(flet ($e105 (xor $e91 $e104)) +(flet ($e106 (if_then_else $e84 $e102 $e84)) +(flet ($e107 (implies $e106 $e98)) +(flet ($e108 (implies $e107 $e103)) +(flet ($e109 (or $e95 $e95)) +(flet ($e110 (implies $e108 $e109)) +(flet ($e111 (not $e99)) +(flet ($e112 (or $e110 $e105)) +(flet ($e113 (or $e112 $e112)) +(flet ($e114 (xor $e111 $e113)) +$e114 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + -- cgit v1.2.3