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/fuzz22.delta01.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/fuzz22.delta01.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz22.delta01.smt | 58 |
1 files changed, 0 insertions, 58 deletions
diff --git a/test/regress/regress0/bv/fuzz22.delta01.smt b/test/regress/regress0/bv/fuzz22.delta01.smt deleted file mode 100644 index a1ef9e444..000000000 --- a/test/regress/regress0/bv/fuzz22.delta01.smt +++ /dev/null @@ -1,58 +0,0 @@ -(benchmark fuzzsmt -:logic QF_BV -:extrafuns ((v3 BitVec[4])) -:extrafuns ((v0 BitVec[4])) -:extrafuns ((v1 BitVec[4])) -:extrafuns ((v2 BitVec[4])) -:extrafuns ((v4 BitVec[4])) -:status sat -:formula -(flet ($n1 true) -(let (?n2 bv12[4]) -(flet ($n3 (bvuge ?n2 v2)) -(flet ($n4 (not $n3)) -(flet ($n5 false) -(let (?n6 bv0[4]) -(let (?n7 (bvnot v0)) -(let (?n8 (bvlshr v1 ?n7)) -(let (?n9 (bvneg ?n8)) -(flet ($n10 (= ?n6 ?n9)) -(flet ($n11 (not $n10)) -(flet ($n12 (or $n5 $n10 $n11)) -(let (?n13 (bvnot v2)) -(let (?n14 (bvcomp ?n2 v0)) -(let (?n15 (zero_extend[3] ?n14)) -(let (?n16 (bvxnor ?n13 ?n15)) -(flet ($n17 (distinct v2 ?n16)) -(let (?n18 bv1[1]) -(flet ($n19 (bvsgt v0 ?n13)) -(let (?n20 bv0[1]) -(let (?n21 (ite $n19 ?n18 ?n20)) -(flet ($n22 (= ?n18 ?n21)) -(flet ($n23 (bvsge v1 ?n6)) -(let (?n24 (ite $n23 ?n18 ?n20)) -(let (?n25 (zero_extend[3] ?n24)) -(let (?n26 (ite $n22 ?n25 ?n13)) -(flet ($n27 (bvsge ?n8 ?n26)) -(flet ($n28 (not $n27)) -(flet ($n29 (or $n5 $n17 $n28)) -(flet ($n30 (bvule ?n2 ?n9)) -(let (?n31 (ite $n30 ?n18 ?n20)) -(let (?n32 (sign_extend[3] ?n31)) -(flet ($n33 (bvsle ?n32 ?n16)) -(flet ($n34 (not $n33)) -(let (?n35 (bvxor v0 v4)) -(flet ($n36 (bvugt ?n8 ?n35)) -(let (?n37 (bvneg ?n13)) -(flet ($n38 (bvslt ?n37 v4)) -(let (?n39 (ite $n38 ?n18 ?n20)) -(flet ($n40 (distinct ?n24 ?n39)) -(let (?n41 (bvlshr ?n8 v3)) -(flet ($n42 (bvslt ?n41 ?n9)) -(flet ($n43 (or $n5 $n40 $n42)) -(flet ($n44 (bvsle ?n7 ?n13)) -(flet ($n45 (bvsle ?n6 ?n41)) -(flet ($n46 (or $n5 $n44 $n45)) -(flet ($n47 (and $n4 $n12 $n29 $n34 $n36 $n43 $n46)) -$n47 -)))))))))))))))))))))))))))))))))))))))))))))))) |