failing bv examples

1 files changed, 143 insertions, 0 deletions

diff --git a/test/regress/regress0/bv/fuzz27.smt b/test/regress/regress0/bv/fuzz27.smt
new file mode 100644
index 000000000..c26632ebc
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz27.smt
@@ -0,0 +1,143 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:status unknown
+:extrafuns ((v0 BitVec[4]))
+:extrafuns ((v1 BitVec[4]))
+:extrafuns ((v2 BitVec[4]))
+:extrafuns ((v3 BitVec[4]))
+:formula
+(let (?e4 bv8[4])
+(let (?e5 bv9[4])
+(let (?e6 bv11[4])
+(let (?e7 (ite (bvslt ?e6 ?e5) bv1[1] bv0[1]))
+(let (?e8 (bvor (sign_extend[3] ?e7) ?e4))
+(let (?e9 (ite (bvslt v0 ?e6) bv1[1] bv0[1]))
+(let (?e10 (bvxnor ?e8 ?e5))
+(let (?e11 (zero_extend[0] v3))
+(let (?e12 (bvxnor (sign_extend[3] ?e7) ?e6))
+(let (?e13 (bvnot v3))
+(let (?e14 (ite (bvugt ?e12 v3) bv1[1] bv0[1]))
+(let (?e15 (bvcomp ?e10 ?e12))
+(let (?e16 (bvxnor v3 ?e6))
+(let (?e17 (rotate_right[0] ?e9))
+(let (?e18 (bvneg ?e17))
+(let (?e19 (bvor (zero_extend[3] ?e7) ?e10))
+(let (?e20 (bvnot ?e17))
+(let (?e21 (ite (bvsle ?e4 ?e12) bv1[1] bv0[1]))
+(let (?e22 (bvxnor ?e9 ?e15))
+(let (?e23 (bvadd v1 ?e19))
+(let (?e24 (bvashr ?e17 ?e22))
+(let (?e25 (bvnor (sign_extend[3] ?e15) ?e16))
+(let (?e26 (ite (bvule ?e11 ?e4) bv1[1] bv0[1]))
+(let (?e27 (ite (bvsle ?e4 (sign_extend[3] ?e9)) bv1[1] bv0[1]))
+(let (?e28 (ite (bvuge ?e23 v3) bv1[1] bv0[1]))
+(let (?e29 (ite (bvsgt ?e11 (sign_extend[3] ?e7)) bv1[1] bv0[1]))
+(let (?e30 (ite (= bv1[1] (extract[0:0] ?e29)) (sign_extend[3] ?e24) ?e6))
+(let (?e31 (ite (bvugt v1 ?e16) bv1[1] bv0[1]))
+(let (?e32 (bvand v2 ?e23))
+(flet ($e33 (bvugt (sign_extend[3] ?e29) ?e11))
+(flet ($e34 (distinct ?e20 ?e18))
+(flet ($e35 (bvult ?e19 ?e30))
+(flet ($e36 (bvult ?e11 ?e25))
+(flet ($e37 (bvuge (zero_extend[3] ?e14) ?e4))
+(flet ($e38 (= ?e15 ?e17))
+(flet ($e39 (bvslt (sign_extend[3] ?e17) ?e16))
+(flet ($e40 (bvult (zero_extend[3] ?e24) ?e30))
+(flet ($e41 (distinct ?e13 ?e12))
+(flet ($e42 (bvslt ?e16 ?e11))
+(flet ($e43 (bvsle ?e12 (sign_extend[3] ?e22)))
+(flet ($e44 (bvuge ?e15 ?e26))
+(flet ($e45 (bvsgt ?e19 (zero_extend[3] ?e18)))
+(flet ($e46 (bvslt ?e30 ?e23))
+(flet ($e47 (bvsgt ?e32 ?e8))
+(flet ($e48 (bvule ?e10 (sign_extend[3] ?e31)))
+(flet ($e49 (bvslt (sign_extend[3] ?e15) v0))
+(flet ($e50 (bvsgt (sign_extend[3] ?e14) v1))
+(flet ($e51 (bvslt v3 ?e23))
+(flet ($e52 (distinct ?e6 (sign_extend[3] ?e20)))
+(flet ($e53 (bvugt v2 ?e32))
+(flet ($e54 (bvsge ?e18 ?e15))
+(flet ($e55 (bvsgt ?e32 (sign_extend[3] ?e20)))
+(flet ($e56 (bvuge ?e21 ?e21))
+(flet ($e57 (bvule ?e22 ?e14))
+(flet ($e58 (= ?e28 ?e17))
+(flet ($e59 (bvslt (sign_extend[3] ?e27) ?e19))
+(flet ($e60 (bvult ?e24 ?e20))
+(flet ($e61 (bvugt ?e5 (sign_extend[3] ?e20)))
+(flet ($e62 (bvsle ?e26 ?e28))
+(flet ($e63 (bvule ?e31 ?e26))
+(flet ($e64 (bvuge ?e21 ?e18))
+(flet ($e65 (bvuge (sign_extend[3] ?e24) ?e13))
+(flet ($e66 (bvsge ?e23 ?e16))
+(flet ($e67 (bvugt (zero_extend[3] ?e17) ?e12))
+(flet ($e68 (bvsgt ?e30 v1))
+(flet ($e69 (bvule ?e16 ?e30))
+(flet ($e70 (bvult ?e22 ?e17))
+(flet ($e71 (bvult v1 ?e19))
+(flet ($e72 (bvuge ?e24 ?e28))
+(flet ($e73 (bvsge ?e11 (sign_extend[3] ?e22)))
+(flet ($e74 (bvsgt ?e7 ?e18))
+(flet ($e75 (distinct ?e32 ?e16))
+(flet ($e76 (bvsge v3 ?e16))
+(flet ($e77 (bvsle (sign_extend[3] ?e15) v1))
+(flet ($e78 (bvule ?e8 ?e23))
+(flet ($e79 (bvsge ?e30 (sign_extend[3] ?e14)))
+(flet ($e80 (bvsge ?e4 (zero_extend[3] ?e18)))
+(flet ($e81 (bvslt v1 ?e4))
+(flet ($e82 (bvslt ?e5 v3))
+(flet ($e83 (distinct ?e29 ?e7))
+(flet ($e84 (bvult v1 ?e32))
+(flet ($e85 (bvslt (zero_extend[3] ?e27) ?e5))
+(flet ($e86 (bvslt v0 (zero_extend[3] ?e17)))
+(flet ($e87 (bvsge (sign_extend[3] ?e24) ?e8))
+(flet ($e88 (bvslt ?e16 ?e12))
+(flet ($e89 (bvsge ?e29 ?e18))
+(flet ($e90 (bvsge v1 (sign_extend[3] ?e26)))
+(flet ($e91 (bvsle (sign_extend[3] ?e26) ?e25))
+(flet ($e92 (bvsgt v0 ?e32))
+(flet ($e93 (bvult ?e17 ?e17))
+(flet ($e94 (distinct v0 ?e11))
+(flet ($e95 (bvsgt ?e4 ?e5))
+(flet ($e96 (bvsge ?e7 ?e18))
+(flet ($e97 (distinct ?e16 ?e32))
+(flet ($e98 (bvslt v3 (sign_extend[3] ?e22)))
+(flet ($e99 (bvsge ?e28 ?e9))
+(flet ($e100 
+(and
+ (or $e96 $e47 $e61)
+ (or (not $e97) (not $e88) (not $e40))
+ (or $e40 (not $e45) $e61)
+ (or (not $e86) (not $e95) $e82)
+ (or $e65 $e59 (not $e50))
+ (or $e35 (not $e70) (not $e83))
+ (or $e40 $e98 (not $e96))
+ (or $e84 (not $e87) (not $e95))
+ (or (not $e58) $e98 $e41)
+ (or (not $e64) (not $e46) $e85)
+ (or $e43 (not $e60) $e89)
+ (or $e55 (not $e38) (not $e34))
+ (or $e35 $e58 (not $e39))
+ (or $e87 (not $e47) $e68)
+ (or $e52 (not $e79) $e35)
+ (or (not $e67) $e65 $e43)
+ (or $e60 (not $e71) (not $e84))
+ (or (not $e46) $e63 (not $e67))
+ (or $e57 $e41 $e88)
+ (or (not $e60) $e52 $e50)
+ (or (not $e57) $e88 (not $e99))
+ (or $e69 $e45 $e35)
+ (or (not $e38) (not $e48) $e77)
+ (or (not $e38) $e60 $e69)
+ (or (not $e94) (not $e77) $e68)
+ (or (not $e76) (not $e68) $e97)
+ (or (not $e75) (not $e43) $e72)
+ (or (not $e54) $e42 (not $e61))
+ (or (not $e89) $e42 $e44)
+ (or (not $e73) $e68 $e39)
+ (or $e82 $e69 (not $e89))
+ (or (not $e38) (not $e67) $e55)
+ (or (not $e92) (not $e63) $e99)
+))
+$e100
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+