diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz37.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz37.smt | 122 |
1 files changed, 0 insertions, 122 deletions
diff --git a/test/regress/regress0/bv/fuzz37.smt b/test/regress/regress0/bv/fuzz37.smt deleted file mode 100644 index 98fdfda48..000000000 --- a/test/regress/regress0/bv/fuzz37.smt +++ /dev/null @@ -1,122 +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 bv2[4]) -(let (?e6 bv2[4]) -(let (?e7 (bvlshr v4 v3)) -(let (?e8 (ite (bvugt ?e5 v1) bv1[1] bv0[1])) -(let (?e9 (bvor v3 v1)) -(let (?e10 (bvnot v4)) -(let (?e11 (bvsub v0 ?e6)) -(let (?e12 (bvnor ?e5 (zero_extend[3] ?e8))) -(let (?e13 (bvmul ?e12 v1)) -(let (?e14 (ite (= ?e10 v3) bv1[1] bv0[1])) -(let (?e15 (ite (bvult v0 ?e11) bv1[1] bv0[1])) -(let (?e16 (bvashr ?e9 ?e5)) -(let (?e17 (bvnor v1 ?e11)) -(let (?e18 (bvcomp ?e17 ?e11)) -(let (?e19 (zero_extend[0] ?e13)) -(let (?e20 (bvsub v3 ?e19)) -(let (?e21 (bvshl v4 ?e10)) -(let (?e22 (ite (bvule ?e10 (sign_extend[3] ?e14)) bv1[1] bv0[1])) -(let (?e23 (concat ?e15 ?e15)) -(let (?e24 (rotate_left[0] v1)) -(let (?e25 (bvshl ?e21 v1)) -(let (?e26 (bvnor ?e24 ?e7)) -(let (?e27 (bvand ?e11 v0)) -(let (?e28 (bvlshr ?e20 (zero_extend[3] ?e8))) -(let (?e29 (bvcomp ?e10 v2)) -(flet ($e30 (bvuge (zero_extend[3] ?e14) v2)) -(flet ($e31 (bvult ?e17 ?e12)) -(flet ($e32 (distinct ?e16 ?e17)) -(flet ($e33 (bvuge (zero_extend[3] ?e18) ?e21)) -(flet ($e34 (= ?e20 ?e19)) -(flet ($e35 (bvuge ?e27 (sign_extend[3] ?e18))) -(flet ($e36 (bvult ?e10 ?e27)) -(flet ($e37 (bvugt v3 v1)) -(flet ($e38 (bvuge ?e24 ?e17)) -(flet ($e39 (bvult v1 (sign_extend[2] ?e23))) -(flet ($e40 (bvsle (sign_extend[3] ?e22) ?e5)) -(flet ($e41 (bvult ?e25 ?e5)) -(flet ($e42 (distinct ?e10 ?e16)) -(flet ($e43 (bvugt ?e24 (sign_extend[3] ?e22))) -(flet ($e44 (bvuge (zero_extend[3] ?e8) ?e20)) -(flet ($e45 (bvsgt ?e6 ?e11)) -(flet ($e46 (bvslt v1 ?e26)) -(flet ($e47 (bvsgt v1 ?e16)) -(flet ($e48 (bvsgt ?e7 v3)) -(flet ($e49 (bvugt ?e16 ?e12)) -(flet ($e50 (bvule ?e14 ?e22)) -(flet ($e51 (bvsgt v3 ?e9)) -(flet ($e52 (bvugt ?e24 (zero_extend[3] ?e14))) -(flet ($e53 (= v2 (zero_extend[3] ?e22))) -(flet ($e54 (bvuge ?e5 (sign_extend[3] ?e29))) -(flet ($e55 (bvsgt ?e13 ?e16)) -(flet ($e56 (bvsge ?e21 ?e6)) -(flet ($e57 (bvuge ?e11 v4)) -(flet ($e58 (bvslt ?e6 ?e28)) -(flet ($e59 (bvsle (sign_extend[3] ?e29) ?e27)) -(flet ($e60 (bvslt ?e20 ?e24)) -(flet ($e61 (bvsge (zero_extend[3] ?e14) ?e28)) -(flet ($e62 (bvsle ?e20 ?e13)) -(flet ($e63 (bvsge ?e25 ?e21)) -(flet ($e64 (distinct (sign_extend[3] ?e29) v4)) -(flet ($e65 (distinct (zero_extend[3] ?e29) ?e10)) -(flet ($e66 (bvsle (zero_extend[2] ?e23) ?e27)) -(flet ($e67 (bvsgt ?e17 v3)) -(flet ($e68 (bvule v1 (sign_extend[3] ?e18))) -(flet ($e69 (bvule ?e25 ?e7)) -(flet ($e70 (bvuge v1 ?e28)) -(flet ($e71 (bvugt v2 ?e9)) -(flet ($e72 (distinct (zero_extend[3] ?e29) ?e6)) -(flet ($e73 (bvslt v1 ?e13)) -(flet ($e74 (bvuge (zero_extend[3] ?e14) ?e12)) -(flet ($e75 (bvult (zero_extend[3] ?e8) v4)) -(flet ($e76 (bvslt v0 ?e19)) -(flet ($e77 (bvule ?e29 ?e22)) -(flet ($e78 (distinct (sign_extend[3] ?e14) ?e16)) -(flet ($e79 (bvule ?e27 ?e20)) -(flet ($e80 (bvsgt v0 (zero_extend[2] ?e23))) -(flet ($e81 (bvule ?e21 v2)) -(flet ($e82 (bvsge ?e28 v3)) -(flet ($e83 (distinct (sign_extend[3] ?e8) ?e13)) -(flet ($e84 (bvule (sign_extend[3] ?e15) v2)) -(flet ($e85 -(and - (or $e32 $e81 (not $e60)) - (or (not $e60) $e69 $e50) - (or (not $e53) (not $e67) $e51) - (or $e30 $e62 $e78) - (or $e37 $e65 (not $e81)) - (or $e38 (not $e81) (not $e69)) - (or $e80 (not $e84) $e36) - (or (not $e46) (not $e63) $e33) - (or (not $e78) (not $e61) (not $e84)) - (or $e50 (not $e35) (not $e52)) - (or (not $e32) (not $e77) (not $e63)) - (or $e66 $e65 (not $e84)) - (or $e72 (not $e53) $e42) - (or $e44 (not $e60) $e78) - (or (not $e61) (not $e34) $e53) - (or (not $e49) (not $e40) $e79) - (or $e81 $e42 (not $e44)) - (or $e37 (not $e74) $e51) - (or (not $e47) (not $e57) $e72) - (or (not $e34) (not $e52) (not $e62)) - (or $e58 (not $e56) $e72) - (or $e43 $e34 (not $e62)) - (or (not $e50) (not $e75) (not $e42)) - (or $e61 $e39 (not $e73)) - (or $e34 (not $e50) $e78) - (or $e46 $e68 (not $e37)) - (or $e79 (not $e78) (not $e31)) -)) -$e85 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - |