diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-14 21:08:28 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-14 21:08:28 +0000 |
commit | c43514fef548f977e88e2986c2f993b975830cc2 (patch) | |
tree | 4362eb7aab0de2376813a07cbc6cc37d781528b0 /test | |
parent | 66033cd2059d817cdeab5adc25f1397532a3fa78 (diff) |
bug fixes in justification heuristic
* remove assert iteSkolemMap gives ite-s (not true with repeatSimp)
* handle a corner case in findSplitter triggered by repeatSimp
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/decision/Makefile.am | 9 | ||||
-rw-r--r-- | test/regress/regress0/decision/error122.delta01.smt | 19 | ||||
-rw-r--r-- | test/regress/regress0/decision/error122.smt | 53 | ||||
-rw-r--r-- | test/regress/regress0/decision/error20.delta01.smt | 19 | ||||
-rw-r--r-- | test/regress/regress0/decision/error20.smt | 66 |
5 files changed, 163 insertions, 3 deletions
diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index b098476fc..de3ccd60a 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -22,11 +22,14 @@ TESTS = \ uflia-error0.smt2 \ uflia-xs-09-16-3-4-1-5.smt \ uflia-xs-09-16-3-4-1-5.delta03.smt \ - aufbv-fuzz01.smt \ - bug347.smt + aufbv-fuzz01.smt \ + bug347.smt \ + error20.smt \ + error20.delta01.smt \ + error122.smt \ + error122.delta01.smt # Incorrect answers: -# aufbv-fuzz01.smt \ # EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/decision/error122.delta01.smt b/test/regress/regress0/decision/error122.delta01.smt new file mode 100644 index 000000000..7c8f930b8 --- /dev/null +++ b/test/regress/regress0/decision/error122.delta01.smt @@ -0,0 +1,19 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:extrafuns ((v0 BitVec[16])) +:extrafuns ((a2 Array[16:7])) +:status sat +:formula +(let (?n1 bv0[7]) +(let (?n2 (store a2 v0 ?n1)) +(let (?n3 bv1[16]) +(let (?n4 (select ?n2 ?n3)) +(flet ($n5 (bvult ?n1 ?n4)) +(let (?n6 bv1[1]) +(let (?n7 bv0[1]) +(let (?n8 (ite $n5 ?n6 ?n7)) +(let (?n9 (sign_extend[15] ?n8)) +(flet ($n10 (distinct v0 ?n9)) +(flet ($n11 (not $n10)) +$n11 +)))))))))))) diff --git a/test/regress/regress0/decision/error122.smt b/test/regress/regress0/decision/error122.smt new file mode 100644 index 000000000..2503ba01e --- /dev/null +++ b/test/regress/regress0/decision/error122.smt @@ -0,0 +1,53 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status unsat +:extrafuns ((v0 BitVec[16])) +:extrafuns ((a1 Array[16:4])) +:extrafuns ((a2 Array[16:7])) +:formula +(let (?e3 bv8911[14]) +(let (?e4 (ite (bvsgt (zero_extend[2] ?e3) v0) bv1[1] bv0[1])) +(let (?e5 (store a2 v0 (extract[13:7] v0))) +(let (?e6 (store a2 (zero_extend[15] ?e4) (zero_extend[6] ?e4))) +(let (?e7 (select ?e5 (zero_extend[2] ?e3))) +(let (?e8 (store ?e5 (sign_extend[2] ?e3) (sign_extend[6] ?e4))) +(let (?e9 (select a1 v0)) +(let (?e10 (store ?e8 (zero_extend[15] ?e4) (extract[6:0] v0))) +(let (?e11 (bvadd (zero_extend[6] ?e4) ?e7)) +(let (?e12 (ite (bvult ?e11 ?e7) bv1[1] bv0[1])) +(let (?e13 (ite (bvult (zero_extend[3] ?e12) ?e9) bv1[1] bv0[1])) +(let (?e14 (bvlshr (sign_extend[12] ?e9) v0)) +(let (?e15 (ite (= bv1[1] (extract[12:12] ?e3)) ?e14 ?e14)) +(flet ($e16 (bvslt ?e15 v0)) +(flet ($e17 (bvult (sign_extend[15] ?e4) ?e14)) +(flet ($e18 (= (sign_extend[15] ?e12) ?e15)) +(flet ($e19 (distinct (sign_extend[15] ?e12) v0)) +(flet ($e20 (bvugt ?e11 ?e11)) +(flet ($e21 (bvule ?e13 ?e13)) +(flet ($e22 (bvslt ?e15 (sign_extend[9] ?e11))) +(flet ($e23 (bvslt (zero_extend[9] ?e11) v0)) +(flet ($e24 (bvult v0 (sign_extend[15] ?e12))) +(flet ($e25 (bvslt ?e7 (sign_extend[6] ?e4))) +(flet ($e26 (bvule (zero_extend[12] ?e9) ?e15)) +(flet ($e27 (bvuge ?e13 ?e13)) +(flet ($e28 (distinct (zero_extend[6] ?e12) ?e7)) +(flet ($e29 (distinct ?e3 (sign_extend[13] ?e12))) +(flet ($e30 (xor $e27 $e17)) +(flet ($e31 (or $e25 $e28)) +(flet ($e32 (iff $e31 $e21)) +(flet ($e33 (and $e18 $e22)) +(flet ($e34 (iff $e30 $e33)) +(flet ($e35 (and $e24 $e24)) +(flet ($e36 (and $e29 $e20)) +(flet ($e37 (and $e34 $e26)) +(flet ($e38 (iff $e36 $e16)) +(flet ($e39 (or $e38 $e32)) +(flet ($e40 (not $e19)) +(flet ($e41 (xor $e23 $e35)) +(flet ($e42 (and $e41 $e40)) +(flet ($e43 (implies $e42 $e37)) +(flet ($e44 (not $e43)) +(flet ($e45 (and $e39 $e44)) +$e45 +)))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/decision/error20.delta01.smt b/test/regress/regress0/decision/error20.delta01.smt new file mode 100644 index 000000000..dfa582be9 --- /dev/null +++ b/test/regress/regress0/decision/error20.delta01.smt @@ -0,0 +1,19 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:extrafuns ((v0 BitVec[16])) +:extrafuns ((v1 BitVec[1])) +:extrafuns ((a4 Array[1:7])) +:status sat +:formula +(let (?n1 (select a4 v1)) +(let (?n2 bv0[7]) +(flet ($n3 (bvsle ?n1 ?n2)) +(let (?n4 bv0[16]) +(let (?n5 bv0[1]) +(flet ($n6 (= v1 ?n5)) +(let (?n7 (ite $n6 ?n4 v0)) +(flet ($n8 (= ?n4 ?n7)) +(flet ($n9 (not $n8)) +(flet ($n10 (and $n3 $n9)) +$n10 +))))))))))) diff --git a/test/regress/regress0/decision/error20.smt b/test/regress/regress0/decision/error20.smt new file mode 100644 index 000000000..adc638500 --- /dev/null +++ b/test/regress/regress0/decision/error20.smt @@ -0,0 +1,66 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status sat +:extrafuns ((v0 BitVec[16])) +:extrafuns ((v1 BitVec[1])) +:extrafuns ((a2 Array[12:10])) +:extrafuns ((a3 Array[14:11])) +:extrafuns ((a4 Array[1:7])) +:formula +(let (?e5 bv1[1]) +(let (?e6 (ite (= bv1[1] (extract[0:0] v1)) (sign_extend[15] ?e5) v0)) +(let (?e7 (store a4 (extract[4:4] v0) (extract[9:3] v0))) +(let (?e8 (store ?e7 ?e5 (extract[12:6] v0))) +(let (?e9 (store ?e8 v1 (sign_extend[6] ?e5))) +(let (?e10 (select a4 v1)) +(let (?e11 (store ?e8 ?e5 (zero_extend[6] v1))) +(let (?e12 (select ?e8 v1)) +(let (?e13 (store a2 (extract[14:3] v0) (zero_extend[3] ?e10))) +(let (?e14 (rotate_right[0] v1)) +(let (?e15 (rotate_right[3] ?e10)) +(let (?e16 (ite (bvsge ?e12 (zero_extend[6] v1)) bv1[1] bv0[1])) +(let (?e17 (repeat[5] ?e14)) +(let (?e18 (bvsdiv (sign_extend[9] ?e15) ?e6)) +(let (?e19 (bvmul (zero_extend[15] ?e5) v0)) +(flet ($e20 (= (zero_extend[15] ?e5) ?e18)) +(flet ($e21 (bvugt (zero_extend[9] ?e10) ?e19)) +(flet ($e22 (bvsgt ?e15 (zero_extend[6] v1))) +(flet ($e23 (bvslt ?e14 ?e16)) +(flet ($e24 (bvugt ?e19 (zero_extend[15] v1))) +(flet ($e25 (distinct ?e12 ?e12)) +(flet ($e26 (bvule ?e17 (sign_extend[4] ?e5))) +(flet ($e27 (bvsle ?e18 (zero_extend[15] ?e16))) +(flet ($e28 (bvsle ?e10 ?e15)) +(flet ($e29 (bvsgt ?e12 (zero_extend[6] ?e16))) +(flet ($e30 (bvsgt (sign_extend[4] ?e5) ?e17)) +(flet ($e31 (bvsle ?e17 (zero_extend[4] ?e14))) +(flet ($e32 (bvult (zero_extend[11] ?e17) ?e6)) +(flet ($e33 (bvult ?e5 ?e5)) +(flet ($e34 (bvugt ?e12 (sign_extend[2] ?e17))) +(flet ($e35 (bvsle (sign_extend[6] v1) ?e15)) +(flet ($e36 (bvule ?e15 (zero_extend[6] ?e14))) +(flet ($e37 (bvsgt v0 ?e6)) +(flet ($e38 (if_then_else $e23 $e25 $e26)) +(flet ($e39 (iff $e33 $e35)) +(flet ($e40 (or $e21 $e36)) +(flet ($e41 (or $e20 $e32)) +(flet ($e42 (and $e22 $e39)) +(flet ($e43 (not $e41)) +(flet ($e44 (implies $e24 $e31)) +(flet ($e45 (or $e42 $e44)) +(flet ($e46 (iff $e27 $e37)) +(flet ($e47 (or $e29 $e46)) +(flet ($e48 (not $e28)) +(flet ($e49 (and $e47 $e43)) +(flet ($e50 (iff $e40 $e30)) +(flet ($e51 (xor $e34 $e50)) +(flet ($e52 (iff $e45 $e51)) +(flet ($e53 (if_then_else $e49 $e49 $e52)) +(flet ($e54 (or $e53 $e38)) +(flet ($e55 (iff $e54 $e54)) +(flet ($e56 (and $e48 $e55)) +(flet ($e57 (and $e56 (not (= ?e6 bv0[16])))) +(flet ($e58 (and $e57 (not (= ?e6 (bvnot bv0[16]))))) +$e58 +))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |