diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-14 21:54:25 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-14 21:54:25 +0000 |
commit | 56013a80a76b0d46f6f8497d7570e51877dbf99d (patch) | |
tree | 9d4ed01590a15b13b91485333fd497e26889e0c0 /test/regress/regress0 | |
parent | b273e586629c5759dc88cd962e52a89f65b674a7 (diff) |
bug fixes to models, array rewriter with previously failing testcases
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/aufbv/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/aufbv/fuzz13.smt | 90 | ||||
-rw-r--r-- | test/regress/regress0/auflia/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/auflia/fuzz02.smt | 244 | ||||
-rw-r--r-- | test/regress/regress0/auflia/fuzz03.smt | 15 | ||||
-rw-r--r-- | test/regress/regress0/auflia/fuzz04.smt | 15 |
6 files changed, 369 insertions, 1 deletions
diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index 1a698b180..c67ce5b00 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -44,6 +44,7 @@ TESTS = \ fuzz10.smt \ fuzz11.smt \ fuzz12.smt \ + fuzz13.smt \ fifo32bc06k08.delta01.smt \ rewrite_bug.smt \ array_rewrite_bug.smt diff --git a/test/regress/regress0/aufbv/fuzz13.smt b/test/regress/regress0/aufbv/fuzz13.smt new file mode 100644 index 000000000..d8c0b8480 --- /dev/null +++ b/test/regress/regress0/aufbv/fuzz13.smt @@ -0,0 +1,90 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status sat +:extrafuns ((v0 BitVec[9])) +:extrafuns ((v1 BitVec[14])) +:extrafuns ((a2 Array[2:5])) +:extrafuns ((a3 Array[8:5])) +:formula +(let (?e4 bv712[10]) +(let (?e5 (ite (bvslt ?e4 ?e4) bv1[1] bv0[1])) +(let (?e6 (ite (= bv1[1] (extract[2:2] v1)) (sign_extend[5] v0) v1)) +(let (?e7 (store a2 (sign_extend[1] ?e5) (extract[12:8] ?e6))) +(let (?e8 (store ?e7 (zero_extend[1] ?e5) (extract[6:2] v1))) +(let (?e9 (select ?e8 (extract[12:11] v1))) +(let (?e10 (select a2 (extract[2:1] ?e4))) +(let (?e11 (store ?e8 (zero_extend[1] ?e5) ?e10)) +(let (?e12 (select ?e11 (extract[1:0] ?e10))) +(let (?e13 (select a2 (extract[3:2] ?e9))) +(let (?e14 (ite (bvsge (zero_extend[4] ?e10) v0) bv1[1] bv0[1])) +(let (?e15 (bvnand ?e4 (zero_extend[5] ?e13))) +(let (?e16 (ite (bvule ?e12 ?e12) bv1[1] bv0[1])) +(let (?e17 (extract[0:0] ?e5)) +(let (?e18 (zero_extend[0] ?e6)) +(let (?e19 (bvsdiv (zero_extend[9] ?e12) v1)) +(let (?e20 (bvsdiv (zero_extend[9] ?e9) ?e6)) +(flet ($e21 (bvugt v1 (zero_extend[9] ?e12))) +(flet ($e22 (bvuge ?e9 (sign_extend[4] ?e14))) +(flet ($e23 (bvslt ?e6 (sign_extend[9] ?e10))) +(flet ($e24 (bvugt ?e19 v1)) +(flet ($e25 (bvult (sign_extend[4] ?e12) v0)) +(flet ($e26 (= (sign_extend[4] ?e15) v1)) +(flet ($e27 (= ?e19 (sign_extend[9] ?e12))) +(flet ($e28 (bvsge (zero_extend[9] ?e9) ?e6)) +(flet ($e29 (bvuge ?e13 (zero_extend[4] ?e5))) +(flet ($e30 (distinct (zero_extend[4] ?e14) ?e9)) +(flet ($e31 (bvsle (zero_extend[4] ?e14) ?e12)) +(flet ($e32 (bvslt ?e10 ?e12)) +(flet ($e33 (distinct ?e6 ?e18)) +(flet ($e34 (bvsge (sign_extend[4] ?e12) v0)) +(flet ($e35 (bvsge ?e6 (zero_extend[5] v0))) +(flet ($e36 (distinct v0 (sign_extend[4] ?e13))) +(flet ($e37 (= ?e18 (sign_extend[5] v0))) +(flet ($e38 (bvugt ?e16 ?e5)) +(flet ($e39 (bvslt ?e9 (sign_extend[4] ?e16))) +(flet ($e40 (distinct (zero_extend[9] ?e13) ?e19)) +(flet ($e41 (bvsle ?e19 (zero_extend[13] ?e5))) +(flet ($e42 (bvslt (zero_extend[4] ?e12) v0)) +(flet ($e43 (bvugt ?e14 ?e17)) +(flet ($e44 (bvsle (sign_extend[4] ?e14) ?e13)) +(flet ($e45 (bvugt (zero_extend[4] ?e14) ?e12)) +(flet ($e46 (bvsge ?e19 ?e6)) +(flet ($e47 (bvsle ?e10 (zero_extend[4] ?e14))) +(flet ($e48 (bvsle ?e20 (zero_extend[4] ?e4))) +(flet ($e49 (and $e22 $e30)) +(flet ($e50 (or $e38 $e29)) +(flet ($e51 (xor $e41 $e34)) +(flet ($e52 (iff $e21 $e48)) +(flet ($e53 (iff $e46 $e23)) +(flet ($e54 (iff $e33 $e44)) +(flet ($e55 (and $e24 $e43)) +(flet ($e56 (implies $e32 $e31)) +(flet ($e57 (or $e56 $e47)) +(flet ($e58 (xor $e50 $e40)) +(flet ($e59 (or $e57 $e45)) +(flet ($e60 (iff $e42 $e59)) +(flet ($e61 (or $e35 $e36)) +(flet ($e62 (if_then_else $e51 $e60 $e25)) +(flet ($e63 (or $e55 $e54)) +(flet ($e64 (xor $e53 $e39)) +(flet ($e65 (and $e63 $e63)) +(flet ($e66 (or $e61 $e28)) +(flet ($e67 (and $e27 $e27)) +(flet ($e68 (or $e26 $e26)) +(flet ($e69 (or $e65 $e49)) +(flet ($e70 (xor $e58 $e62)) +(flet ($e71 (implies $e68 $e37)) +(flet ($e72 (if_then_else $e52 $e52 $e70)) +(flet ($e73 (implies $e66 $e67)) +(flet ($e74 (xor $e64 $e71)) +(flet ($e75 (and $e73 $e73)) +(flet ($e76 (implies $e72 $e69)) +(flet ($e77 (xor $e76 $e75)) +(flet ($e78 (iff $e77 $e74)) +(flet ($e79 (and $e78 (not (= v1 bv0[14])))) +(flet ($e80 (and $e79 (not (= v1 (bvnot bv0[14]))))) +(flet ($e81 (and $e80 (not (= ?e6 bv0[14])))) +(flet ($e82 (and $e81 (not (= ?e6 (bvnot bv0[14]))))) +$e82 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index 362209579..ed810eaeb 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -15,7 +15,10 @@ endif TESTS = \ bug330.smt2 \ bug336.smt2 \ - fuzz01.delta01.smt + fuzz01.delta01.smt \ + fuzz02.smt \ + fuzz03.smt \ + fuzz04.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/auflia/fuzz02.smt b/test/regress/regress0/auflia/fuzz02.smt new file mode 100644 index 000000000..7f34226e7 --- /dev/null +++ b/test/regress/regress0/auflia/fuzz02.smt @@ -0,0 +1,244 @@ +(benchmark fuzzsmt +:logic QF_AUFLIA +:status sat +:extrafuns ((f0 Int Int)) +:extrafuns ((f1 Array Array)) +:extrapreds ((p0 Int Int Int)) +:extrapreds ((p1 Array Array Array)) +:extrafuns ((v0 Int)) +:extrafuns ((v1 Int)) +:extrafuns ((v2 Array)) +:extrafuns ((v3 Array)) +:formula +(let (?e4 1) +(let (?e5 (+ v0 v0)) +(let (?e6 (f0 v0)) +(let (?e7 (ite (p0 ?e6 v1 ?e5) 1 0)) +(let (?e8 (* v0 ?e4)) +(let (?e9 (select v3 ?e6)) +(let (?e10 (select v3 ?e5)) +(let (?e11 (f1 v3)) +(let (?e12 (f1 ?e11)) +(let (?e13 (f1 ?e12)) +(let (?e14 (f1 v2)) +(flet ($e15 (p1 v3 v3 v3)) +(flet ($e16 (p1 ?e11 ?e11 ?e13)) +(flet ($e17 (p1 ?e14 ?e13 ?e12)) +(flet ($e18 (p1 v2 v3 ?e11)) +(flet ($e19 (p0 v1 ?e9 v0)) +(flet ($e20 (p0 ?e8 v1 ?e7)) +(flet ($e21 (> v0 ?e6)) +(flet ($e22 (< ?e5 ?e10)) +(let (?e23 (ite $e20 ?e12 ?e12)) +(let (?e24 (ite $e21 ?e23 v3)) +(let (?e25 (ite $e22 ?e13 ?e12)) +(let (?e26 (ite $e18 v2 ?e24)) +(let (?e27 (ite $e15 ?e11 ?e26)) +(let (?e28 (ite $e22 ?e14 ?e26)) +(let (?e29 (ite $e16 ?e13 ?e23)) +(let (?e30 (ite $e17 ?e11 ?e28)) +(let (?e31 (ite $e19 ?e13 ?e11)) +(let (?e32 (ite $e21 v0 ?e7)) +(let (?e33 (ite $e20 ?e8 v1)) +(let (?e34 (ite $e20 ?e32 ?e32)) +(let (?e35 (ite $e16 v1 ?e8)) +(let (?e36 (ite $e17 ?e6 ?e7)) +(let (?e37 (ite $e19 ?e32 ?e7)) +(let (?e38 (ite $e21 ?e9 ?e8)) +(let (?e39 (ite $e15 ?e10 ?e37)) +(let (?e40 (ite $e19 ?e7 ?e6)) +(let (?e41 (ite $e22 ?e5 ?e8)) +(let (?e42 (ite $e18 ?e32 ?e8)) +(let (?e43 (select ?e13 ?e35)) +(let (?e44 (select ?e26 ?e37)) +(let (?e45 (f1 ?e26)) +(let (?e46 (f1 ?e12)) +(let (?e47 (f1 ?e25)) +(let (?e48 (f1 ?e25)) +(let (?e49 (f1 ?e24)) +(let (?e50 (f1 ?e14)) +(let (?e51 (f1 ?e23)) +(let (?e52 (f1 ?e27)) +(let (?e53 (f1 ?e30)) +(let (?e54 (f1 ?e29)) +(let (?e55 (f1 ?e31)) +(let (?e56 (f1 v3)) +(let (?e57 (f1 ?e50)) +(let (?e58 (f1 ?e13)) +(let (?e59 (f1 ?e11)) +(let (?e60 (f1 ?e12)) +(let (?e61 (f1 ?e28)) +(let (?e62 (f1 ?e49)) +(let (?e63 (f1 v2)) +(let (?e64 (f0 ?e36)) +(let (?e65 (+ v0 ?e36)) +(let (?e66 (- v1 ?e35)) +(let (?e67 (f0 ?e65)) +(let (?e68 (f0 ?e32)) +(let (?e69 (f0 ?e6)) +(let (?e70 (- ?e35 ?e68)) +(let (?e71 (* ?e4 ?e40)) +(let (?e72 (~ ?e42)) +(let (?e73 (- ?e38 ?e37)) +(let (?e74 (~ ?e39)) +(let (?e75 (ite (p0 ?e64 ?e34 ?e70) 1 0)) +(let (?e76 (- ?e10 ?e5)) +(let (?e77 (* ?e41 ?e4)) +(let (?e78 (ite (p0 ?e73 ?e7 ?e34) 1 0)) +(let (?e79 (~ ?e10)) +(let (?e80 (- ?e42 ?e64)) +(let (?e81 (* ?e10 (~ ?e4))) +(let (?e82 (+ ?e9 ?e69)) +(let (?e83 (- ?e34 ?e39)) +(let (?e84 (~ ?e33)) +(let (?e85 (+ ?e43 ?e33)) +(let (?e86 (- ?e37 ?e37)) +(let (?e87 (ite (p0 ?e5 ?e64 ?e83) 1 0)) +(let (?e88 (f0 ?e74)) +(let (?e89 (ite (p0 ?e88 ?e9 ?e73) 1 0)) +(let (?e90 (+ ?e88 ?e80)) +(let (?e91 (- ?e8 ?e8)) +(let (?e92 (~ ?e44)) +(flet ($e93 (p1 ?e52 ?e59 ?e30)) +(flet ($e94 (p1 ?e61 ?e29 ?e46)) +(flet ($e95 (p1 ?e51 ?e50 ?e63)) +(flet ($e96 (p1 ?e13 ?e63 ?e23)) +(flet ($e97 (p1 ?e57 ?e25 ?e57)) +(flet ($e98 (p1 v2 ?e58 ?e31)) +(flet ($e99 (p1 ?e14 ?e28 ?e14)) +(flet ($e100 (p1 ?e62 ?e57 ?e30)) +(flet ($e101 (p1 ?e53 ?e12 ?e62)) +(flet ($e102 (p1 ?e49 ?e12 ?e52)) +(flet ($e103 (p1 ?e46 ?e49 ?e14)) +(flet ($e104 (p1 ?e57 v2 ?e31)) +(flet ($e105 (p1 ?e24 ?e55 ?e14)) +(flet ($e106 (p1 ?e53 ?e59 ?e30)) +(flet ($e107 (p1 v3 ?e11 ?e30)) +(flet ($e108 (p1 ?e56 ?e59 ?e60)) +(flet ($e109 (p1 ?e62 ?e23 ?e55)) +(flet ($e110 (p1 ?e29 ?e59 ?e51)) +(flet ($e111 (p1 ?e30 ?e28 ?e59)) +(flet ($e112 (p1 v2 ?e54 ?e13)) +(flet ($e113 (p1 ?e14 ?e50 ?e48)) +(flet ($e114 (p1 ?e26 ?e60 ?e30)) +(flet ($e115 (p1 ?e27 ?e12 ?e47)) +(flet ($e116 (p1 ?e45 ?e53 ?e62)) +(flet ($e117 (<= ?e91 ?e85)) +(flet ($e118 (>= ?e40 ?e89)) +(flet ($e119 (distinct ?e76 ?e77)) +(flet ($e120 (>= ?e91 ?e5)) +(flet ($e121 (= ?e84 ?e68)) +(flet ($e122 (p0 ?e41 v1 ?e36)) +(flet ($e123 (= ?e77 ?e69)) +(flet ($e124 (> ?e38 ?e10)) +(flet ($e125 (p0 v1 ?e77 ?e5)) +(flet ($e126 (= ?e64 ?e41)) +(flet ($e127 (>= ?e81 ?e40)) +(flet ($e128 (< ?e67 ?e39)) +(flet ($e129 (distinct ?e78 ?e65)) +(flet ($e130 (<= ?e34 ?e33)) +(flet ($e131 (<= ?e72 ?e76)) +(flet ($e132 (> ?e87 ?e88)) +(flet ($e133 (>= ?e92 ?e8)) +(flet ($e134 (>= ?e86 ?e36)) +(flet ($e135 (> ?e32 ?e33)) +(flet ($e136 (distinct ?e90 ?e6)) +(flet ($e137 (< ?e88 ?e35)) +(flet ($e138 (p0 ?e9 ?e38 ?e78)) +(flet ($e139 (> ?e80 ?e32)) +(flet ($e140 (p0 ?e79 ?e91 ?e88)) +(flet ($e141 (p0 ?e75 ?e10 ?e74)) +(flet ($e142 (>= ?e34 ?e39)) +(flet ($e143 (p0 ?e66 ?e67 ?e66)) +(flet ($e144 (= ?e90 ?e39)) +(flet ($e145 (< ?e37 ?e79)) +(flet ($e146 (distinct ?e44 ?e78)) +(flet ($e147 (< ?e83 v0)) +(flet ($e148 (>= ?e7 ?e69)) +(flet ($e149 (>= ?e73 ?e10)) +(flet ($e150 (p0 ?e71 ?e90 ?e65)) +(flet ($e151 (p0 ?e36 ?e33 ?e33)) +(flet ($e152 (> ?e82 ?e80)) +(flet ($e153 (distinct ?e79 ?e10)) +(flet ($e154 (p0 ?e42 ?e64 v0)) +(flet ($e155 (< ?e70 ?e86)) +(flet ($e156 (<= ?e43 ?e7)) +(flet ($e157 (or $e16 $e139)) +(flet ($e158 (if_then_else $e103 $e93 $e141)) +(flet ($e159 (not $e132)) +(flet ($e160 (or $e111 $e100)) +(flet ($e161 (iff $e160 $e134)) +(flet ($e162 (and $e19 $e133)) +(flet ($e163 (and $e146 $e128)) +(flet ($e164 (and $e157 $e156)) +(flet ($e165 (xor $e140 $e155)) +(flet ($e166 (implies $e113 $e153)) +(flet ($e167 (iff $e164 $e102)) +(flet ($e168 (implies $e121 $e116)) +(flet ($e169 (if_then_else $e142 $e119 $e104)) +(flet ($e170 (implies $e129 $e99)) +(flet ($e171 (or $e135 $e161)) +(flet ($e172 (or $e126 $e15)) +(flet ($e173 (implies $e158 $e137)) +(flet ($e174 (iff $e166 $e117)) +(flet ($e175 (iff $e105 $e174)) +(flet ($e176 (not $e125)) +(flet ($e177 (iff $e120 $e171)) +(flet ($e178 (xor $e168 $e149)) +(flet ($e179 (and $e96 $e96)) +(flet ($e180 (and $e130 $e143)) +(flet ($e181 (and $e108 $e20)) +(flet ($e182 (if_then_else $e173 $e159 $e167)) +(flet ($e183 (xor $e118 $e107)) +(flet ($e184 (implies $e98 $e169)) +(flet ($e185 (and $e177 $e136)) +(flet ($e186 (not $e185)) +(flet ($e187 (and $e170 $e138)) +(flet ($e188 (iff $e109 $e147)) +(flet ($e189 (or $e188 $e145)) +(flet ($e190 (implies $e152 $e94)) +(flet ($e191 (if_then_else $e97 $e181 $e163)) +(flet ($e192 (iff $e115 $e190)) +(flet ($e193 (if_then_else $e183 $e172 $e17)) +(flet ($e194 (not $e127)) +(flet ($e195 (iff $e179 $e101)) +(flet ($e196 (iff $e186 $e154)) +(flet ($e197 (if_then_else $e178 $e176 $e150)) +(flet ($e198 (xor $e122 $e124)) +(flet ($e199 (not $e182)) +(flet ($e200 (and $e112 $e197)) +(flet ($e201 (iff $e151 $e184)) +(flet ($e202 (or $e106 $e192)) +(flet ($e203 (iff $e162 $e95)) +(flet ($e204 (and $e199 $e199)) +(flet ($e205 (if_then_else $e131 $e187 $e131)) +(flet ($e206 (xor $e144 $e201)) +(flet ($e207 (and $e18 $e202)) +(flet ($e208 (and $e193 $e22)) +(flet ($e209 (or $e123 $e203)) +(flet ($e210 (not $e196)) +(flet ($e211 (and $e209 $e200)) +(flet ($e212 (xor $e208 $e114)) +(flet ($e213 (xor $e212 $e175)) +(flet ($e214 (and $e148 $e206)) +(flet ($e215 (or $e198 $e210)) +(flet ($e216 (or $e213 $e215)) +(flet ($e217 (xor $e189 $e194)) +(flet ($e218 (and $e214 $e204)) +(flet ($e219 (and $e211 $e21)) +(flet ($e220 (and $e165 $e191)) +(flet ($e221 (xor $e180 $e180)) +(flet ($e222 (and $e218 $e205)) +(flet ($e223 (iff $e195 $e219)) +(flet ($e224 (not $e221)) +(flet ($e225 (iff $e222 $e220)) +(flet ($e226 (implies $e225 $e223)) +(flet ($e227 (not $e207)) +(flet ($e228 (if_then_else $e226 $e226 $e216)) +(flet ($e229 (iff $e217 $e110)) +(flet ($e230 (not $e229)) +(flet ($e231 (if_then_else $e224 $e230 $e227)) +(flet ($e232 (or $e231 $e228)) +$e232 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/auflia/fuzz03.smt b/test/regress/regress0/auflia/fuzz03.smt new file mode 100644 index 000000000..151250a1f --- /dev/null +++ b/test/regress/regress0/auflia/fuzz03.smt @@ -0,0 +1,15 @@ +(benchmark fuzzsmt +:logic QF_AUFLIA +:extrapreds ((p1 Array Array Array)) +:extrafuns ((v1 Array)) +:extrafuns ((f1 Array Array Array Array)) +:status sat +:formula +(let (?n1 0) +(let (?n2 (store v1 ?n1 ?n1)) +(let (?n3 (f1 v1 v1 ?n2)) +(let (?n4 (f1 v1 ?n2 v1)) +(let (?n5 (f1 v1 ?n4 ?n2)) +(flet ($n6 (p1 ?n3 ?n5 v1)) +$n6 +))))))) diff --git a/test/regress/regress0/auflia/fuzz04.smt b/test/regress/regress0/auflia/fuzz04.smt new file mode 100644 index 000000000..7523aae28 --- /dev/null +++ b/test/regress/regress0/auflia/fuzz04.smt @@ -0,0 +1,15 @@ +(benchmark fuzzsmt +:logic QF_AUFLIA +:extrapreds ((p1 Array Array)) +:extrafuns ((f1 Array Array Array Array)) +:extrafuns ((v3 Array)) +:status sat +:formula +(let (?n1 (f1 v3 v3 v3)) +(let (?n2 0) +(let (?n3 (store v3 ?n2 ?n2)) +(let (?n4 (f1 v3 v3 ?n3)) +(let (?n5 (f1 v3 ?n4 v3)) +(flet ($n6 (p1 ?n1 ?n5)) +$n6 +))))))) |