fixed TheoryBool rewriter bug

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
+))))))))))))))))))))))))))))))))))))))))))))))))))
+