diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz02.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz02.smt | 122 |
1 files changed, 0 insertions, 122 deletions
diff --git a/test/regress/regress0/bv/fuzz02.smt b/test/regress/regress0/bv/fuzz02.smt deleted file mode 100644 index 41b616ef0..000000000 --- a/test/regress/regress0/bv/fuzz02.smt +++ /dev/null @@ -1,122 +0,0 @@ -(benchmark fuzzsmt -:logic QF_BV -:status sat -:extrafuns ((v0 BitVec[3])) -:extrafuns ((v1 BitVec[12])) -:extrafuns ((v2 BitVec[9])) -:formula -(let (?e3 bv10[9]) -(let (?e4 (extract[6:6] ?e3)) -(let (?e5 (ite (bvult v2 v2) bv1[1] bv0[1])) -(let (?e6 (ite (bvsgt ?e4 ?e4) bv1[1] bv0[1])) -(let (?e7 (sign_extend[5] ?e6)) -(let (?e8 (concat ?e7 ?e5)) -(let (?e9 (bvcomp ?e8 (zero_extend[1] ?e7))) -(let (?e10 (ite (bvule ?e7 (zero_extend[5] ?e9)) bv1[1] bv0[1])) -(let (?e11 (bvadd (sign_extend[2] ?e10) v0)) -(let (?e12 (extract[1:0] v0)) -(let (?e13 (ite (bvslt ?e12 ?e12) bv1[1] bv0[1])) -(let (?e14 (ite (bvult ?e7 (sign_extend[4] ?e12)) bv1[1] bv0[1])) -(let (?e15 (bvlshr (sign_extend[8] ?e4) v2)) -(let (?e16 (repeat[2] v0)) -(let (?e17 (rotate_right[4] ?e15)) -(let (?e18 (bvxor ?e14 ?e14)) -(let (?e19 (bvand v2 (sign_extend[7] ?e12))) -(let (?e20 (bvnot v1)) -(flet ($e21 (= ?e15 ?e3)) -(flet ($e22 (= (sign_extend[6] ?e9) ?e8)) -(flet ($e23 (= ?e6 ?e4)) -(flet ($e24 (= ?e11 (zero_extend[2] ?e13))) -(flet ($e25 (= v0 (zero_extend[2] ?e13))) -(flet ($e26 (= (sign_extend[1] ?e4) ?e12)) -(flet ($e27 (= ?e15 ?e3)) -(flet ($e28 (= ?e3 ?e19)) -(flet ($e29 (= (zero_extend[8] ?e14) ?e15)) -(flet ($e30 (= v0 (sign_extend[2] ?e6))) -(flet ($e31 (= ?e11 (sign_extend[2] ?e4))) -(flet ($e32 (= ?e7 (zero_extend[5] ?e6))) -(flet ($e33 (= ?e5 ?e5)) -(flet ($e34 (= (zero_extend[8] ?e6) v2)) -(flet ($e35 (= ?e20 (zero_extend[3] ?e3))) -(flet ($e36 (= (zero_extend[8] ?e4) ?e15)) -(flet ($e37 (= ?e3 (sign_extend[8] ?e5))) -(flet ($e38 (= (sign_extend[11] ?e9) v1)) -(flet ($e39 (= (zero_extend[1] ?e9) ?e12)) -(flet ($e40 (= (sign_extend[6] v0) ?e15)) -(flet ($e41 (= ?e7 (zero_extend[5] ?e14))) -(flet ($e42 (= ?e6 ?e14)) -(flet ($e43 (= ?e16 (zero_extend[5] ?e4))) -(flet ($e44 (= (zero_extend[8] ?e9) v2)) -(flet ($e45 (= v1 (zero_extend[11] ?e5))) -(flet ($e46 (= ?e8 (zero_extend[6] ?e4))) -(flet ($e47 (= (sign_extend[1] ?e13) ?e12)) -(flet ($e48 (= (zero_extend[11] ?e18) v1)) -(flet ($e49 (= (zero_extend[11] ?e5) v1)) -(flet ($e50 (= ?e15 (sign_extend[8] ?e4))) -(flet ($e51 (= ?e13 ?e14)) -(flet ($e52 (= (zero_extend[2] ?e5) ?e11)) -(flet ($e53 (= (sign_extend[11] ?e9) v1)) -(flet ($e54 (= ?e8 (sign_extend[6] ?e5))) -(flet ($e55 (= (sign_extend[7] ?e12) v2)) -(flet ($e56 (= ?e20 (sign_extend[3] ?e15))) -(flet ($e57 (= ?e15 (sign_extend[6] ?e11))) -(flet ($e58 (= ?e6 ?e4)) -(flet ($e59 (= (sign_extend[8] ?e10) v2)) -(flet ($e60 (= (zero_extend[8] ?e10) ?e19)) -(flet ($e61 (= ?e9 ?e6)) -(flet ($e62 (= ?e11 (sign_extend[2] ?e9))) -(flet ($e63 (= v2 (zero_extend[8] ?e18))) -(flet ($e64 (= (sign_extend[2] ?e10) ?e11)) -(flet ($e65 (= ?e5 ?e5)) -(flet ($e66 (= (zero_extend[3] ?e16) ?e17)) -(flet ($e67 (if_then_else $e34 $e37 $e22)) -(flet ($e68 (xor $e61 $e63)) -(flet ($e69 (iff $e55 $e53)) -(flet ($e70 (not $e51)) -(flet ($e71 (or $e70 $e56)) -(flet ($e72 (or $e23 $e54)) -(flet ($e73 (or $e43 $e39)) -(flet ($e74 (implies $e58 $e32)) -(flet ($e75 (and $e21 $e59)) -(flet ($e76 (implies $e33 $e38)) -(flet ($e77 (and $e41 $e57)) -(flet ($e78 (if_then_else $e77 $e74 $e64)) -(flet ($e79 (iff $e36 $e52)) -(flet ($e80 (or $e29 $e25)) -(flet ($e81 (iff $e68 $e62)) -(flet ($e82 (xor $e78 $e76)) -(flet ($e83 (xor $e66 $e69)) -(flet ($e84 (or $e45 $e27)) -(flet ($e85 (xor $e83 $e79)) -(flet ($e86 (if_then_else $e72 $e72 $e65)) -(flet ($e87 (iff $e28 $e75)) -(flet ($e88 (if_then_else $e26 $e73 $e47)) -(flet ($e89 (xor $e60 $e60)) -(flet ($e90 (xor $e49 $e42)) -(flet ($e91 (iff $e44 $e48)) -(flet ($e92 (and $e71 $e80)) -(flet ($e93 (not $e88)) -(flet ($e94 (iff $e35 $e35)) -(flet ($e95 (iff $e81 $e90)) -(flet ($e96 (xor $e89 $e85)) -(flet ($e97 (xor $e82 $e94)) -(flet ($e98 (or $e92 $e40)) -(flet ($e99 (implies $e93 $e24)) -(flet ($e100 (if_then_else $e46 $e31 $e50)) -(flet ($e101 (or $e86 $e97)) -(flet ($e102 (and $e101 $e67)) -(flet ($e103 (if_then_else $e87 $e96 $e30)) -(flet ($e104 (not $e100)) -(flet ($e105 (xor $e91 $e104)) -(flet ($e106 (if_then_else $e84 $e102 $e84)) -(flet ($e107 (implies $e106 $e98)) -(flet ($e108 (implies $e107 $e103)) -(flet ($e109 (or $e95 $e95)) -(flet ($e110 (implies $e108 $e109)) -(flet ($e111 (not $e99)) -(flet ($e112 (or $e110 $e105)) -(flet ($e113 (or $e112 $e112)) -(flet ($e114 (xor $e111 $e113)) -$e114 -))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - |