diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-09-06 15:28:07 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-06 15:28:07 -0700 |
commit | 91a5055015a97935d19b3dbf18062e189268a1f9 (patch) | |
tree | fb1fd19d80fb89d71286b462927540c0648d7551 /test/regress/regress1/decision/error3.smt | |
parent | 7fc142a10140bba5a732237e3adf8fe6729d90e7 (diff) |
Remove SMT1 parser. (#3228)
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).
Fixes #2948 and fixes #1313.
Diffstat (limited to 'test/regress/regress1/decision/error3.smt')
-rw-r--r-- | test/regress/regress1/decision/error3.smt | 138 |
1 files changed, 0 insertions, 138 deletions
diff --git a/test/regress/regress1/decision/error3.smt b/test/regress/regress1/decision/error3.smt deleted file mode 100644 index 36c409f3f..000000000 --- a/test/regress/regress1/decision/error3.smt +++ /dev/null @@ -1,138 +0,0 @@ -(benchmark fuzzsmt -:logic QF_AUFBV -:status unsat -:extrafuns ((v0 BitVec[15])) -:extrafuns ((v1 BitVec[3])) -:extrafuns ((a2 Array[13:3])) -:extrafuns ((a3 Array[16:5])) -:formula -(let (?e4 bv228[11]) -(let (?e5 (ite (bvsgt v1 v1) bv1[1] bv0[1])) -(let (?e6 (ite (bvslt (sign_extend[2] ?e5) v1) bv1[1] bv0[1])) -(let (?e7 (bvnot ?e6)) -(let (?e8 (ite (bvuge v0 (zero_extend[14] ?e6)) bv1[1] bv0[1])) -(let (?e9 (bvmul (zero_extend[10] ?e7) ?e4)) -(let (?e10 (select a2 (zero_extend[12] ?e6))) -(let (?e11 (select a2 (extract[13:1] v0))) -(let (?e12 (select a2 (extract[13:1] v0))) -(let (?e13 (select a2 (zero_extend[2] ?e4))) -(let (?e14 (ite (bvuge ?e9 (zero_extend[10] ?e5)) bv1[1] bv0[1])) -(let (?e15 (repeat[2] ?e7)) -(let (?e16 (bvshl (sign_extend[2] ?e6) ?e11)) -(let (?e17 (bvsmod (zero_extend[8] ?e16) ?e9)) -(let (?e18 (bvudiv (sign_extend[2] ?e6) ?e16)) -(let (?e19 (bvlshr v0 (zero_extend[4] ?e17))) -(let (?e20 (rotate_left[5] ?e4)) -(let (?e21 (ite (= ?e6 ?e5) bv1[1] bv0[1])) -(let (?e22 (ite (bvsgt ?e20 ?e9) bv1[1] bv0[1])) -(let (?e23 (bvor ?e20 (sign_extend[10] ?e14))) -(let (?e24 (bvxnor ?e17 (sign_extend[10] ?e7))) -(let (?e25 (repeat[14] ?e8)) -(let (?e26 (ite (bvsge ?e12 (sign_extend[2] ?e14)) bv1[1] bv0[1])) -(let (?e27 (bvshl ?e13 (zero_extend[2] ?e5))) -(let (?e28 (zero_extend[3] ?e17)) -(let (?e29 (bvxnor ?e22 ?e8)) -(let (?e30 (concat v1 ?e8)) -(let (?e31 (bvsmod (sign_extend[4] ?e24) ?e19)) -(let (?e32 (sign_extend[1] ?e31)) -(let (?e33 (ite (bvult ?e10 (sign_extend[1] ?e15)) bv1[1] bv0[1])) -(flet ($e34 (bvult ?e28 (sign_extend[11] ?e11))) -(flet ($e35 (bvule ?e25 (sign_extend[13] ?e7))) -(flet ($e36 (bvuge (zero_extend[8] ?e12) ?e20)) -(flet ($e37 (bvsgt ?e30 (sign_extend[1] v1))) -(flet ($e38 (= (zero_extend[4] ?e17) v0)) -(flet ($e39 (bvult ?e19 (zero_extend[1] ?e25))) -(flet ($e40 (bvugt ?e24 (zero_extend[8] ?e11))) -(flet ($e41 (bvsle (sign_extend[14] ?e21) ?e31)) -(flet ($e42 (bvsge (zero_extend[2] ?e22) ?e16)) -(flet ($e43 (bvugt ?e33 ?e7)) -(flet ($e44 (bvsle (sign_extend[2] ?e22) ?e10)) -(flet ($e45 (= ?e16 (sign_extend[2] ?e21))) -(flet ($e46 (bvule ?e11 (sign_extend[2] ?e7))) -(flet ($e47 (bvugt v1 (sign_extend[2] ?e29))) -(flet ($e48 (bvsgt ?e22 ?e8)) -(flet ($e49 (bvslt (zero_extend[2] ?e14) ?e12)) -(flet ($e50 (bvule ?e10 (zero_extend[2] ?e26))) -(flet ($e51 (bvslt v0 (zero_extend[4] ?e24))) -(flet ($e52 (bvugt v0 (zero_extend[14] ?e26))) -(flet ($e53 (= (sign_extend[4] ?e4) ?e31)) -(flet ($e54 (bvsle ?e13 (zero_extend[2] ?e29))) -(flet ($e55 (bvult ?e20 (zero_extend[8] ?e12))) -(flet ($e56 (bvugt ?e6 ?e5)) -(flet ($e57 (= ?e28 ?e28)) -(flet ($e58 (bvuge ?e9 (zero_extend[7] ?e30))) -(flet ($e59 (bvsge ?e28 (zero_extend[13] ?e5))) -(flet ($e60 (bvsge ?e20 (sign_extend[8] ?e27))) -(flet ($e61 (bvsgt (sign_extend[12] ?e27) ?e31)) -(flet ($e62 (bvule ?e16 ?e12)) -(flet ($e63 (bvslt ?e27 (sign_extend[2] ?e33))) -(flet ($e64 (bvuge (sign_extend[14] ?e26) ?e31)) -(flet ($e65 (bvsgt v0 (zero_extend[1] ?e28))) -(flet ($e66 (bvsgt ?e24 ?e17)) -(flet ($e67 (bvugt ?e23 (sign_extend[8] ?e18))) -(flet ($e68 (distinct ?e24 (zero_extend[10] ?e22))) -(flet ($e69 (bvuge (sign_extend[2] ?e21) ?e12)) -(flet ($e70 (bvuge ?e17 (zero_extend[8] ?e18))) -(flet ($e71 (distinct (sign_extend[4] ?e17) ?e31)) -(flet ($e72 (bvsge ?e5 ?e6)) -(flet ($e73 (bvsle (zero_extend[10] ?e6) ?e4)) -(flet ($e74 (bvult ?e32 (sign_extend[15] ?e14))) -(flet ($e75 (= ?e6 ?e7)) -(flet ($e76 (bvule ?e31 (zero_extend[12] ?e18))) -(flet ($e77 (bvult ?e23 (zero_extend[9] ?e15))) -(flet ($e78 (iff $e44 $e34)) -(flet ($e79 (iff $e73 $e41)) -(flet ($e80 (xor $e42 $e61)) -(flet ($e81 (and $e66 $e46)) -(flet ($e82 (not $e81)) -(flet ($e83 (or $e62 $e58)) -(flet ($e84 (implies $e82 $e53)) -(flet ($e85 (or $e69 $e50)) -(flet ($e86 (iff $e52 $e76)) -(flet ($e87 (or $e68 $e43)) -(flet ($e88 (iff $e48 $e75)) -(flet ($e89 (or $e74 $e60)) -(flet ($e90 (xor $e64 $e49)) -(flet ($e91 (implies $e59 $e45)) -(flet ($e92 (or $e91 $e80)) -(flet ($e93 (and $e55 $e85)) -(flet ($e94 (or $e40 $e78)) -(flet ($e95 (xor $e51 $e89)) -(flet ($e96 (implies $e87 $e38)) -(flet ($e97 (not $e57)) -(flet ($e98 (or $e97 $e92)) -(flet ($e99 (or $e98 $e84)) -(flet ($e100 (iff $e35 $e95)) -(flet ($e101 (if_then_else $e36 $e47 $e99)) -(flet ($e102 (xor $e37 $e101)) -(flet ($e103 (iff $e86 $e83)) -(flet ($e104 (implies $e63 $e103)) -(flet ($e105 (iff $e102 $e94)) -(flet ($e106 (if_then_else $e56 $e79 $e56)) -(flet ($e107 (iff $e104 $e54)) -(flet ($e108 (or $e77 $e77)) -(flet ($e109 (implies $e70 $e70)) -(flet ($e110 (implies $e105 $e39)) -(flet ($e111 (or $e88 $e106)) -(flet ($e112 (if_then_else $e100 $e65 $e110)) -(flet ($e113 (and $e72 $e67)) -(flet ($e114 (or $e109 $e111)) -(flet ($e115 (implies $e112 $e71)) -(flet ($e116 (not $e108)) -(flet ($e117 (not $e115)) -(flet ($e118 (implies $e114 $e113)) -(flet ($e119 (and $e90 $e117)) -(flet ($e120 (or $e119 $e107)) -(flet ($e121 (if_then_else $e116 $e93 $e96)) -(flet ($e122 (not $e120)) -(flet ($e123 (implies $e121 $e121)) -(flet ($e124 (not $e123)) -(flet ($e125 (if_then_else $e124 $e122 $e118)) -(flet ($e126 (and $e125 (not (= ?e19 bv0[15])))) -(flet ($e127 (and $e126 (not (= ?e19 (bvnot bv0[15]))))) -(flet ($e128 (and $e127 (not (= ?e9 bv0[11])))) -(flet ($e129 (and $e128 (not (= ?e9 (bvnot bv0[11]))))) -(flet ($e130 (and $e129 (not (= ?e16 bv0[3])))) -$e130 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - |