diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz24.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz24.smt | 203 |
1 files changed, 203 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz24.smt b/test/regress/regress0/bv/fuzz24.smt new file mode 100644 index 000000000..0f722108a --- /dev/null +++ b/test/regress/regress0/bv/fuzz24.smt @@ -0,0 +1,203 @@ +(benchmark fuzzsmt +:logic QF_BV +:status unknown +: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 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |