1 files changed, 122 insertions, 0 deletions
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
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+