diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz27.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz27.smt | 143 |
1 files changed, 0 insertions, 143 deletions
diff --git a/test/regress/regress0/bv/fuzz27.smt b/test/regress/regress0/bv/fuzz27.smt deleted file mode 100644 index 786a6aa9c..000000000 --- a/test/regress/regress0/bv/fuzz27.smt +++ /dev/null @@ -1,143 +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])) -:formula -(let (?e4 bv8[4]) -(let (?e5 bv9[4]) -(let (?e6 bv11[4]) -(let (?e7 (ite (bvslt ?e6 ?e5) bv1[1] bv0[1])) -(let (?e8 (bvor (sign_extend[3] ?e7) ?e4)) -(let (?e9 (ite (bvslt v0 ?e6) bv1[1] bv0[1])) -(let (?e10 (bvxnor ?e8 ?e5)) -(let (?e11 (zero_extend[0] v3)) -(let (?e12 (bvxnor (sign_extend[3] ?e7) ?e6)) -(let (?e13 (bvnot v3)) -(let (?e14 (ite (bvugt ?e12 v3) bv1[1] bv0[1])) -(let (?e15 (bvcomp ?e10 ?e12)) -(let (?e16 (bvxnor v3 ?e6)) -(let (?e17 (rotate_right[0] ?e9)) -(let (?e18 (bvneg ?e17)) -(let (?e19 (bvor (zero_extend[3] ?e7) ?e10)) -(let (?e20 (bvnot ?e17)) -(let (?e21 (ite (bvsle ?e4 ?e12) bv1[1] bv0[1])) -(let (?e22 (bvxnor ?e9 ?e15)) -(let (?e23 (bvadd v1 ?e19)) -(let (?e24 (bvashr ?e17 ?e22)) -(let (?e25 (bvnor (sign_extend[3] ?e15) ?e16)) -(let (?e26 (ite (bvule ?e11 ?e4) bv1[1] bv0[1])) -(let (?e27 (ite (bvsle ?e4 (sign_extend[3] ?e9)) bv1[1] bv0[1])) -(let (?e28 (ite (bvuge ?e23 v3) bv1[1] bv0[1])) -(let (?e29 (ite (bvsgt ?e11 (sign_extend[3] ?e7)) bv1[1] bv0[1])) -(let (?e30 (ite (= bv1[1] (extract[0:0] ?e29)) (sign_extend[3] ?e24) ?e6)) -(let (?e31 (ite (bvugt v1 ?e16) bv1[1] bv0[1])) -(let (?e32 (bvand v2 ?e23)) -(flet ($e33 (bvugt (sign_extend[3] ?e29) ?e11)) -(flet ($e34 (distinct ?e20 ?e18)) -(flet ($e35 (bvult ?e19 ?e30)) -(flet ($e36 (bvult ?e11 ?e25)) -(flet ($e37 (bvuge (zero_extend[3] ?e14) ?e4)) -(flet ($e38 (= ?e15 ?e17)) -(flet ($e39 (bvslt (sign_extend[3] ?e17) ?e16)) -(flet ($e40 (bvult (zero_extend[3] ?e24) ?e30)) -(flet ($e41 (distinct ?e13 ?e12)) -(flet ($e42 (bvslt ?e16 ?e11)) -(flet ($e43 (bvsle ?e12 (sign_extend[3] ?e22))) -(flet ($e44 (bvuge ?e15 ?e26)) -(flet ($e45 (bvsgt ?e19 (zero_extend[3] ?e18))) -(flet ($e46 (bvslt ?e30 ?e23)) -(flet ($e47 (bvsgt ?e32 ?e8)) -(flet ($e48 (bvule ?e10 (sign_extend[3] ?e31))) -(flet ($e49 (bvslt (sign_extend[3] ?e15) v0)) -(flet ($e50 (bvsgt (sign_extend[3] ?e14) v1)) -(flet ($e51 (bvslt v3 ?e23)) -(flet ($e52 (distinct ?e6 (sign_extend[3] ?e20))) -(flet ($e53 (bvugt v2 ?e32)) -(flet ($e54 (bvsge ?e18 ?e15)) -(flet ($e55 (bvsgt ?e32 (sign_extend[3] ?e20))) -(flet ($e56 (bvuge ?e21 ?e21)) -(flet ($e57 (bvule ?e22 ?e14)) -(flet ($e58 (= ?e28 ?e17)) -(flet ($e59 (bvslt (sign_extend[3] ?e27) ?e19)) -(flet ($e60 (bvult ?e24 ?e20)) -(flet ($e61 (bvugt ?e5 (sign_extend[3] ?e20))) -(flet ($e62 (bvsle ?e26 ?e28)) -(flet ($e63 (bvule ?e31 ?e26)) -(flet ($e64 (bvuge ?e21 ?e18)) -(flet ($e65 (bvuge (sign_extend[3] ?e24) ?e13)) -(flet ($e66 (bvsge ?e23 ?e16)) -(flet ($e67 (bvugt (zero_extend[3] ?e17) ?e12)) -(flet ($e68 (bvsgt ?e30 v1)) -(flet ($e69 (bvule ?e16 ?e30)) -(flet ($e70 (bvult ?e22 ?e17)) -(flet ($e71 (bvult v1 ?e19)) -(flet ($e72 (bvuge ?e24 ?e28)) -(flet ($e73 (bvsge ?e11 (sign_extend[3] ?e22))) -(flet ($e74 (bvsgt ?e7 ?e18)) -(flet ($e75 (distinct ?e32 ?e16)) -(flet ($e76 (bvsge v3 ?e16)) -(flet ($e77 (bvsle (sign_extend[3] ?e15) v1)) -(flet ($e78 (bvule ?e8 ?e23)) -(flet ($e79 (bvsge ?e30 (sign_extend[3] ?e14))) -(flet ($e80 (bvsge ?e4 (zero_extend[3] ?e18))) -(flet ($e81 (bvslt v1 ?e4)) -(flet ($e82 (bvslt ?e5 v3)) -(flet ($e83 (distinct ?e29 ?e7)) -(flet ($e84 (bvult v1 ?e32)) -(flet ($e85 (bvslt (zero_extend[3] ?e27) ?e5)) -(flet ($e86 (bvslt v0 (zero_extend[3] ?e17))) -(flet ($e87 (bvsge (sign_extend[3] ?e24) ?e8)) -(flet ($e88 (bvslt ?e16 ?e12)) -(flet ($e89 (bvsge ?e29 ?e18)) -(flet ($e90 (bvsge v1 (sign_extend[3] ?e26))) -(flet ($e91 (bvsle (sign_extend[3] ?e26) ?e25)) -(flet ($e92 (bvsgt v0 ?e32)) -(flet ($e93 (bvult ?e17 ?e17)) -(flet ($e94 (distinct v0 ?e11)) -(flet ($e95 (bvsgt ?e4 ?e5)) -(flet ($e96 (bvsge ?e7 ?e18)) -(flet ($e97 (distinct ?e16 ?e32)) -(flet ($e98 (bvslt v3 (sign_extend[3] ?e22))) -(flet ($e99 (bvsge ?e28 ?e9)) -(flet ($e100 -(and - (or $e96 $e47 $e61) - (or (not $e97) (not $e88) (not $e40)) - (or $e40 (not $e45) $e61) - (or (not $e86) (not $e95) $e82) - (or $e65 $e59 (not $e50)) - (or $e35 (not $e70) (not $e83)) - (or $e40 $e98 (not $e96)) - (or $e84 (not $e87) (not $e95)) - (or (not $e58) $e98 $e41) - (or (not $e64) (not $e46) $e85) - (or $e43 (not $e60) $e89) - (or $e55 (not $e38) (not $e34)) - (or $e35 $e58 (not $e39)) - (or $e87 (not $e47) $e68) - (or $e52 (not $e79) $e35) - (or (not $e67) $e65 $e43) - (or $e60 (not $e71) (not $e84)) - (or (not $e46) $e63 (not $e67)) - (or $e57 $e41 $e88) - (or (not $e60) $e52 $e50) - (or (not $e57) $e88 (not $e99)) - (or $e69 $e45 $e35) - (or (not $e38) (not $e48) $e77) - (or (not $e38) $e60 $e69) - (or (not $e94) (not $e77) $e68) - (or (not $e76) (not $e68) $e97) - (or (not $e75) (not $e43) $e72) - (or (not $e54) $e42 (not $e61)) - (or (not $e89) $e42 $e44) - (or (not $e73) $e68 $e39) - (or $e82 $e69 (not $e89)) - (or (not $e38) (not $e67) $e55) - (or (not $e92) (not $e63) $e99) -)) -$e100 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - |