From a648adc7767ccd720cf1684ee8adac3d03f64f53 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 14 Jun 2012 21:35:18 +0000 Subject: [PATCH] add failing regression, move error up --- src/smt/smt_engine.cpp | 3 + test/regress/regress0/decision/Makefile.am | 3 +- .../regress0/decision/error3.delta01.smt | 32 ++++ test/regress/regress0/decision/error3.smt | 138 ++++++++++++++++++ 4 files changed, 175 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/decision/error3.delta01.smt create mode 100644 test/regress/regress0/decision/error3.smt diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3da8e1b33..e3f549898 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1387,8 +1387,11 @@ void SmtEnginePrivate::processAssertions() { } if(Options::current()->repeatSimp) { + unsigned preReSimp = d_assertionsToCheck.size(); d_assertionsToCheck.swap(d_assertionsToPreprocess); simplifyAssertions(); + Assert(preReSimp == d_assertionsToCheck.size(), + "Can't add assertions here"); removeITEs(); } diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index de3ccd60a..31f54fdfc 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -28,8 +28,9 @@ TESTS = \ error20.delta01.smt \ error122.smt \ error122.delta01.smt - # Incorrect answers: +# error3.smt \ +# error3.delta01.smt # EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/decision/error3.delta01.smt b/test/regress/regress0/decision/error3.delta01.smt new file mode 100644 index 000000000..59568bad6 --- /dev/null +++ b/test/regress/regress0/decision/error3.delta01.smt @@ -0,0 +1,32 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:extrafuns ((v1 BitVec[3])) +:extrafuns ((a2 Array[13:3])) +:status unknown +:formula +(let (?n1 bv0[3]) +(flet ($n2 (bvsgt v1 v1)) +(let (?n3 bv1[1]) +(let (?n4 bv0[1]) +(let (?n5 (ite $n2 ?n3 ?n4)) +(let (?n6 (sign_extend[2] ?n5)) +(flet ($n7 (bvslt ?n6 v1)) +(let (?n8 (ite $n7 ?n3 ?n4)) +(let (?n9 (sign_extend[2] ?n8)) +(let (?n10 bv0[13]) +(let (?n11 (select a2 ?n10)) +(let (?n12 (bvshl ?n9 ?n11)) +(flet ($n13 (= ?n1 ?n12)) +(flet ($n14 (not $n13)) +(let (?n15 (bvnot ?n8)) +(let (?n16 (zero_extend[10] ?n15)) +(let (?n17 bv0[11]) +(flet ($n18 (= ?n16 ?n17)) +(flet ($n19 (not $n18)) +(let (?n20 (repeat[2] ?n15)) +(let (?n21 (zero_extend[9] ?n20)) +(flet ($n22 (bvult ?n17 ?n21)) +(flet ($n23 (and $n19 $n22)) +(flet ($n24 (and $n14 $n23)) +$n24 +))))))))))))))))))))))))) diff --git a/test/regress/regress0/decision/error3.smt b/test/regress/regress0/decision/error3.smt new file mode 100644 index 000000000..57a982d08 --- /dev/null +++ b/test/regress/regress0/decision/error3.smt @@ -0,0 +1,138 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status unknown +: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 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + -- 2.30.2