diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz24.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz24.smt | 203 |
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 -))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - |