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