diff options
author | lianah <lianahady@gmail.com> | 2013-04-01 15:23:46 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-04-01 15:23:46 -0400 |
commit | bf7f728381bb27163f3e056d698ba4da6316b9c8 (patch) | |
tree | 6393e9d211ba72f3ab21724cac2256b94637aa1d /test/regress/regress0/incorrect1.smt | |
parent | 3cf2615b17761da8d310c7d80b55bdac0aa4c54f (diff) |
fixed TheoryBool rewriter bug
Diffstat (limited to 'test/regress/regress0/incorrect1.smt')
-rw-r--r-- | test/regress/regress0/incorrect1.smt | 57 |
1 files changed, 57 insertions, 0 deletions
diff --git a/test/regress/regress0/incorrect1.smt b/test/regress/regress0/incorrect1.smt new file mode 100644 index 000000000..f1352334c --- /dev/null +++ b/test/regress/regress0/incorrect1.smt @@ -0,0 +1,57 @@ +(benchmark fuzzsmt +:logic QF_BV +:status unknown +:extrafuns ((v0 BitVec[10])) +:formula +(let (?e1 bv30369[16]) +(let (?e2 bv3[2]) +(let (?e3 (ite (bvule ?e1 ?e1) bv1[1] bv0[1])) +(let (?e4 (bvcomp (zero_extend[1] ?e3) ?e2)) +(let (?e5 (ite (bvsgt (sign_extend[15] ?e4) ?e1) bv1[1] bv0[1])) +(let (?e6 (bvsmod ?e1 ?e1)) +(let (?e7 (bvsdiv v0 v0)) +(flet ($e8 (bvult ?e2 ?e2)) +(flet ($e9 (bvsge ?e7 (zero_extend[9] ?e3))) +(flet ($e10 (bvugt (sign_extend[15] ?e4) ?e6)) +(flet ($e11 (bvsgt (sign_extend[15] ?e3) ?e6)) +(flet ($e12 (bvsgt v0 (sign_extend[9] ?e3))) +(flet ($e13 (bvsgt ?e4 ?e4)) +(flet ($e14 (bvsle ?e1 (zero_extend[14] ?e2))) +(flet ($e15 (bvslt (sign_extend[14] ?e2) ?e6)) +(flet ($e16 (bvslt (zero_extend[9] ?e3) ?e7)) +(flet ($e17 (= ?e6 (sign_extend[15] ?e3))) +(flet ($e18 (= (zero_extend[8] ?e2) v0)) +(flet ($e19 (bvsgt ?e2 (sign_extend[1] ?e3))) +(flet ($e20 (bvslt ?e3 ?e4)) +(flet ($e21 (bvslt ?e6 (zero_extend[15] ?e4))) +(flet ($e22 (distinct (zero_extend[9] ?e4) v0)) +(flet ($e23 (bvuge ?e1 (sign_extend[15] ?e5))) +(flet ($e24 (or $e12 $e19)) +(flet ($e25 (implies $e16 $e8)) +(flet ($e26 (and $e14 $e20)) +(flet ($e27 (not $e13)) +(flet ($e28 (not $e22)) +(flet ($e29 (xor $e11 $e23)) +(flet ($e30 (or $e29 $e15)) +(flet ($e31 (not $e26)) +(flet ($e32 (iff $e31 $e18)) +(flet ($e33 (and $e27 $e17)) +(flet ($e34 (xor $e21 $e10)) +(flet ($e35 (xor $e32 $e33)) +(flet ($e36 (and $e30 $e30)) +(flet ($e37 (xor $e9 $e9)) +(flet ($e38 (xor $e36 $e34)) +(flet ($e39 (or $e24 $e25)) +(flet ($e40 (iff $e38 $e28)) +(flet ($e41 (iff $e40 $e35)) +(flet ($e42 (not $e37)) +(flet ($e43 (and $e42 $e42)) +(flet ($e44 (iff $e43 $e41)) +(flet ($e45 (iff $e39 $e44)) +(flet ($e46 (and $e45 (not (= v0 bv0[10])))) +(flet ($e47 (and $e46 (not (= v0 (bvnot bv0[10]))))) +(flet ($e48 (and $e47 (not (= ?e1 bv0[16])))) +(flet ($e49 (and $e48 (not (= ?e1 (bvnot bv0[16]))))) +$e49 +)))))))))))))))))))))))))))))))))))))))))))))))))) + |