1 files changed, 0 insertions, 122 deletions
diff --git a/test/regress/regress0/bv/fuzz37.smt b/test/regress/regress0/bv/fuzz37.smt
deleted file mode 100644
index 98fdfda48..000000000
--- a/test/regress/regress0/bv/fuzz37.smt
+++ /dev/null
@@ -1,122 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_BV
-:status sat
-:extrafuns ((v0 BitVec[4]))
-:extrafuns ((v1 BitVec[4]))
-:extrafuns ((v2 BitVec[4]))
-:extrafuns ((v3 BitVec[4]))
-:extrafuns ((v4 BitVec[4]))
-:formula
-(let (?e5 bv2[4])
-(let (?e6 bv2[4])
-(let (?e7 (bvlshr v4 v3))
-(let (?e8 (ite (bvugt ?e5 v1) bv1[1] bv0[1]))
-(let (?e9 (bvor v3 v1))
-(let (?e10 (bvnot v4))
-(let (?e11 (bvsub v0 ?e6))
-(let (?e12 (bvnor ?e5 (zero_extend[3] ?e8)))
-(let (?e13 (bvmul ?e12 v1))
-(let (?e14 (ite (= ?e10 v3) bv1[1] bv0[1]))
-(let (?e15 (ite (bvult v0 ?e11) bv1[1] bv0[1]))
-(let (?e16 (bvashr ?e9 ?e5))
-(let (?e17 (bvnor v1 ?e11))
-(let (?e18 (bvcomp ?e17 ?e11))
-(let (?e19 (zero_extend[0] ?e13))
-(let (?e20 (bvsub v3 ?e19))
-(let (?e21 (bvshl v4 ?e10))
-(let (?e22 (ite (bvule ?e10 (sign_extend[3] ?e14)) bv1[1] bv0[1]))
-(let (?e23 (concat ?e15 ?e15))
-(let (?e24 (rotate_left[0] v1))
-(let (?e25 (bvshl ?e21 v1))
-(let (?e26 (bvnor ?e24 ?e7))
-(let (?e27 (bvand ?e11 v0))
-(let (?e28 (bvlshr ?e20 (zero_extend[3] ?e8)))
-(let (?e29 (bvcomp ?e10 v2))
-(flet ($e30 (bvuge (zero_extend[3] ?e14) v2))
-(flet ($e31 (bvult ?e17 ?e12))
-(flet ($e32 (distinct ?e16 ?e17))
-(flet ($e33 (bvuge (zero_extend[3] ?e18) ?e21))
-(flet ($e34 (= ?e20 ?e19))
-(flet ($e35 (bvuge ?e27 (sign_extend[3] ?e18)))
-(flet ($e36 (bvult ?e10 ?e27))
-(flet ($e37 (bvugt v3 v1))
-(flet ($e38 (bvuge ?e24 ?e17))
-(flet ($e39 (bvult v1 (sign_extend[2] ?e23)))
-(flet ($e40 (bvsle (sign_extend[3] ?e22) ?e5))
-(flet ($e41 (bvult ?e25 ?e5))
-(flet ($e42 (distinct ?e10 ?e16))
-(flet ($e43 (bvugt ?e24 (sign_extend[3] ?e22)))
-(flet ($e44 (bvuge (zero_extend[3] ?e8) ?e20))
-(flet ($e45 (bvsgt ?e6 ?e11))
-(flet ($e46 (bvslt v1 ?e26))
-(flet ($e47 (bvsgt v1 ?e16))
-(flet ($e48 (bvsgt ?e7 v3))
-(flet ($e49 (bvugt ?e16 ?e12))
-(flet ($e50 (bvule ?e14 ?e22))
-(flet ($e51 (bvsgt v3 ?e9))
-(flet ($e52 (bvugt ?e24 (zero_extend[3] ?e14)))
-(flet ($e53 (= v2 (zero_extend[3] ?e22)))
-(flet ($e54 (bvuge ?e5 (sign_extend[3] ?e29)))
-(flet ($e55 (bvsgt ?e13 ?e16))
-(flet ($e56 (bvsge ?e21 ?e6))
-(flet ($e57 (bvuge ?e11 v4))
-(flet ($e58 (bvslt ?e6 ?e28))
-(flet ($e59 (bvsle (sign_extend[3] ?e29) ?e27))
-(flet ($e60 (bvslt ?e20 ?e24))
-(flet ($e61 (bvsge (zero_extend[3] ?e14) ?e28))
-(flet ($e62 (bvsle ?e20 ?e13))
-(flet ($e63 (bvsge ?e25 ?e21))
-(flet ($e64 (distinct (sign_extend[3] ?e29) v4))
-(flet ($e65 (distinct (zero_extend[3] ?e29) ?e10))
-(flet ($e66 (bvsle (zero_extend[2] ?e23) ?e27))
-(flet ($e67 (bvsgt ?e17 v3))
-(flet ($e68 (bvule v1 (sign_extend[3] ?e18)))
-(flet ($e69 (bvule ?e25 ?e7))
-(flet ($e70 (bvuge v1 ?e28))
-(flet ($e71 (bvugt v2 ?e9))
-(flet ($e72 (distinct (zero_extend[3] ?e29) ?e6))
-(flet ($e73 (bvslt v1 ?e13))
-(flet ($e74 (bvuge (zero_extend[3] ?e14) ?e12))
-(flet ($e75 (bvult (zero_extend[3] ?e8) v4))
-(flet ($e76 (bvslt v0 ?e19))
-(flet ($e77 (bvule ?e29 ?e22))
-(flet ($e78 (distinct (sign_extend[3] ?e14) ?e16))
-(flet ($e79 (bvule ?e27 ?e20))
-(flet ($e80 (bvsgt v0 (zero_extend[2] ?e23)))
-(flet ($e81 (bvule ?e21 v2))
-(flet ($e82 (bvsge ?e28 v3))
-(flet ($e83 (distinct (sign_extend[3] ?e8) ?e13))
-(flet ($e84 (bvule (sign_extend[3] ?e15) v2))
-(flet ($e85 
-(and
- (or $e32 $e81 (not $e60))
- (or (not $e60) $e69 $e50)
- (or (not $e53) (not $e67) $e51)
- (or $e30 $e62 $e78)
- (or $e37 $e65 (not $e81))
- (or $e38 (not $e81) (not $e69))
- (or $e80 (not $e84) $e36)
- (or (not $e46) (not $e63) $e33)
- (or (not $e78) (not $e61) (not $e84))
- (or $e50 (not $e35) (not $e52))
- (or (not $e32) (not $e77) (not $e63))
- (or $e66 $e65 (not $e84))
- (or $e72 (not $e53) $e42)
- (or $e44 (not $e60) $e78)
- (or (not $e61) (not $e34) $e53)
- (or (not $e49) (not $e40) $e79)
- (or $e81 $e42 (not $e44))
- (or $e37 (not $e74) $e51)
- (or (not $e47) (not $e57) $e72)
- (or (not $e34) (not $e52) (not $e62))
- (or $e58 (not $e56) $e72)
- (or $e43 $e34 (not $e62))
- (or (not $e50) (not $e75) (not $e42))
- (or $e61 $e39 (not $e73))
- (or $e34 (not $e50) $e78)
- (or $e46 $e68 (not $e37))
- (or $e79 (not $e78) (not $e31))
-))
-$e85
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-