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/regress0/bv/fuzz30.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/regress0/bv/fuzz30.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz30.smt | 72 |
1 files changed, 0 insertions, 72 deletions
diff --git a/test/regress/regress0/bv/fuzz30.smt b/test/regress/regress0/bv/fuzz30.smt deleted file mode 100644 index 494cde3a3..000000000 --- a/test/regress/regress0/bv/fuzz30.smt +++ /dev/null @@ -1,72 +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 bv4[4]) -(let (?e5 bv9[4]) -(let (?e6 (bvnand ?e4 v0)) -(let (?e7 (bvsub v0 v1)) -(let (?e8 (bvmul v2 v1)) -(let (?e9 (bvand ?e8 v1)) -(let (?e10 (bvneg ?e8)) -(let (?e11 (bvxor ?e9 ?e10)) -(let (?e12 (ite (= bv1[1] (extract[0:0] ?e11)) v1 v0)) -(let (?e13 (bvand ?e7 v1)) -(let (?e14 (ite (bvslt ?e12 ?e4) bv1[1] bv0[1])) -(let (?e15 (ite (distinct ?e4 ?e6) bv1[1] bv0[1])) -(let (?e16 (bvlshr ?e9 ?e5)) -(let (?e17 (repeat[2] ?e14)) -(let (?e18 (ite (bvsge ?e11 ?e8) bv1[1] bv0[1])) -(let (?e19 (ite (bvslt (sign_extend[2] ?e17) v3) bv1[1] bv0[1])) -(flet ($e20 (bvuge ?e16 ?e12)) -(flet ($e21 (bvsgt ?e11 (sign_extend[3] ?e15))) -(flet ($e22 (bvsle (zero_extend[2] ?e17) ?e8)) -(flet ($e23 (= ?e6 ?e5)) -(flet ($e24 (bvslt ?e11 (zero_extend[3] ?e14))) -(flet ($e25 (bvslt ?e9 ?e8)) -(flet ($e26 (bvugt (sign_extend[3] ?e15) ?e6)) -(flet ($e27 (bvsge ?e10 v3)) -(flet ($e28 (bvsge ?e5 v1)) -(flet ($e29 (bvult ?e6 ?e16)) -(flet ($e30 (bvugt ?e7 ?e16)) -(flet ($e31 (bvsge ?e11 ?e7)) -(flet ($e32 (bvugt ?e9 ?e13)) -(flet ($e33 (distinct ?e5 ?e16)) -(flet ($e34 (bvuge ?e6 (zero_extend[2] ?e17))) -(flet ($e35 (bvuge ?e9 ?e7)) -(flet ($e36 (bvult v3 v0)) -(flet ($e37 (bvsgt v2 ?e16)) -(flet ($e38 (bvult ?e11 v1)) -(flet ($e39 (bvuge v2 v1)) -(flet ($e40 (bvugt ?e12 (zero_extend[2] ?e17))) -(flet ($e41 (bvsle (zero_extend[3] ?e15) ?e4)) -(flet ($e42 (= ?e8 ?e9)) -(flet ($e43 (distinct ?e10 ?e8)) -(flet ($e44 (bvsge v3 ?e8)) -(flet ($e45 (bvule ?e9 (sign_extend[3] ?e18))) -(flet ($e46 (bvsge ?e13 (sign_extend[3] ?e18))) -(flet ($e47 (distinct (sign_extend[3] ?e19) ?e10)) -(flet ($e48 -(and - (or $e37 $e24 (not $e32)) - (or (not $e27) (not $e35) (not $e24)) - (or (not $e32) (not $e35) (not $e30)) - (or (not $e36) $e35 $e41) - (or (not $e45) $e23 (not $e37)) - (or $e45 (not $e20) $e28) - (or $e29 $e37 $e20) - (or (not $e21) $e25 $e22) - (or (not $e24) (not $e40) (not $e46)) - (or (not $e47) (not $e22) (not $e33)) - (or $e41 $e40 (not $e43)) - (or $e25 (not $e38) $e28) - (or $e22 (not $e28) $e44) - (or (not $e40) $e37 (not $e31)) -)) -$e48 -)))))))))))))))))))))))))))))))))))))))))))))) - |