1 files changed, 0 insertions, 203 deletions
diff --git a/test/regress/regress0/bv/fuzz24.smt b/test/regress/regress0/bv/fuzz24.smt
deleted file mode 100644
index a32c1e804..000000000
--- a/test/regress/regress0/bv/fuzz24.smt
+++ /dev/null
@@ -1,203 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_BV
-:status unsat
-:extrafuns ((v0 BitVec[4]))
-:extrafuns ((v1 BitVec[4]))
-:formula
-(let (?e2 bv15[4])
-(let (?e3 bv6[4])
-(let (?e4 bv13[4])
-(let (?e5 bv12[4])
-(let (?e6 (ite (bvslt v1 ?e4) bv1[1] bv0[1]))
-(let (?e7 (bvxor ?e2 ?e5))
-(let (?e8 (sign_extend[1] ?e6))
-(let (?e9 (rotate_right[2] ?e2))
-(let (?e10 (bvshl v1 ?e4))
-(let (?e11 (bvmul v1 (zero_extend[2] ?e8)))
-(let (?e12 (ite (bvugt ?e11 ?e10) bv1[1] bv0[1]))
-(let (?e13 (bvshl ?e4 ?e5))
-(let (?e14 (bvashr (zero_extend[3] ?e12) ?e5))
-(let (?e15 (bvnor ?e4 ?e10))
-(let (?e16 (ite (bvsgt ?e5 ?e13) bv1[1] bv0[1]))
-(let (?e17 (zero_extend[0] ?e11))
-(let (?e18 (bvneg ?e14))
-(let (?e19 (repeat[4] ?e6))
-(let (?e20 (sign_extend[0] ?e9))
-(let (?e21 (bvsub v1 ?e2))
-(let (?e22 (ite (distinct ?e17 (sign_extend[3] ?e16)) bv1[1] bv0[1]))
-(let (?e23 (ite (bvult ?e2 ?e11) bv1[1] bv0[1]))
-(let (?e24 (ite (= bv1[1] (extract[3:3] ?e21)) ?e13 ?e4))
-(let (?e25 (bvand ?e10 ?e24))
-(let (?e26 (ite (= bv1[1] (extract[2:2] ?e14)) (sign_extend[3] ?e6) ?e24))
-(let (?e27 (rotate_left[0] ?e23))
-(let (?e28 (ite (bvule ?e18 (zero_extend[3] ?e22)) bv1[1] bv0[1]))
-(let (?e29 (ite (bvult ?e19 ?e3) bv1[1] bv0[1]))
-(let (?e30 (ite (= bv1[1] (extract[0:0] ?e27)) ?e20 ?e20))
-(let (?e31 (bvneg ?e29))
-(let (?e32 (ite (bvsge ?e10 ?e30) bv1[1] bv0[1]))
-(let (?e33 (bvashr ?e28 ?e27))
-(let (?e34 (bvnot ?e6))
-(let (?e35 (bvnand (zero_extend[3] ?e6) ?e26))
-(let (?e36 (ite (bvsge (sign_extend[3] ?e16) ?e18) bv1[1] bv0[1]))
-(let (?e37 (ite (bvsgt (sign_extend[3] ?e16) ?e30) bv1[1] bv0[1]))
-(let (?e38 (ite (bvsgt ?e31 ?e28) bv1[1] bv0[1]))
-(let (?e39 (ite (bvuge ?e32 ?e22) bv1[1] bv0[1]))
-(let (?e40 (ite (distinct ?e21 (sign_extend[3] ?e27)) bv1[1] bv0[1]))
-(let (?e41 (bvsub ?e15 ?e20))
-(let (?e42 (bvcomp (zero_extend[3] ?e34) ?e25))
-(let (?e43 (bvneg ?e6))
-(let (?e44 (ite (bvslt ?e34 ?e39) bv1[1] bv0[1]))
-(let (?e45 (ite (bvsge ?e31 ?e42) bv1[1] bv0[1]))
-(let (?e46 (bvnand ?e44 ?e32))
-(let (?e47 (ite (bvslt ?e39 ?e6) bv1[1] bv0[1]))
-(let (?e48 (ite (distinct v0 ?e35) bv1[1] bv0[1]))
-(flet ($e49 (bvult ?e13 (sign_extend[2] ?e8)))
-(flet ($e50 (bvsgt ?e39 ?e46))
-(flet ($e51 (bvult ?e38 ?e42))
-(flet ($e52 (bvult ?e14 (zero_extend[3] ?e33)))
-(flet ($e53 (= ?e30 ?e24))
-(flet ($e54 (bvult (zero_extend[3] ?e34) ?e35))
-(flet ($e55 (bvsle ?e41 (zero_extend[3] ?e27)))
-(flet ($e56 (distinct (sign_extend[3] ?e46) v1))
-(flet ($e57 (bvsge (sign_extend[3] ?e12) ?e26))
-(flet ($e58 (bvule ?e13 (sign_extend[3] ?e22)))
-(flet ($e59 (bvsle ?e47 ?e28))
-(flet ($e60 (= (zero_extend[3] ?e47) ?e11))
-(flet ($e61 (bvsge (zero_extend[3] ?e22) ?e9))
-(flet ($e62 (bvult ?e44 ?e37))
-(flet ($e63 (distinct ?e30 ?e19))
-(flet ($e64 (bvugt ?e38 ?e42))
-(flet ($e65 (bvult ?e21 (zero_extend[3] ?e47)))
-(flet ($e66 (= ?e43 ?e34))
-(flet ($e67 (bvult ?e38 ?e38))
-(flet ($e68 (= v0 (sign_extend[3] ?e6)))
-(flet ($e69 (bvsle (zero_extend[3] ?e37) ?e7))
-(flet ($e70 (bvult ?e12 ?e47))
-(flet ($e71 (bvsle (zero_extend[3] ?e6) v1))
-(flet ($e72 (bvsle ?e5 ?e13))
-(flet ($e73 (bvult ?e33 ?e39))
-(flet ($e74 (bvule (sign_extend[3] ?e46) ?e24))
-(flet ($e75 (distinct ?e20 ?e20))
-(flet ($e76 (bvslt ?e17 (zero_extend[3] ?e40)))
-(flet ($e77 (= ?e7 (zero_extend[3] ?e34)))
-(flet ($e78 (bvslt ?e15 ?e41))
-(flet ($e79 (bvsle ?e34 ?e47))
-(flet ($e80 (bvslt (zero_extend[3] ?e36) ?e2))
-(flet ($e81 (bvult (sign_extend[3] ?e37) ?e18))
-(flet ($e82 (bvugt (zero_extend[3] ?e27) ?e18))
-(flet ($e83 (bvugt ?e30 ?e2))
-(flet ($e84 (bvsle (sign_extend[3] ?e12) ?e41))
-(flet ($e85 (bvsgt ?e10 (zero_extend[3] ?e47)))
-(flet ($e86 (bvslt ?e36 ?e38))
-(flet ($e87 (bvsgt ?e25 (sign_extend[3] ?e40)))
-(flet ($e88 (bvsle (sign_extend[3] ?e32) ?e17))
-(flet ($e89 (bvugt (zero_extend[3] ?e6) v0))
-(flet ($e90 (bvugt ?e39 ?e47))
-(flet ($e91 (bvule ?e18 (zero_extend[3] ?e34)))
-(flet ($e92 (bvult ?e43 ?e47))
-(flet ($e93 (bvsge (sign_extend[3] ?e29) ?e20))
-(flet ($e94 (bvsgt ?e13 (zero_extend[3] ?e36)))
-(flet ($e95 (distinct ?e7 ?e7))
-(flet ($e96 (bvslt (zero_extend[3] ?e16) ?e30))
-(flet ($e97 (bvsgt v1 ?e35))
-(flet ($e98 (bvugt ?e22 ?e44))
-(flet ($e99 (bvuge ?e2 ?e5))
-(flet ($e100 (distinct ?e19 (sign_extend[3] ?e39)))
-(flet ($e101 (bvsge ?e4 (sign_extend[3] ?e44)))
-(flet ($e102 (bvsgt ?e6 ?e6))
-(flet ($e103 (bvsge ?e32 ?e12))
-(flet ($e104 (bvsle ?e17 ?e17))
-(flet ($e105 (bvsgt ?e16 ?e34))
-(flet ($e106 (bvsle ?e26 v1))
-(flet ($e107 (bvult ?e13 v0))
-(flet ($e108 (bvugt (zero_extend[3] ?e12) ?e25))
-(flet ($e109 (= ?e27 ?e34))
-(flet ($e110 (bvsge ?e26 (zero_extend[3] ?e28)))
-(flet ($e111 (bvslt ?e22 ?e33))
-(flet ($e112 (= (zero_extend[1] ?e48) ?e8))
-(flet ($e113 (bvslt (sign_extend[3] ?e12) ?e15))
-(flet ($e114 (bvsle ?e11 ?e26))
-(flet ($e115 (bvult ?e38 ?e16))
-(flet ($e116 (bvuge (sign_extend[3] ?e38) ?e4))
-(flet ($e117 (= ?e10 (zero_extend[3] ?e32)))
-(flet ($e118 (bvsgt (zero_extend[3] ?e27) ?e41))
-(flet ($e119 (bvslt ?e10 ?e21))
-(flet ($e120 (= ?e12 ?e44))
-(flet ($e121 (bvugt ?e9 (sign_extend[3] ?e22)))
-(flet ($e122 (bvsle ?e24 (sign_extend[3] ?e29)))
-(flet ($e123 (bvule ?e16 ?e44))
-(flet ($e124 (bvuge (zero_extend[3] ?e48) ?e11))
-(flet ($e125 (bvult ?e39 ?e45))
-(flet ($e126 (bvugt ?e40 ?e16))
-(flet ($e127 (bvsgt ?e9 ?e3))
-(flet ($e128 (bvsgt ?e36 ?e47))
-(flet ($e129 (= (zero_extend[3] ?e22) ?e9))
-(flet ($e130 (bvule ?e11 (zero_extend[3] ?e16)))
-(flet ($e131 (bvslt ?e32 ?e39))
-(flet ($e132 (= (zero_extend[3] ?e38) ?e35))
-(flet ($e133 (bvsge (sign_extend[3] ?e12) ?e7))
-(flet ($e134 (bvult ?e13 ?e14))
-(flet ($e135 (bvuge (sign_extend[1] ?e16) ?e8))
-(flet ($e136 (bvuge ?e9 (zero_extend[3] ?e33)))
-(flet ($e137 (bvule ?e14 ?e10))
-(flet ($e138 (= (sign_extend[3] ?e43) ?e11))
-(flet ($e139 (bvsge ?e39 ?e44))
-(flet ($e140 (bvsle ?e2 ?e18))
-(flet ($e141 (bvslt (sign_extend[3] ?e31) ?e4))
-(flet ($e142 (bvsge ?e9 (zero_extend[3] ?e27)))
-(flet ($e143 (bvsgt ?e18 (zero_extend[3] ?e39)))
-(flet ($e144 (bvsge ?e5 (zero_extend[3] ?e23)))
-(flet ($e145 
-(and
- (or $e117 (not $e78) $e113)
- (or (not $e104) (not $e95) (not $e138))
- (or (not $e105) $e83 (not $e138))
- (or $e121 (not $e67) (not $e106))
- (or (not $e75) $e116 $e131)
- (or $e96 (not $e103) $e120)
- (or $e64 (not $e105) $e86)
- (or $e132 (not $e131) (not $e127))
- (or $e67 (not $e121) $e135)
- (or $e58 (not $e73) (not $e120))
- (or (not $e90) (not $e54) $e119)
- (or $e103 (not $e122) (not $e144))
- (or (not $e141) $e140 $e89)
- (or (not $e73) $e60 $e79)
- (or $e89 $e129 (not $e74))
- (or $e92 (not $e112) (not $e60))
- (or (not $e139) (not $e126) (not $e101))
- (or $e64 $e104 $e101)
- (or (not $e112) $e53 $e91)
- (or (not $e128) $e93 (not $e131))
- (or $e113 (not $e99) (not $e73))
- (or $e86 (not $e70) $e66)
- (or $e131 (not $e125) $e140)
- (or (not $e51) $e140 (not $e102))
- (or $e68 (not $e144) (not $e119))
- (or (not $e132) $e66 $e114)
- (or (not $e137) (not $e73) $e108)
- (or $e86 (not $e57) (not $e75))
- (or (not $e59) (not $e124) (not $e81))
- (or $e130 $e121 $e130)
- (or $e138 (not $e136) (not $e129))
- (or $e108 $e115 $e55)
- (or (not $e130) $e63 $e107)
- (or $e142 $e92 $e65)
- (or (not $e130) $e140 (not $e64))
- (or $e123 (not $e92) (not $e115))
- (or (not $e51) $e54 (not $e77))
- (or $e70 (not $e75) $e129)
- (or $e93 (not $e74) (not $e144))
- (or $e104 $e68 (not $e136))
- (or (not $e92) (not $e126) $e111)
- (or (not $e105) $e91 (not $e52))
- (or (not $e57) (not $e88) (not $e75))
- (or $e127 $e114 $e99)
- (or $e125 (not $e85) $e123)
- (or (not $e90) (not $e49) (not $e112))
- (or $e135 (not $e110) (not $e61))
- (or $e73 $e124 (not $e115))
-))
-$e145
-)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-