1 files changed, 0 insertions, 158 deletions
diff --git a/test/regress/regress0/bv/fuzz22.smt b/test/regress/regress0/bv/fuzz22.smt
deleted file mode 100644
index 5aad8f7f7..000000000
--- a/test/regress/regress0/bv/fuzz22.smt
+++ /dev/null
@@ -1,158 +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 bv12[4])
-(let (?e6 bv12[4])
-(let (?e7 (ite (= bv1[1] (extract[2:2] v0)) v1 v2))
-(let (?e8 (rotate_left[1] v0))
-(let (?e9 (bvnot ?e8))
-(let (?e10 (bvnot v2))
-(let (?e11 (bvcomp v0 ?e5))
-(let (?e12 (bvashr v1 ?e10))
-(let (?e13 (repeat[1] ?e9))
-(let (?e14 (zero_extend[0] ?e6))
-(let (?e15 (ite (bvsge ?e7 ?e14) bv1[1] bv0[1]))
-(let (?e16 (bvlshr ?e12 ?e9))
-(let (?e17 (bvxor v4 ?e8))
-(let (?e18 (bvneg ?e10))
-(let (?e19 (bvnor ?e14 ?e5))
-(let (?e20 (bvneg ?e16))
-(let (?e21 (ite (bvsgt ?e8 ?e10) bv1[1] bv0[1]))
-(let (?e22 (ite (bvslt ?e18 v4) bv1[1] bv0[1]))
-(let (?e23 (ite (= bv1[1] (extract[0:0] ?e21)) (zero_extend[3] ?e15) ?e10))
-(let (?e24 (bvshl ?e6 ?e14))
-(let (?e25 (rotate_left[0] ?e10))
-(let (?e26 (ite (bvult ?e25 ?e17) bv1[1] bv0[1]))
-(let (?e27 (ite (bvult v1 ?e9) bv1[1] bv0[1]))
-(let (?e28 (zero_extend[0] ?e19))
-(let (?e29 (bvor ?e10 ?e9))
-(let (?e30 (ite (bvule ?e6 ?e20) bv1[1] bv0[1]))
-(let (?e31 (bvxor v2 ?e6))
-(let (?e32 (bvmul ?e13 (zero_extend[3] ?e21)))
-(let (?e33 (bvnot ?e27))
-(let (?e34 (sign_extend[0] ?e16))
-(let (?e35 (bvashr ?e16 ?e13))
-(let (?e36 (bvnot ?e7))
-(let (?e37 (bvxnor ?e25 (zero_extend[3] ?e11)))
-(let (?e38 (rotate_right[3] ?e37))
-(let (?e39 (ite (bvult ?e14 (sign_extend[3] ?e33)) bv1[1] bv0[1]))
-(let (?e40 (bvxor ?e34 ?e6))
-(let (?e41 (bvlshr ?e16 v3))
-(flet ($e42 (bvult ?e14 ?e6))
-(flet ($e43 (distinct ?e22 ?e15))
-(flet ($e44 (bvslt v0 ?e7))
-(flet ($e45 (= ?e7 ?e37))
-(flet ($e46 (bvslt ?e13 ?e9))
-(flet ($e47 (bvsge ?e32 (sign_extend[3] ?e39)))
-(flet ($e48 (bvuge ?e37 ?e32))
-(flet ($e49 (bvsgt ?e36 ?e17))
-(flet ($e50 (bvslt v3 ?e7))
-(flet ($e51 (bvult ?e24 ?e16))
-(flet ($e52 (bvuge ?e16 (zero_extend[3] ?e39)))
-(flet ($e53 (= v3 ?e38))
-(flet ($e54 (bvult ?e8 (sign_extend[3] ?e21)))
-(flet ($e55 (= ?e37 v4))
-(flet ($e56 (bvslt v2 (sign_extend[3] ?e30)))
-(flet ($e57 (bvule ?e37 (zero_extend[3] ?e26)))
-(flet ($e58 (bvult v3 ?e19))
-(flet ($e59 (bvslt ?e10 (sign_extend[3] ?e15)))
-(flet ($e60 (= ?e6 ?e12))
-(flet ($e61 (bvule ?e28 (sign_extend[3] ?e39)))
-(flet ($e62 (= ?e17 ?e35))
-(flet ($e63 (bvslt ?e41 (zero_extend[3] ?e21)))
-(flet ($e64 (bvugt v0 ?e13))
-(flet ($e65 (bvuge ?e14 v1))
-(flet ($e66 (bvuge (sign_extend[3] ?e26) ?e18))
-(flet ($e67 (bvult v3 ?e29))
-(flet ($e68 (bvule ?e10 v1))
-(flet ($e69 (bvule ?e19 ?e13))
-(flet ($e70 (= ?e23 ?e12))
-(flet ($e71 (bvslt ?e17 ?e28))
-(flet ($e72 (bvule (zero_extend[3] ?e33) ?e16))
-(flet ($e73 (bvsge ?e23 ?e8))
-(flet ($e74 (bvsle ?e9 ?e10))
-(flet ($e75 (bvslt ?e41 ?e20))
-(flet ($e76 (bvsle (sign_extend[3] ?e30) ?e38))
-(flet ($e77 (bvuge ?e41 (sign_extend[3] ?e11)))
-(flet ($e78 (bvsle ?e24 ?e41))
-(flet ($e79 (bvuge ?e25 (sign_extend[3] ?e21)))
-(flet ($e80 (bvuge ?e24 ?e9))
-(flet ($e81 (bvuge ?e6 v2))
-(flet ($e82 (bvsge ?e13 (sign_extend[3] ?e30)))
-(flet ($e83 (bvsge ?e5 (sign_extend[3] ?e39)))
-(flet ($e84 (bvsgt ?e7 (sign_extend[3] ?e27)))
-(flet ($e85 (bvsle ?e23 ?e14))
-(flet ($e86 (bvult ?e8 (zero_extend[3] ?e39)))
-(flet ($e87 (bvugt ?e25 v2))
-(flet ($e88 (bvslt ?e12 (sign_extend[3] ?e11)))
-(flet ($e89 (bvult v3 ?e14))
-(flet ($e90 (distinct ?e8 ?e38))
-(flet ($e91 (bvslt ?e10 ?e9))
-(flet ($e92 (bvslt ?e32 ?e8))
-(flet ($e93 (bvsle v0 (sign_extend[3] ?e39)))
-(flet ($e94 (= v1 ?e32))
-(flet ($e95 (bvule ?e30 ?e15))
-(flet ($e96 (bvult (sign_extend[3] ?e33) ?e9))
-(flet ($e97 (bvsge ?e16 ?e23))
-(flet ($e98 (bvsge ?e40 (sign_extend[3] ?e21)))
-(flet ($e99 (bvuge ?e14 ?e31))
-(flet ($e100 (bvslt ?e40 ?e9))
-(flet ($e101 (bvsge ?e41 ?e6))
-(flet ($e102 (bvsgt ?e24 ?e24))
-(flet ($e103 (distinct ?e37 v2))
-(flet ($e104 (distinct ?e35 v3))
-(flet ($e105 (distinct v1 (zero_extend[3] ?e21)))
-(flet ($e106 (bvsgt ?e9 v1))
-(flet ($e107 (bvugt ?e10 ?e37))
-(flet ($e108 (bvsgt ?e8 (zero_extend[3] ?e21)))
-(flet ($e109 (bvule (sign_extend[3] ?e27) ?e16))
-(flet ($e110 (= ?e19 ?e20))
-(flet ($e111 (bvslt (sign_extend[3] ?e22) ?e38))
-(flet ($e112 (bvugt ?e34 ?e17))
-(flet ($e113 
-(and
- (or (not $e110) $e45 $e110)
- (or $e45 $e103 (not $e97))
- (or (not $e58) (not $e78) (not $e74))
- (or (not $e42) (not $e55) (not $e70))
- (or $e101 (not $e66) $e107)
- (or $e50 $e98 (not $e86))
- (or $e74 (not $e76) (not $e106))
- (or $e93 (not $e79) (not $e49))
- (or (not $e80) (not $e98) (not $e108))
- (or (not $e47) (not $e103) $e55)
- (or (not $e112) (not $e88) (not $e108))
- (or $e75 (not $e43) $e45)
- (or (not $e54) (not $e83) (not $e62))
- (or (not $e45) (not $e56) $e84)
- (or $e43 (not $e73) $e84)
- (or (not $e90) (not $e94) $e72)
- (or (not $e101) $e80 $e91)
- (or (not $e64) $e89 $e71)
- (or $e43 $e100 $e101)
- (or (not $e106) (not $e65) (not $e70))
- (or (not $e47) $e103 (not $e63))
- (or (not $e81) (not $e90) $e55)
- (or $e67 (not $e109) (not $e84))
- (or $e70 $e73 $e67)
- (or $e109 $e85 $e89)
- (or (not $e86) $e75 (not $e70))
- (or $e91 $e109 $e68)
- (or (not $e110) $e102 (not $e106))
- (or (not $e63) (not $e62) $e111)
- (or $e87 (not $e53) (not $e92))
- (or $e99 $e43 (not $e94))
- (or $e69 $e60 $e90)
- (or (not $e53) $e103 (not $e79))
- (or (not $e89) (not $e82) $e64)
- (or $e69 (not $e91) $e103)
-))
-$e113
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-