diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/bv/fuzz01.smt | 183 | ||||
| -rw-r--r-- | test/regress/regress0/bv/fuzz02.smt | 122 | ||||
| -rw-r--r-- | test/regress/regress0/bv/fuzz03.smt | 81 | ||||
| -rw-r--r-- | test/regress/regress0/bv/fuzz04.smt | 249 | ||||
| -rw-r--r-- | test/regress/regress0/bv/fuzz05.smt | 282 | ||||
| -rw-r--r-- | test/regress/regress0/bv/fuzz06.smt | 218 | ||||
| -rw-r--r-- | test/regress/regress0/bv/fuzz07.smt | 395 | ||||
| -rw-r--r-- | test/regress/regress0/bv/fuzz08.smt | 19 | ||||
| -rw-r--r-- | test/regress/regress0/bv/fuzz09.smt | 370 |
9 files changed, 1919 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz01.smt b/test/regress/regress0/bv/fuzz01.smt new file mode 100644 index 000000000..df6b54394 --- /dev/null +++ b/test/regress/regress0/bv/fuzz01.smt @@ -0,0 +1,183 @@ +(benchmark fuzzsmt +:logic QF_BV +:status sat +:extrafuns ((v0 BitVec[16])) +:extrafuns ((v1 BitVec[2])) +:extrafuns ((v2 BitVec[11])) +:extrafuns ((v3 BitVec[5])) +:extrafuns ((v4 BitVec[15])) +:formula +(let (?e5 bv0[1]) +(let (?e6 (ite (bvult v4 (sign_extend[13] v1)) bv1[1] bv0[1])) +(let (?e7 (bvadd (sign_extend[9] v1) v2)) +(let (?e8 (bvcomp v4 v4)) +(let (?e9 (bvadd ?e7 (zero_extend[10] ?e6))) +(let (?e10 (bvand v0 (sign_extend[11] v3))) +(let (?e11 (ite (bvsge (zero_extend[11] v3) v0) bv1[1] bv0[1])) +(let (?e12 (ite (bvsge (zero_extend[9] v1) ?e9) bv1[1] bv0[1])) +(let (?e13 (repeat[1] v0)) +(let (?e14 (bvshl ?e6 ?e12)) +(let (?e15 (ite (= bv1[1] (extract[0:0] v0)) ?e9 (zero_extend[10] ?e6))) +(let (?e16 (ite (bvsle (sign_extend[9] v1) v2) bv1[1] bv0[1])) +(let (?e17 (ite (bvsge v4 (zero_extend[14] ?e6)) bv1[1] bv0[1])) +(let (?e18 (bvcomp (sign_extend[10] ?e6) ?e9)) +(let (?e19 (ite (bvsle ?e15 ?e15) bv1[1] bv0[1])) +(let (?e20 (ite (bvule ?e10 (zero_extend[15] ?e5)) bv1[1] bv0[1])) +(flet ($e21 (= (zero_extend[10] ?e18) ?e9)) +(flet ($e22 (= ?e7 ?e7)) +(flet ($e23 (= ?e17 ?e6)) +(flet ($e24 (= (zero_extend[15] ?e17) ?e10)) +(flet ($e25 (= (zero_extend[10] ?e16) ?e7)) +(flet ($e26 (= (sign_extend[13] v1) v4)) +(flet ($e27 (= (sign_extend[15] ?e16) v0)) +(flet ($e28 (= (sign_extend[15] ?e18) ?e10)) +(flet ($e29 (= ?e7 (sign_extend[10] ?e18))) +(flet ($e30 (= ?e9 (sign_extend[9] v1))) +(flet ($e31 (= ?e11 ?e18)) +(flet ($e32 (= (sign_extend[15] ?e20) ?e10)) +(flet ($e33 (= ?e18 ?e8)) +(flet ($e34 (= ?e14 ?e6)) +(flet ($e35 (= (zero_extend[15] ?e20) v0)) +(flet ($e36 (= v4 (sign_extend[14] ?e11))) +(flet ($e37 (= (sign_extend[1] v4) ?e13)) +(flet ($e38 (= ?e20 ?e16)) +(flet ($e39 (= v1 (sign_extend[1] ?e14))) +(flet ($e40 (= ?e5 ?e19)) +(flet ($e41 (= ?e7 (sign_extend[10] ?e14))) +(flet ($e42 (= ?e15 (sign_extend[6] v3))) +(flet ($e43 (= ?e18 ?e18)) +(flet ($e44 (= ?e16 ?e8)) +(flet ($e45 (= (sign_extend[15] ?e8) v0)) +(flet ($e46 (= (zero_extend[4] ?e15) v4)) +(flet ($e47 (= (sign_extend[14] ?e20) v4)) +(flet ($e48 (= v3 (sign_extend[4] ?e17))) +(flet ($e49 (= ?e17 ?e6)) +(flet ($e50 (= ?e10 (sign_extend[15] ?e16))) +(flet ($e51 (= ?e16 ?e18)) +(flet ($e52 (= (sign_extend[10] ?e12) ?e9)) +(flet ($e53 (= ?e8 ?e19)) +(flet ($e54 (= (zero_extend[1] ?e14) v1)) +(flet ($e55 (= v1 (sign_extend[1] ?e6))) +(flet ($e56 (= v4 (zero_extend[14] ?e14))) +(flet ($e57 (= ?e17 ?e20)) +(flet ($e58 (= ?e20 ?e11)) +(flet ($e59 (= (zero_extend[4] ?e6) v3)) +(flet ($e60 (= v0 (zero_extend[5] ?e9))) +(flet ($e61 (= v0 (sign_extend[15] ?e17))) +(flet ($e62 (= ?e15 ?e9)) +(flet ($e63 (= (sign_extend[4] ?e15) v4)) +(flet ($e64 (= (zero_extend[10] ?e16) ?e15)) +(flet ($e65 (= v4 (zero_extend[14] ?e18))) +(flet ($e66 (= (sign_extend[10] ?e14) ?e9)) +(flet ($e67 (= ?e20 ?e17)) +(flet ($e68 (= ?e14 ?e18)) +(flet ($e69 (= ?e10 (sign_extend[5] ?e9))) +(flet ($e70 (= ?e5 ?e16)) +(flet ($e71 (= (zero_extend[10] ?e19) ?e15)) +(flet ($e72 (= ?e15 ?e9)) +(flet ($e73 (= ?e12 ?e11)) +(flet ($e74 (= (sign_extend[10] ?e14) ?e7)) +(flet ($e75 (= ?e20 ?e20)) +(flet ($e76 (= ?e12 ?e18)) +(flet ($e77 (= ?e20 ?e16)) +(flet ($e78 (= ?e17 ?e16)) +(flet ($e79 (= (zero_extend[14] ?e17) v4)) +(flet ($e80 (= ?e7 (sign_extend[10] ?e8))) +(flet ($e81 (= ?e11 ?e20)) +(flet ($e82 (= ?e9 (sign_extend[10] ?e8))) +(flet ($e83 (= v0 (zero_extend[15] ?e18))) +(flet ($e84 (= ?e17 ?e12)) +(flet ($e85 (= (zero_extend[4] ?e18) v3)) +(flet ($e86 (= v1 (sign_extend[1] ?e5))) +(flet ($e87 (= ?e14 ?e5)) +(flet ($e88 (= ?e13 (zero_extend[15] ?e14))) +(flet ($e89 (= ?e19 ?e16)) +(flet ($e90 (= ?e20 ?e17)) +(flet ($e91 (= ?e15 v2)) +(flet ($e92 (or $e72 $e38)) +(flet ($e93 (if_then_else $e58 $e65 $e60)) +(flet ($e94 (not $e71)) +(flet ($e95 (and $e75 $e63)) +(flet ($e96 (and $e82 $e53)) +(flet ($e97 (iff $e22 $e59)) +(flet ($e98 (if_then_else $e96 $e41 $e29)) +(flet ($e99 (not $e46)) +(flet ($e100 (not $e39)) +(flet ($e101 (not $e62)) +(flet ($e102 (iff $e91 $e83)) +(flet ($e103 (implies $e51 $e61)) +(flet ($e104 (not $e33)) +(flet ($e105 (xor $e84 $e45)) +(flet ($e106 (implies $e54 $e50)) +(flet ($e107 (iff $e40 $e57)) +(flet ($e108 (xor $e30 $e89)) +(flet ($e109 (implies $e68 $e103)) +(flet ($e110 (if_then_else $e101 $e52 $e99)) +(flet ($e111 (or $e80 $e110)) +(flet ($e112 (iff $e108 $e88)) +(flet ($e113 (xor $e86 $e78)) +(flet ($e114 (not $e48)) +(flet ($e115 (if_then_else $e67 $e92 $e49)) +(flet ($e116 (implies $e77 $e93)) +(flet ($e117 (and $e26 $e25)) +(flet ($e118 (or $e47 $e117)) +(flet ($e119 (or $e87 $e21)) +(flet ($e120 (not $e64)) +(flet ($e121 (not $e119)) +(flet ($e122 (and $e106 $e118)) +(flet ($e123 (or $e114 $e43)) +(flet ($e124 (implies $e100 $e74)) +(flet ($e125 (iff $e123 $e109)) +(flet ($e126 (iff $e23 $e37)) +(flet ($e127 (not $e121)) +(flet ($e128 (and $e70 $e98)) +(flet ($e129 (if_then_else $e76 $e90 $e122)) +(flet ($e130 (iff $e81 $e111)) +(flet ($e131 (implies $e24 $e24)) +(flet ($e132 (iff $e130 $e42)) +(flet ($e133 (if_then_else $e79 $e34 $e94)) +(flet ($e134 (implies $e102 $e56)) +(flet ($e135 (or $e66 $e27)) +(flet ($e136 (and $e131 $e55)) +(flet ($e137 (iff $e105 $e120)) +(flet ($e138 (if_then_else $e129 $e85 $e32)) +(flet ($e139 (xor $e44 $e132)) +(flet ($e140 (xor $e133 $e139)) +(flet ($e141 (and $e134 $e128)) +(flet ($e142 (or $e127 $e113)) +(flet ($e143 (implies $e136 $e136)) +(flet ($e144 (iff $e143 $e36)) +(flet ($e145 (not $e144)) +(flet ($e146 (if_then_else $e35 $e137 $e142)) +(flet ($e147 (if_then_else $e116 $e126 $e112)) +(flet ($e148 (and $e141 $e97)) +(flet ($e149 (implies $e146 $e115)) +(flet ($e150 (not $e140)) +(flet ($e151 (and $e150 $e95)) +(flet ($e152 (if_then_else $e147 $e138 $e147)) +(flet ($e153 (or $e135 $e31)) +(flet ($e154 (iff $e148 $e73)) +(flet ($e155 (or $e152 $e69)) +(flet ($e156 (not $e107)) +(flet ($e157 (if_then_else $e149 $e28 $e104)) +(flet ($e158 (iff $e157 $e124)) +(flet ($e159 (iff $e125 $e151)) +(flet ($e160 (if_then_else $e154 $e159 $e145)) +(flet ($e161 (iff $e155 $e155)) +(flet ($e162 (iff $e160 $e160)) +(flet ($e163 (iff $e158 $e156)) +(flet ($e164 (iff $e162 $e162)) +(flet ($e165 (and $e163 $e161)) +(flet ($e166 (xor $e164 $e165)) +(flet ($e167 (or $e166 $e166)) +(flet ($e168 (or $e167 $e167)) +(flet ($e169 (iff $e153 $e153)) +(flet ($e170 (or $e168 $e168)) +(flet ($e171 (or $e169 $e169)) +(flet ($e172 (not $e171)) +(flet ($e173 (implies $e170 $e170)) +(flet ($e174 (not $e172)) +(flet ($e175 (iff $e173 $e174)) +$e175 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/bv/fuzz02.smt b/test/regress/regress0/bv/fuzz02.smt new file mode 100644 index 000000000..41b616ef0 --- /dev/null +++ b/test/regress/regress0/bv/fuzz02.smt @@ -0,0 +1,122 @@ +(benchmark fuzzsmt +:logic QF_BV +:status sat +:extrafuns ((v0 BitVec[3])) +:extrafuns ((v1 BitVec[12])) +:extrafuns ((v2 BitVec[9])) +:formula +(let (?e3 bv10[9]) +(let (?e4 (extract[6:6] ?e3)) +(let (?e5 (ite (bvult v2 v2) bv1[1] bv0[1])) +(let (?e6 (ite (bvsgt ?e4 ?e4) bv1[1] bv0[1])) +(let (?e7 (sign_extend[5] ?e6)) +(let (?e8 (concat ?e7 ?e5)) +(let (?e9 (bvcomp ?e8 (zero_extend[1] ?e7))) +(let (?e10 (ite (bvule ?e7 (zero_extend[5] ?e9)) bv1[1] bv0[1])) +(let (?e11 (bvadd (sign_extend[2] ?e10) v0)) +(let (?e12 (extract[1:0] v0)) +(let (?e13 (ite (bvslt ?e12 ?e12) bv1[1] bv0[1])) +(let (?e14 (ite (bvult ?e7 (sign_extend[4] ?e12)) bv1[1] bv0[1])) +(let (?e15 (bvlshr (sign_extend[8] ?e4) v2)) +(let (?e16 (repeat[2] v0)) +(let (?e17 (rotate_right[4] ?e15)) +(let (?e18 (bvxor ?e14 ?e14)) +(let (?e19 (bvand v2 (sign_extend[7] ?e12))) +(let (?e20 (bvnot v1)) +(flet ($e21 (= ?e15 ?e3)) +(flet ($e22 (= (sign_extend[6] ?e9) ?e8)) +(flet ($e23 (= ?e6 ?e4)) +(flet ($e24 (= ?e11 (zero_extend[2] ?e13))) +(flet ($e25 (= v0 (zero_extend[2] ?e13))) +(flet ($e26 (= (sign_extend[1] ?e4) ?e12)) +(flet ($e27 (= ?e15 ?e3)) +(flet ($e28 (= ?e3 ?e19)) +(flet ($e29 (= (zero_extend[8] ?e14) ?e15)) +(flet ($e30 (= v0 (sign_extend[2] ?e6))) +(flet ($e31 (= ?e11 (sign_extend[2] ?e4))) +(flet ($e32 (= ?e7 (zero_extend[5] ?e6))) +(flet ($e33 (= ?e5 ?e5)) +(flet ($e34 (= (zero_extend[8] ?e6) v2)) +(flet ($e35 (= ?e20 (zero_extend[3] ?e3))) +(flet ($e36 (= (zero_extend[8] ?e4) ?e15)) +(flet ($e37 (= ?e3 (sign_extend[8] ?e5))) +(flet ($e38 (= (sign_extend[11] ?e9) v1)) +(flet ($e39 (= (zero_extend[1] ?e9) ?e12)) +(flet ($e40 (= (sign_extend[6] v0) ?e15)) +(flet ($e41 (= ?e7 (zero_extend[5] ?e14))) +(flet ($e42 (= ?e6 ?e14)) +(flet ($e43 (= ?e16 (zero_extend[5] ?e4))) +(flet ($e44 (= (zero_extend[8] ?e9) v2)) +(flet ($e45 (= v1 (zero_extend[11] ?e5))) +(flet ($e46 (= ?e8 (zero_extend[6] ?e4))) +(flet ($e47 (= (sign_extend[1] ?e13) ?e12)) +(flet ($e48 (= (zero_extend[11] ?e18) v1)) +(flet ($e49 (= (zero_extend[11] ?e5) v1)) +(flet ($e50 (= ?e15 (sign_extend[8] ?e4))) +(flet ($e51 (= ?e13 ?e14)) +(flet ($e52 (= (zero_extend[2] ?e5) ?e11)) +(flet ($e53 (= (sign_extend[11] ?e9) v1)) +(flet ($e54 (= ?e8 (sign_extend[6] ?e5))) +(flet ($e55 (= (sign_extend[7] ?e12) v2)) +(flet ($e56 (= ?e20 (sign_extend[3] ?e15))) +(flet ($e57 (= ?e15 (sign_extend[6] ?e11))) +(flet ($e58 (= ?e6 ?e4)) +(flet ($e59 (= (sign_extend[8] ?e10) v2)) +(flet ($e60 (= (zero_extend[8] ?e10) ?e19)) +(flet ($e61 (= ?e9 ?e6)) +(flet ($e62 (= ?e11 (sign_extend[2] ?e9))) +(flet ($e63 (= v2 (zero_extend[8] ?e18))) +(flet ($e64 (= (sign_extend[2] ?e10) ?e11)) +(flet ($e65 (= ?e5 ?e5)) +(flet ($e66 (= (zero_extend[3] ?e16) ?e17)) +(flet ($e67 (if_then_else $e34 $e37 $e22)) +(flet ($e68 (xor $e61 $e63)) +(flet ($e69 (iff $e55 $e53)) +(flet ($e70 (not $e51)) +(flet ($e71 (or $e70 $e56)) +(flet ($e72 (or $e23 $e54)) +(flet ($e73 (or $e43 $e39)) +(flet ($e74 (implies $e58 $e32)) +(flet ($e75 (and $e21 $e59)) +(flet ($e76 (implies $e33 $e38)) +(flet ($e77 (and $e41 $e57)) +(flet ($e78 (if_then_else $e77 $e74 $e64)) +(flet ($e79 (iff $e36 $e52)) +(flet ($e80 (or $e29 $e25)) +(flet ($e81 (iff $e68 $e62)) +(flet ($e82 (xor $e78 $e76)) +(flet ($e83 (xor $e66 $e69)) +(flet ($e84 (or $e45 $e27)) +(flet ($e85 (xor $e83 $e79)) +(flet ($e86 (if_then_else $e72 $e72 $e65)) +(flet ($e87 (iff $e28 $e75)) +(flet ($e88 (if_then_else $e26 $e73 $e47)) +(flet ($e89 (xor $e60 $e60)) +(flet ($e90 (xor $e49 $e42)) +(flet ($e91 (iff $e44 $e48)) +(flet ($e92 (and $e71 $e80)) +(flet ($e93 (not $e88)) +(flet ($e94 (iff $e35 $e35)) +(flet ($e95 (iff $e81 $e90)) +(flet ($e96 (xor $e89 $e85)) +(flet ($e97 (xor $e82 $e94)) +(flet ($e98 (or $e92 $e40)) +(flet ($e99 (implies $e93 $e24)) +(flet ($e100 (if_then_else $e46 $e31 $e50)) +(flet ($e101 (or $e86 $e97)) +(flet ($e102 (and $e101 $e67)) +(flet ($e103 (if_then_else $e87 $e96 $e30)) +(flet ($e104 (not $e100)) +(flet ($e105 (xor $e91 $e104)) +(flet ($e106 (if_then_else $e84 $e102 $e84)) +(flet ($e107 (implies $e106 $e98)) +(flet ($e108 (implies $e107 $e103)) +(flet ($e109 (or $e95 $e95)) +(flet ($e110 (implies $e108 $e109)) +(flet ($e111 (not $e99)) +(flet ($e112 (or $e110 $e105)) +(flet ($e113 (or $e112 $e112)) +(flet ($e114 (xor $e111 $e113)) +$e114 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/bv/fuzz03.smt b/test/regress/regress0/bv/fuzz03.smt new file mode 100644 index 000000000..fe0b5b129 --- /dev/null +++ b/test/regress/regress0/bv/fuzz03.smt @@ -0,0 +1,81 @@ +(benchmark fuzzsmt +:logic QF_BV +:status sat +:extrafuns ((v0 BitVec[1])) +:extrafuns ((v1 BitVec[4])) +:extrafuns ((v2 BitVec[11])) +:extrafuns ((v3 BitVec[9])) +:formula +(let (?e4 bv0[1]) +(let (?e5 bv125[7]) +(let (?e6 (bvxor v2 (zero_extend[2] v3))) +(let (?e7 (ite (bvule (zero_extend[2] v3) ?e6) bv1[1] bv0[1])) +(let (?e8 (ite (= ?e6 v2) bv1[1] bv0[1])) +(let (?e9 (ite (= bv1[1] (extract[0:0] ?e8)) (zero_extend[10] ?e4) ?e6)) +(let (?e10 (ite (bvule (sign_extend[4] ?e5) ?e6) bv1[1] bv0[1])) +(let (?e11 (bvnor (zero_extend[8] ?e10) v3)) +(let (?e12 (ite (bvugt (sign_extend[8] ?e7) ?e11) bv1[1] bv0[1])) +(let (?e13 (bvor ?e6 (zero_extend[10] ?e12))) +(let (?e14 (bvor ?e4 v0)) +(let (?e15 (bvnor ?e13 (zero_extend[2] ?e11))) +(let (?e16 (sign_extend[5] ?e15)) +(let (?e17 (zero_extend[5] ?e6)) +(let (?e18 (ite (bvugt (sign_extend[8] v0) ?e11) bv1[1] bv0[1])) +(let (?e19 (rotate_right[0] v1)) +(flet ($e20 (= ?e18 ?e12)) +(flet ($e21 (= (sign_extend[10] ?e8) ?e13)) +(flet ($e22 (= ?e16 ?e16)) +(flet ($e23 (= (sign_extend[10] ?e14) ?e9)) +(flet ($e24 (= v3 (zero_extend[8] ?e14))) +(flet ($e25 (= v0 ?e10)) +(flet ($e26 (= (sign_extend[8] ?e7) v3)) +(flet ($e27 (= (sign_extend[5] ?e9) ?e16)) +(flet ($e28 (= ?e14 ?e7)) +(flet ($e29 (= ?e12 ?e18)) +(flet ($e30 (= ?e6 ?e13)) +(flet ($e31 (= ?e9 (zero_extend[10] ?e12))) +(flet ($e32 (= ?e16 (sign_extend[5] v2))) +(flet ($e33 (= v1 v1)) +(flet ($e34 (= (sign_extend[12] v1) ?e16)) +(flet ($e35 (= (sign_extend[5] ?e15) ?e16)) +(flet ($e36 (= v2 (zero_extend[7] ?e19))) +(flet ($e37 (= ?e13 (sign_extend[4] ?e5))) +(flet ($e38 (= (zero_extend[10] ?e14) ?e15)) +(flet ($e39 (= (sign_extend[5] v1) ?e11)) +(flet ($e40 (= (zero_extend[3] ?e7) v1)) +(flet ($e41 (= (sign_extend[7] v1) ?e13)) +(flet ($e42 (= v2 (zero_extend[10] v0))) +(flet ($e43 (= ?e13 (zero_extend[10] ?e4))) +(flet ($e44 (= ?e9 (sign_extend[7] ?e19))) +(flet ($e45 (= ?e15 (sign_extend[10] v0))) +(flet ($e46 (= ?e17 (zero_extend[5] ?e6))) +(flet ($e47 (iff $e38 $e44)) +(flet ($e48 (and $e23 $e36)) +(flet ($e49 (not $e25)) +(flet ($e50 (xor $e32 $e39)) +(flet ($e51 (if_then_else $e30 $e26 $e29)) +(flet ($e52 (not $e24)) +(flet ($e53 (if_then_else $e43 $e34 $e41)) +(flet ($e54 (iff $e47 $e33)) +(flet ($e55 (iff $e28 $e37)) +(flet ($e56 (or $e27 $e53)) +(flet ($e57 (and $e52 $e56)) +(flet ($e58 (if_then_else $e48 $e50 $e50)) +(flet ($e59 (if_then_else $e21 $e40 $e57)) +(flet ($e60 (implies $e58 $e55)) +(flet ($e61 (implies $e54 $e45)) +(flet ($e62 (implies $e35 $e61)) +(flet ($e63 (iff $e22 $e62)) +(flet ($e64 (or $e63 $e59)) +(flet ($e65 (and $e42 $e60)) +(flet ($e66 (or $e20 $e51)) +(flet ($e67 (or $e49 $e65)) +(flet ($e68 (not $e31)) +(flet ($e69 (xor $e64 $e68)) +(flet ($e70 (implies $e66 $e66)) +(flet ($e71 (iff $e46 $e69)) +(flet ($e72 (implies $e70 $e71)) +(flet ($e73 (implies $e72 $e67)) +$e73 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/bv/fuzz04.smt b/test/regress/regress0/bv/fuzz04.smt new file mode 100644 index 000000000..c5598a23a --- /dev/null +++ b/test/regress/regress0/bv/fuzz04.smt @@ -0,0 +1,249 @@ +(benchmark fuzzsmt +:logic QF_BV +:status sat +:extrafuns ((v0 BitVec[3])) +:extrafuns ((v1 BitVec[9])) +:extrafuns ((v2 BitVec[15])) +:extrafuns ((v3 BitVec[5])) +:formula +(let (?e4 bv111[9]) +(let (?e5 bv6[3]) +(let (?e6 (bvor v1 (zero_extend[6] v0))) +(let (?e7 (bvxor (sign_extend[4] v3) v1)) +(let (?e8 (bvlshr v1 ?e6)) +(let (?e9 (bvnot v0)) +(let (?e10 (bvshl v1 (sign_extend[6] v0))) +(let (?e11 (bvnot v1)) +(let (?e12 (bvmul ?e7 ?e7)) +(let (?e13 (ite (bvsgt ?e10 (zero_extend[4] v3)) bv1[1] bv0[1])) +(let (?e14 (bvnor ?e11 ?e6)) +(let (?e15 (bvnor v2 (zero_extend[6] ?e7))) +(let (?e16 (ite (= bv1[1] (extract[0:0] v3)) v1 ?e6)) +(let (?e17 (ite (bvule ?e10 ?e14) bv1[1] bv0[1])) +(let (?e18 (ite (bvuge (sign_extend[2] ?e17) ?e5) bv1[1] bv0[1])) +(let (?e19 (bvnot ?e10)) +(let (?e20 (ite (bvuge ?e13 ?e18) bv1[1] bv0[1])) +(let (?e21 (bvneg ?e15)) +(let (?e22 (bvmul ?e7 ?e10)) +(let (?e23 (rotate_left[2] v1)) +(let (?e24 (bvneg ?e13)) +(let (?e25 (sign_extend[7] ?e22)) +(let (?e26 (bvnand (sign_extend[6] v0) v1)) +(let (?e27 (bvxnor (zero_extend[1] ?e21) ?e25)) +(let (?e28 (bvnand ?e9 v0)) +(let (?e29 (bvor ?e15 (sign_extend[6] ?e26))) +(let (?e30 (bvsub ?e16 (sign_extend[8] ?e20))) +(let (?e31 (bvand (sign_extend[2] ?e13) ?e28)) +(let (?e32 (rotate_right[2] ?e12)) +(let (?e33 (repeat[1] ?e25)) +(let (?e34 (ite (= bv1[1] (extract[4:4] ?e19)) (zero_extend[6] ?e9) ?e23)) +(let (?e35 (bvlshr ?e8 (zero_extend[6] ?e31))) +(let (?e36 (rotate_left[5] ?e4)) +(flet ($e37 (= (sign_extend[8] ?e24) ?e12)) +(flet ($e38 (= (sign_extend[10] v3) v2)) +(flet ($e39 (= ?e29 (sign_extend[6] ?e32))) +(flet ($e40 (= ?e19 (sign_extend[6] ?e9))) +(flet ($e41 (= (zero_extend[6] ?e9) ?e6)) +(flet ($e42 (= ?e25 (zero_extend[15] ?e17))) +(flet ($e43 (= ?e25 (sign_extend[15] ?e17))) +(flet ($e44 (= ?e25 ?e25)) +(flet ($e45 (= v2 (sign_extend[12] ?e31))) +(flet ($e46 (= (sign_extend[15] ?e17) ?e25)) +(flet ($e47 (= ?e12 (zero_extend[6] ?e9))) +(flet ($e48 (= ?e29 (zero_extend[6] ?e4))) +(flet ($e49 (= (zero_extend[8] ?e24) ?e26)) +(flet ($e50 (= (zero_extend[4] ?e17) v3)) +(flet ($e51 (= ?e7 ?e23)) +(flet ($e52 (= (sign_extend[8] ?e18) ?e4)) +(flet ($e53 (= v1 ?e26)) +(flet ($e54 (= (sign_extend[8] ?e18) ?e16)) +(flet ($e55 (= ?e16 ?e36)) +(flet ($e56 (= ?e35 v1)) +(flet ($e57 (= ?e11 ?e36)) +(flet ($e58 (= ?e16 (sign_extend[6] ?e5))) +(flet ($e59 (= ?e22 ?e35)) +(flet ($e60 (= ?e33 (sign_extend[7] ?e6))) +(flet ($e61 (= v2 (sign_extend[12] ?e9))) +(flet ($e62 (= ?e12 ?e12)) +(flet ($e63 (= v0 (zero_extend[2] ?e18))) +(flet ($e64 (= ?e16 ?e7)) +(flet ($e65 (= ?e22 (sign_extend[8] ?e13))) +(flet ($e66 (= (zero_extend[7] ?e8) ?e33)) +(flet ($e67 (= v1 ?e35)) +(flet ($e68 (= ?e30 (zero_extend[6] ?e28))) +(flet ($e69 (= ?e6 (sign_extend[6] ?e31))) +(flet ($e70 (= ?e23 ?e35)) +(flet ($e71 (= ?e11 ?e14)) +(flet ($e72 (= (zero_extend[2] ?e20) v0)) +(flet ($e73 (= (sign_extend[8] ?e18) ?e26)) +(flet ($e74 (= (zero_extend[10] v3) ?e21)) +(flet ($e75 (= ?e19 (zero_extend[8] ?e20))) +(flet ($e76 (= ?e26 (sign_extend[8] ?e20))) +(flet ($e77 (= ?e29 (sign_extend[6] ?e16))) +(flet ($e78 (= (sign_extend[2] ?e17) ?e28)) +(flet ($e79 (= ?e30 ?e10)) +(flet ($e80 (= ?e20 ?e20)) +(flet ($e81 (= ?e15 (zero_extend[6] ?e19))) +(flet ($e82 (= ?e10 (zero_extend[8] ?e18))) +(flet ($e83 (= (zero_extend[14] ?e24) v2)) +(flet ($e84 (= (sign_extend[8] ?e17) ?e4)) +(flet ($e85 (= ?e21 (sign_extend[14] ?e24))) +(flet ($e86 (= ?e22 (sign_extend[8] ?e24))) +(flet ($e87 (= (zero_extend[8] ?e18) ?e23)) +(flet ($e88 (= (sign_extend[6] ?e31) ?e10)) +(flet ($e89 (= ?e21 (sign_extend[6] ?e7))) +(flet ($e90 (= ?e30 (sign_extend[6] v0))) +(flet ($e91 (= ?e33 (sign_extend[7] ?e36))) +(flet ($e92 (= ?e34 (sign_extend[6] ?e9))) +(flet ($e93 (= (zero_extend[2] ?e17) ?e9)) +(flet ($e94 (= ?e15 (zero_extend[6] ?e16))) +(flet ($e95 (= ?e25 (sign_extend[7] ?e8))) +(flet ($e96 (= ?e12 ?e8)) +(flet ($e97 (= v1 (sign_extend[8] ?e13))) +(flet ($e98 (= ?e32 ?e8)) +(flet ($e99 (= v0 v0)) +(flet ($e100 (= ?e14 (sign_extend[6] ?e5))) +(flet ($e101 (= (sign_extend[6] ?e34) ?e29)) +(flet ($e102 (= ?e35 (sign_extend[8] ?e13))) +(flet ($e103 (= ?e6 ?e12)) +(flet ($e104 (= (zero_extend[8] ?e18) ?e36)) +(flet ($e105 (= ?e36 (zero_extend[8] ?e17))) +(flet ($e106 (= (zero_extend[6] ?e5) ?e4)) +(flet ($e107 (= ?e34 (zero_extend[6] ?e5))) +(flet ($e108 (= (sign_extend[8] ?e17) ?e6)) +(flet ($e109 (= (sign_extend[8] ?e20) ?e4)) +(flet ($e110 (= ?e21 (zero_extend[6] ?e32))) +(flet ($e111 (= (zero_extend[6] ?e9) ?e19)) +(flet ($e112 (= ?e6 (zero_extend[8] ?e13))) +(flet ($e113 (= ?e25 (zero_extend[15] ?e24))) +(flet ($e114 (= (sign_extend[8] ?e20) ?e10)) +(flet ($e115 (= (sign_extend[6] v1) v2)) +(flet ($e116 (= (sign_extend[6] v0) ?e7)) +(flet ($e117 (= v1 ?e8)) +(flet ($e118 (= (zero_extend[6] ?e11) ?e15)) +(flet ($e119 (= (sign_extend[6] ?e22) v2)) +(flet ($e120 (= (zero_extend[4] ?e18) v3)) +(flet ($e121 (= ?e10 v1)) +(flet ($e122 (= ?e10 ?e32)) +(flet ($e123 (= v1 (zero_extend[6] ?e28))) +(flet ($e124 (= ?e25 ?e25)) +(flet ($e125 (= (zero_extend[2] ?e31) v3)) +(flet ($e126 (= ?e10 ?e8)) +(flet ($e127 (= ?e29 (sign_extend[12] v0))) +(flet ($e128 (= ?e30 (zero_extend[6] ?e9))) +(flet ($e129 (= v2 v2)) +(flet ($e130 (= (sign_extend[8] ?e18) ?e4)) +(flet ($e131 (= (sign_extend[8] ?e20) ?e36)) +(flet ($e132 (= ?e32 ?e22)) +(flet ($e133 (= ?e8 ?e16)) +(flet ($e134 (= (zero_extend[13] ?e5) ?e33)) +(flet ($e135 (= v2 (sign_extend[14] ?e20))) +(flet ($e136 (= ?e27 ?e27)) +(flet ($e137 (xor $e68 $e88)) +(flet ($e138 (and $e111 $e56)) +(flet ($e139 (and $e39 $e84)) +(flet ($e140 (if_then_else $e139 $e116 $e75)) +(flet ($e141 (xor $e108 $e110)) +(flet ($e142 (xor $e78 $e44)) +(flet ($e143 (xor $e131 $e133)) +(flet ($e144 (and $e97 $e95)) +(flet ($e145 (or $e80 $e124)) +(flet ($e146 (xor $e58 $e45)) +(flet ($e147 (or $e99 $e42)) +(flet ($e148 (or $e67 $e118)) +(flet ($e149 (if_then_else $e47 $e102 $e102)) +(flet ($e150 (and $e106 $e43)) +(flet ($e151 (iff $e82 $e86)) +(flet ($e152 (if_then_else $e61 $e109 $e81)) +(flet ($e153 (iff $e120 $e150)) +(flet ($e154 (not $e144)) +(flet ($e155 (xor $e49 $e69)) +(flet ($e156 (iff $e48 $e115)) +(flet ($e157 (not $e57)) +(flet ($e158 (and $e154 $e94)) +(flet ($e159 (not $e113)) +(flet ($e160 (and $e126 $e89)) +(flet ($e161 (or $e157 $e159)) +(flet ($e162 (and $e77 $e98)) +(flet ($e163 (not $e85)) +(flet ($e164 (implies $e55 $e137)) +(flet ($e165 (xor $e148 $e100)) +(flet ($e166 (not $e60)) +(flet ($e167 (implies $e153 $e65)) +(flet ($e168 (implies $e76 $e141)) +(flet ($e169 (if_then_else $e51 $e165 $e149)) +(flet ($e170 (not $e70)) +(flet ($e171 (xor $e92 $e37)) +(flet ($e172 (and $e104 $e134)) +(flet ($e173 (xor $e130 $e64)) +(flet ($e174 (not $e138)) +(flet ($e175 (implies $e174 $e145)) +(flet ($e176 (iff $e38 $e101)) +(flet ($e177 (or $e146 $e122)) +(flet ($e178 (or $e123 $e172)) +(flet ($e179 (and $e63 $e114)) +(flet ($e180 (xor $e117 $e41)) +(flet ($e181 (or $e136 $e161)) +(flet ($e182 (implies $e121 $e151)) +(flet ($e183 (iff $e52 $e53)) +(flet ($e184 (implies $e79 $e103)) +(flet ($e185 (or $e87 $e183)) +(flet ($e186 (not $e50)) +(flet ($e187 (iff $e173 $e186)) +(flet ($e188 (if_then_else $e170 $e156 $e112)) +(flet ($e189 (implies $e179 $e142)) +(flet ($e190 (not $e71)) +(flet ($e191 (iff $e164 $e93)) +(flet ($e192 (if_then_else $e143 $e191 $e127)) +(flet ($e193 (and $e59 $e189)) +(flet ($e194 (if_then_else $e178 $e132 $e129)) +(flet ($e195 (and $e152 $e167)) +(flet ($e196 (if_then_else $e171 $e62 $e162)) +(flet ($e197 (xor $e192 $e192)) +(flet ($e198 (and $e188 $e135)) +(flet ($e199 (iff $e175 $e196)) +(flet ($e200 (xor $e73 $e193)) +(flet ($e201 (and $e168 $e176)) +(flet ($e202 (iff $e185 $e201)) +(flet ($e203 (xor $e190 $e91)) +(flet ($e204 (iff $e74 $e182)) +(flet ($e205 (xor $e194 $e147)) +(flet ($e206 (and $e128 $e187)) +(flet ($e207 (iff $e83 $e169)) +(flet ($e208 (iff $e177 $e197)) +(flet ($e209 (if_then_else $e166 $e199 $e96)) +(flet ($e210 (or $e119 $e46)) +(flet ($e211 (xor $e200 $e207)) +(flet ($e212 (xor $e205 $e209)) +(flet ($e213 (iff $e212 $e184)) +(flet ($e214 (or $e105 $e180)) +(flet ($e215 (and $e181 $e210)) +(flet ($e216 (xor $e155 $e204)) +(flet ($e217 (and $e213 $e66)) +(flet ($e218 (implies $e214 $e211)) +(flet ($e219 (if_then_else $e206 $e208 $e198)) +(flet ($e220 (xor $e215 $e216)) +(flet ($e221 (if_then_else $e218 $e90 $e203)) +(flet ($e222 (xor $e202 $e160)) +(flet ($e223 (xor $e125 $e158)) +(flet ($e224 (or $e220 $e195)) +(flet ($e225 (or $e219 $e54)) +(flet ($e226 (not $e223)) +(flet ($e227 (if_then_else $e140 $e217 $e140)) +(flet ($e228 (not $e226)) +(flet ($e229 (or $e222 $e224)) +(flet ($e230 (iff $e225 $e221)) +(flet ($e231 (and $e72 $e163)) +(flet ($e232 (and $e227 $e40)) +(flet ($e233 (not $e107)) +(flet ($e234 (and $e232 $e231)) +(flet ($e235 (and $e228 $e228)) +(flet ($e236 (not $e235)) +(flet ($e237 (iff $e229 $e230)) +(flet ($e238 (and $e236 $e233)) +(flet ($e239 (xor $e237 $e238)) +(flet ($e240 (not $e234)) +(flet ($e241 (and $e239 $e240)) +$e241 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/bv/fuzz05.smt b/test/regress/regress0/bv/fuzz05.smt new file mode 100644 index 000000000..6a64a7218 --- /dev/null +++ b/test/regress/regress0/bv/fuzz05.smt @@ -0,0 +1,282 @@ +(benchmark fuzzsmt +:logic QF_BV +:status sat +:extrafuns ((v0 BitVec[12])) +:extrafuns ((v1 BitVec[2])) +:extrafuns ((v2 BitVec[13])) +:extrafuns ((v3 BitVec[10])) +:formula +(let (?e4 bv47[10]) +(let (?e5 (bvshl (zero_extend[8] v1) v3)) +(let (?e6 (bvcomp v2 (zero_extend[11] v1))) +(let (?e7 (ite (bvslt ?e5 ?e4) bv1[1] bv0[1])) +(let (?e8 (ite (bvsgt ?e4 (zero_extend[9] ?e6)) bv1[1] bv0[1])) +(let (?e9 (bvadd v1 (zero_extend[1] ?e6))) +(let (?e10 (ite (bvsle (zero_extend[9] ?e7) ?e4) bv1[1] bv0[1])) +(let (?e11 (rotate_left[0] ?e8)) +(let (?e12 (ite (= bv1[1] (extract[0:0] ?e7)) (zero_extend[1] ?e8) ?e9)) +(let (?e13 (bvadd ?e9 ?e9)) +(let (?e14 (rotate_right[0] ?e7)) +(let (?e15 (ite (bvslt (sign_extend[9] ?e6) ?e5) bv1[1] bv0[1])) +(let (?e16 (ite (distinct ?e7 ?e6) bv1[1] bv0[1])) +(let (?e17 (bvor ?e7 ?e8)) +(let (?e18 (bvand (zero_extend[1] ?e6) ?e9)) +(let (?e19 (ite (bvuge ?e18 (sign_extend[1] ?e16)) bv1[1] bv0[1])) +(let (?e20 (ite (bvsgt ?e18 (sign_extend[1] ?e17)) bv1[1] bv0[1])) +(let (?e21 (ite (= (sign_extend[3] v3) v2) bv1[1] bv0[1])) +(let (?e22 (bvxor ?e10 ?e19)) +(let (?e23 (bvxor (zero_extend[1] ?e19) v1)) +(let (?e24 (ite (bvule v1 (sign_extend[1] ?e19)) bv1[1] bv0[1])) +(let (?e25 (ite (bvuge ?e8 ?e17) bv1[1] bv0[1])) +(let (?e26 (ite (bvsge ?e20 ?e22) bv1[1] bv0[1])) +(let (?e27 (zero_extend[1] ?e22)) +(let (?e28 (bvsub (sign_extend[1] ?e10) v1)) +(let (?e29 (bvlshr ?e27 (sign_extend[1] ?e17))) +(let (?e30 (concat ?e17 ?e4)) +(let (?e31 (bvnand (zero_extend[11] ?e23) v2)) +(let (?e32 (bvashr (zero_extend[9] ?e19) ?e5)) +(let (?e33 (bvmul ?e23 (zero_extend[1] ?e25))) +(let (?e34 (repeat[1] ?e27)) +(let (?e35 (ite (bvuge ?e27 (zero_extend[1] ?e11)) bv1[1] bv0[1])) +(let (?e36 (ite (= (sign_extend[1] ?e11) v1) bv1[1] bv0[1])) +(let (?e37 (bvneg ?e31)) +(let (?e38 (ite (bvsgt ?e22 ?e14) bv1[1] bv0[1])) +(let (?e39 (ite (bvsge ?e36 ?e8) bv1[1] bv0[1])) +(let (?e40 (bvand ?e8 ?e14)) +(let (?e41 (bvand (zero_extend[12] ?e17) v2)) +(let (?e42 (ite (bvsle ?e35 ?e26) bv1[1] bv0[1])) +(let (?e43 (ite (bvsle v2 (sign_extend[12] ?e21)) bv1[1] bv0[1])) +(let (?e44 (bvshl ?e16 ?e42)) +(let (?e45 (ite (= ?e23 ?e29) bv1[1] bv0[1])) +(let (?e46 (repeat[1] ?e41)) +(let (?e47 (bvcomp ?e10 ?e21)) +(let (?e48 (ite (= (zero_extend[9] ?e47) ?e4) bv1[1] bv0[1])) +(let (?e49 (bvnand (zero_extend[11] ?e33) ?e41)) +(let (?e50 (ite (bvslt ?e44 ?e20) bv1[1] bv0[1])) +(let (?e51 (ite (bvsgt ?e31 (sign_extend[12] ?e21)) bv1[1] bv0[1])) +(let (?e52 (ite (bvslt v0 (zero_extend[11] ?e38)) bv1[1] bv0[1])) +(flet ($e53 (= v1 ?e29)) +(flet ($e54 (= (zero_extend[1] ?e44) ?e13)) +(flet ($e55 (= ?e17 ?e44)) +(flet ($e56 (= ?e4 (zero_extend[9] ?e39))) +(flet ($e57 (= (sign_extend[11] ?e14) v0)) +(flet ($e58 (= (zero_extend[12] ?e42) ?e37)) +(flet ($e59 (= ?e40 ?e36)) +(flet ($e60 (= ?e23 ?e33)) +(flet ($e61 (= (zero_extend[1] ?e24) ?e29)) +(flet ($e62 (= ?e28 (zero_extend[1] ?e50))) +(flet ($e63 (= ?e6 ?e25)) +(flet ($e64 (= ?e49 (sign_extend[12] ?e21))) +(flet ($e65 (= ?e20 ?e38)) +(flet ($e66 (= (zero_extend[1] ?e16) ?e18)) +(flet ($e67 (= ?e50 ?e16)) +(flet ($e68 (= ?e20 ?e48)) +(flet ($e69 (= ?e17 ?e21)) +(flet ($e70 (= (sign_extend[12] ?e44) ?e46)) +(flet ($e71 (= ?e51 ?e47)) +(flet ($e72 (= ?e5 (sign_extend[9] ?e16))) +(flet ($e73 (= ?e16 ?e21)) +(flet ($e74 (= ?e5 (sign_extend[8] ?e27))) +(flet ($e75 (= (zero_extend[9] ?e21) ?e5)) +(flet ($e76 (= (sign_extend[8] ?e28) ?e5)) +(flet ($e77 (= (sign_extend[9] ?e10) ?e32)) +(flet ($e78 (= ?e28 (sign_extend[1] ?e11))) +(flet ($e79 (= ?e29 (sign_extend[1] ?e17))) +(flet ($e80 (= ?e36 ?e15)) +(flet ($e81 (= (sign_extend[11] ?e45) v0)) +(flet ($e82 (= ?e27 (sign_extend[1] ?e40))) +(flet ($e83 (= ?e28 (zero_extend[1] ?e44))) +(flet ($e84 (= v2 (zero_extend[1] v0))) +(flet ($e85 (= ?e32 (sign_extend[9] ?e47))) +(flet ($e86 (= v3 (sign_extend[9] ?e24))) +(flet ($e87 (= ?e46 (sign_extend[12] ?e52))) +(flet ($e88 (= ?e46 ?e46)) +(flet ($e89 (= v2 (sign_extend[12] ?e20))) +(flet ($e90 (= v0 (sign_extend[10] ?e23))) +(flet ($e91 (= (zero_extend[9] ?e11) ?e4)) +(flet ($e92 (= ?e52 ?e17)) +(flet ($e93 (= v2 (zero_extend[12] ?e40))) +(flet ($e94 (= ?e35 ?e51)) +(flet ($e95 (= ?e42 ?e10)) +(flet ($e96 (= ?e47 ?e43)) +(flet ($e97 (= (zero_extend[1] ?e11) v1)) +(flet ($e98 (= (zero_extend[1] ?e32) ?e30)) +(flet ($e99 (= ?e23 (zero_extend[1] ?e11))) +(flet ($e100 (= ?e44 ?e22)) +(flet ($e101 (= ?e31 (sign_extend[12] ?e16))) +(flet ($e102 (= ?e32 (zero_extend[8] ?e27))) +(flet ($e103 (= (zero_extend[9] ?e45) ?e5)) +(flet ($e104 (= ?e27 ?e13)) +(flet ($e105 (= (zero_extend[1] ?e7) ?e13)) +(flet ($e106 (= ?e33 (zero_extend[1] ?e26))) +(flet ($e107 (= ?e13 (zero_extend[1] ?e51))) +(flet ($e108 (= ?e32 (zero_extend[9] ?e40))) +(flet ($e109 (= ?e29 v1)) +(flet ($e110 (= ?e35 ?e20)) +(flet ($e111 (= ?e34 (sign_extend[1] ?e19))) +(flet ($e112 (= ?e52 ?e52)) +(flet ($e113 (= (sign_extend[12] ?e40) ?e49)) +(flet ($e114 (= ?e47 ?e47)) +(flet ($e115 (= (zero_extend[12] ?e35) ?e46)) +(flet ($e116 (= (sign_extend[11] ?e35) v0)) +(flet ($e117 (= ?e4 (zero_extend[9] ?e38))) +(flet ($e118 (= v2 (sign_extend[12] ?e7))) +(flet ($e119 (= ?e47 ?e20)) +(flet ($e120 (= (zero_extend[1] ?e11) ?e9)) +(flet ($e121 (= ?e29 (zero_extend[1] ?e16))) +(flet ($e122 (= v0 (zero_extend[11] ?e24))) +(flet ($e123 (= ?e51 ?e36)) +(flet ($e124 (= (sign_extend[8] ?e13) v3)) +(flet ($e125 (= v1 (zero_extend[1] ?e45))) +(flet ($e126 (= (sign_extend[1] ?e48) ?e33)) +(flet ($e127 (= ?e45 ?e7)) +(flet ($e128 (= ?e26 ?e47)) +(flet ($e129 (= (zero_extend[11] v1) ?e41)) +(flet ($e130 (= (sign_extend[1] v0) v2)) +(flet ($e131 (= ?e5 (sign_extend[9] ?e26))) +(flet ($e132 (= (sign_extend[11] ?e48) v0)) +(flet ($e133 (= ?e38 ?e50)) +(flet ($e134 (= ?e13 v1)) +(flet ($e135 (= (sign_extend[1] ?e42) ?e23)) +(flet ($e136 (= ?e20 ?e7)) +(flet ($e137 (= ?e39 ?e19)) +(flet ($e138 (= ?e52 ?e38)) +(flet ($e139 (= ?e5 (zero_extend[9] ?e11))) +(flet ($e140 (= (sign_extend[11] ?e34) ?e49)) +(flet ($e141 (= ?e18 ?e28)) +(flet ($e142 (= ?e43 ?e26)) +(flet ($e143 (= ?e14 ?e16)) +(flet ($e144 (= ?e10 ?e40)) +(flet ($e145 (= ?e6 ?e45)) +(flet ($e146 (= ?e29 ?e18)) +(flet ($e147 (= ?e5 (sign_extend[9] ?e48))) +(flet ($e148 (= (zero_extend[9] ?e19) v3)) +(flet ($e149 (= ?e33 (sign_extend[1] ?e22))) +(flet ($e150 (= ?e50 ?e10)) +(flet ($e151 (= (sign_extend[9] ?e35) v3)) +(flet ($e152 (= ?e23 (zero_extend[1] ?e21))) +(flet ($e153 (= v2 (zero_extend[12] ?e15))) +(flet ($e154 (= v1 (sign_extend[1] ?e38))) +(flet ($e155 (= ?e23 (zero_extend[1] ?e22))) +(flet ($e156 (= ?e34 (zero_extend[1] ?e42))) +(flet ($e157 (= (zero_extend[9] ?e15) ?e4)) +(flet ($e158 (= v3 (sign_extend[9] ?e8))) +(flet ($e159 (= (sign_extend[9] ?e14) ?e32)) +(flet ($e160 (= (sign_extend[10] ?e13) v0)) +(flet ($e161 (= (zero_extend[1] ?e35) ?e12)) +(flet ($e162 (iff $e69 $e132)) +(flet ($e163 (and $e62 $e124)) +(flet ($e164 (iff $e152 $e133)) +(flet ($e165 (not $e65)) +(flet ($e166 (and $e159 $e57)) +(flet ($e167 (and $e163 $e56)) +(flet ($e168 (and $e129 $e90)) +(flet ($e169 (if_then_else $e54 $e102 $e91)) +(flet ($e170 (xor $e127 $e61)) +(flet ($e171 (iff $e137 $e59)) +(flet ($e172 (implies $e87 $e78)) +(flet ($e173 (iff $e77 $e81)) +(flet ($e174 (if_then_else $e170 $e161 $e171)) +(flet ($e175 (if_then_else $e174 $e94 $e92)) +(flet ($e176 (or $e168 $e55)) +(flet ($e177 (and $e121 $e88)) +(flet ($e178 (or $e167 $e131)) +(flet ($e179 (or $e126 $e125)) +(flet ($e180 (or $e151 $e79)) +(flet ($e181 (not $e122)) +(flet ($e182 (or $e112 $e83)) +(flet ($e183 (or $e130 $e136)) +(flet ($e184 (xor $e105 $e153)) +(flet ($e185 (if_then_else $e148 $e128 $e66)) +(flet ($e186 (iff $e109 $e154)) +(flet ($e187 (and $e119 $e96)) +(flet ($e188 (if_then_else $e179 $e64 $e140)) +(flet ($e189 (xor $e134 $e123)) +(flet ($e190 (implies $e97 $e165)) +(flet ($e191 (or $e188 $e71)) +(flet ($e192 (and $e145 $e185)) +(flet ($e193 (or $e191 $e99)) +(flet ($e194 (implies $e53 $e89)) +(flet ($e195 (iff $e180 $e116)) +(flet ($e196 (and $e84 $e117)) +(flet ($e197 (or $e135 $e75)) +(flet ($e198 (xor $e82 $e197)) +(flet ($e199 (if_then_else $e142 $e195 $e177)) +(flet ($e200 (implies $e181 $e73)) +(flet ($e201 (or $e169 $e70)) +(flet ($e202 (or $e150 $e106)) +(flet ($e203 (xor $e110 $e115)) +(flet ($e204 (or $e60 $e60)) +(flet ($e205 (implies $e138 $e187)) +(flet ($e206 (and $e194 $e156)) +(flet ($e207 (not $e114)) +(flet ($e208 (if_then_else $e147 $e63 $e118)) +(flet ($e209 (not $e86)) +(flet ($e210 (xor $e202 $e178)) +(flet ($e211 (if_then_else $e210 $e58 $e100)) +(flet ($e212 (implies $e113 $e166)) +(flet ($e213 (iff $e120 $e141)) +(flet ($e214 (and $e157 $e196)) +(flet ($e215 (if_then_else $e72 $e199 $e68)) +(flet ($e216 (not $e146)) +(flet ($e217 (and $e215 $e95)) +(flet ($e218 (not $e139)) +(flet ($e219 (xor $e214 $e176)) +(flet ($e220 (or $e175 $e211)) +(flet ($e221 (if_then_else $e162 $e198 $e172)) +(flet ($e222 (xor $e221 $e189)) +(flet ($e223 (xor $e213 $e104)) +(flet ($e224 (not $e206)) +(flet ($e225 (and $e203 $e108)) +(flet ($e226 (iff $e200 $e155)) +(flet ($e227 (if_then_else $e111 $e208 $e144)) +(flet ($e228 (implies $e227 $e85)) +(flet ($e229 (not $e223)) +(flet ($e230 (implies $e217 $e205)) +(flet ($e231 (iff $e204 $e80)) +(flet ($e232 (implies $e107 $e143)) +(flet ($e233 (if_then_else $e209 $e220 $e209)) +(flet ($e234 (or $e74 $e225)) +(flet ($e235 (or $e103 $e103)) +(flet ($e236 (implies $e67 $e234)) +(flet ($e237 (xor $e232 $e182)) +(flet ($e238 (xor $e190 $e235)) +(flet ($e239 (or $e231 $e233)) +(flet ($e240 (implies $e212 $e186)) +(flet ($e241 (iff $e218 $e237)) +(flet ($e242 (not $e238)) +(flet ($e243 (xor $e193 $e240)) +(flet ($e244 (implies $e228 $e222)) +(flet ($e245 (not $e230)) +(flet ($e246 (iff $e224 $e93)) +(flet ($e247 (and $e158 $e207)) +(flet ($e248 (if_then_else $e229 $e245 $e183)) +(flet ($e249 (iff $e98 $e184)) +(flet ($e250 (iff $e244 $e242)) +(flet ($e251 (if_then_else $e149 $e101 $e250)) +(flet ($e252 (xor $e236 $e173)) +(flet ($e253 (xor $e248 $e226)) +(flet ($e254 (and $e249 $e192)) +(flet ($e255 (if_then_else $e246 $e254 $e247)) +(flet ($e256 (if_then_else $e76 $e255 $e239)) +(flet ($e257 (not $e256)) +(flet ($e258 (or $e257 $e164)) +(flet ($e259 (or $e243 $e258)) +(flet ($e260 (iff $e219 $e216)) +(flet ($e261 (xor $e160 $e201)) +(flet ($e262 (not $e241)) +(flet ($e263 (not $e252)) +(flet ($e264 (not $e259)) +(flet ($e265 (and $e261 $e251)) +(flet ($e266 (if_then_else $e253 $e260 $e253)) +(flet ($e267 (implies $e264 $e264)) +(flet ($e268 (if_then_else $e266 $e266 $e265)) +(flet ($e269 (iff $e263 $e267)) +(flet ($e270 (if_then_else $e262 $e269 $e269)) +(flet ($e271 (and $e270 $e270)) +(flet ($e272 (not $e271)) +(flet ($e273 (xor $e272 $e272)) +(flet ($e274 (iff $e273 $e268)) +$e274 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/bv/fuzz06.smt b/test/regress/regress0/bv/fuzz06.smt new file mode 100644 index 000000000..6fc41f3c4 --- /dev/null +++ b/test/regress/regress0/bv/fuzz06.smt @@ -0,0 +1,218 @@ +(benchmark fuzzsmt +:logic QF_BV +:status sat +:extrafuns ((v0 BitVec[9])) +:extrafuns ((v1 BitVec[2])) +:extrafuns ((v2 BitVec[1])) +:extrafuns ((v3 BitVec[3])) +:formula +(let (?e4 bv256[9]) +(let (?e5 bv68[7]) +(let (?e6 (extract[0:0] v1)) +(let (?e7 (extract[1:0] v1)) +(let (?e8 (bvsub ?e4 (sign_extend[8] ?e6))) +(let (?e9 (zero_extend[1] v3)) +(let (?e10 (rotate_right[1] v1)) +(let (?e11 (ite (bvult ?e7 ?e7) bv1[1] bv0[1])) +(let (?e12 (extract[1:1] ?e9)) +(let (?e13 (extract[3:1] ?e9)) +(let (?e14 (ite (bvule (sign_extend[2] ?e12) v3) bv1[1] bv0[1])) +(let (?e15 (rotate_left[0] v2)) +(let (?e16 (bvadd ?e14 ?e6)) +(let (?e17 (extract[0:0] ?e16)) +(let (?e18 (bvxnor ?e10 (zero_extend[1] v2))) +(let (?e19 (bvnot v2)) +(let (?e20 (bvadd ?e18 ?e18)) +(let (?e21 (bvnand v3 (sign_extend[2] v2))) +(let (?e22 (bvnot ?e9)) +(let (?e23 (ite (bvslt ?e15 ?e14) bv1[1] bv0[1])) +(let (?e24 (bvcomp (sign_extend[2] ?e10) ?e9)) +(let (?e25 (bvor (zero_extend[1] ?e17) ?e10)) +(let (?e26 (bvand (zero_extend[1] ?e15) ?e25)) +(let (?e27 (ite (distinct (sign_extend[1] ?e26) ?e21) bv1[1] bv0[1])) +(let (?e28 (ite (bvult ?e11 ?e11) bv1[1] bv0[1])) +(let (?e29 (ite (bvugt ?e26 ?e10) bv1[1] bv0[1])) +(let (?e30 (bvadd ?e18 (sign_extend[1] ?e19))) +(let (?e31 (ite (= bv1[1] (extract[0:0] ?e5)) ?e9 (sign_extend[3] ?e19))) +(let (?e32 (bvmul (zero_extend[3] ?e24) ?e31)) +(let (?e33 (ite (bvslt ?e10 (zero_extend[1] ?e12)) bv1[1] bv0[1])) +(let (?e34 (ite (= bv1[1] (extract[0:0] ?e16)) ?e21 (zero_extend[2] ?e15))) +(let (?e35 (ite (bvslt v3 (zero_extend[2] ?e23)) bv1[1] bv0[1])) +(let (?e36 (rotate_right[0] ?e23)) +(let (?e37 (extract[1:1] ?e10)) +(let (?e38 (bvcomp (sign_extend[3] ?e19) ?e31)) +(let (?e39 (bvmul (sign_extend[8] ?e6) v0)) +(flet ($e40 (= ?e15 ?e27)) +(flet ($e41 (= v1 (sign_extend[1] ?e33))) +(flet ($e42 (= ?e36 ?e35)) +(flet ($e43 (= ?e22 (zero_extend[2] ?e30))) +(flet ($e44 (= (sign_extend[1] ?e33) ?e25)) +(flet ($e45 (= ?e18 ?e26)) +(flet ($e46 (= (zero_extend[5] ?e20) ?e5)) +(flet ($e47 (= ?e9 ?e32)) +(flet ($e48 (= (zero_extend[2] ?e37) ?e34)) +(flet ($e49 (= ?e32 (sign_extend[2] ?e25))) +(flet ($e50 (= (sign_extend[2] ?e20) ?e22)) +(flet ($e51 (= v0 (sign_extend[5] ?e9))) +(flet ($e52 (= ?e5 (sign_extend[6] ?e15))) +(flet ($e53 (= ?e11 ?e36)) +(flet ($e54 (= ?e6 ?e15)) +(flet ($e55 (= (zero_extend[8] ?e23) ?e8)) +(flet ($e56 (= ?e8 (zero_extend[8] ?e14))) +(flet ($e57 (= ?e20 ?e25)) +(flet ($e58 (= ?e11 ?e38)) +(flet ($e59 (= ?e11 ?e12)) +(flet ($e60 (= (zero_extend[5] ?e22) ?e4)) +(flet ($e61 (= (sign_extend[5] ?e32) ?e4)) +(flet ($e62 (= (sign_extend[1] ?e35) ?e7)) +(flet ($e63 (= ?e39 ?e39)) +(flet ($e64 (= ?e16 ?e11)) +(flet ($e65 (= ?e29 ?e14)) +(flet ($e66 (= (sign_extend[7] ?e30) v0)) +(flet ($e67 (= ?e4 (zero_extend[5] ?e22))) +(flet ($e68 (= ?e26 ?e18)) +(flet ($e69 (= ?e8 (zero_extend[7] ?e26))) +(flet ($e70 (= (sign_extend[3] ?e33) ?e31)) +(flet ($e71 (= ?e38 v2)) +(flet ($e72 (= (sign_extend[1] ?e24) ?e10)) +(flet ($e73 (= (zero_extend[8] ?e27) ?e4)) +(flet ($e74 (= (sign_extend[1] ?e28) ?e7)) +(flet ($e75 (= (sign_extend[8] v2) ?e8)) +(flet ($e76 (= ?e15 ?e24)) +(flet ($e77 (= ?e22 ?e31)) +(flet ($e78 (= ?e23 ?e6)) +(flet ($e79 (= ?e6 ?e27)) +(flet ($e80 (= ?e18 (sign_extend[1] ?e27))) +(flet ($e81 (= (sign_extend[1] ?e18) v3)) +(flet ($e82 (= ?e5 (zero_extend[6] ?e16))) +(flet ($e83 (= ?e23 ?e12)) +(flet ($e84 (= ?e30 (zero_extend[1] ?e37))) +(flet ($e85 (= (zero_extend[1] ?e38) ?e20)) +(flet ($e86 (= (sign_extend[8] ?e19) ?e8)) +(flet ($e87 (= ?e39 (zero_extend[6] ?e21))) +(flet ($e88 (= ?e21 (zero_extend[2] ?e6))) +(flet ($e89 (= (zero_extend[3] ?e28) ?e31)) +(flet ($e90 (= ?e32 (zero_extend[2] ?e25))) +(flet ($e91 (= ?e22 (zero_extend[1] ?e34))) +(flet ($e92 (= (zero_extend[6] ?e21) ?e39)) +(flet ($e93 (= ?e18 (sign_extend[1] ?e15))) +(flet ($e94 (= (zero_extend[1] ?e28) ?e20)) +(flet ($e95 (= ?e7 v1)) +(flet ($e96 (= (sign_extend[5] ?e31) ?e4)) +(flet ($e97 (= ?e17 ?e37)) +(flet ($e98 (= (zero_extend[3] ?e6) ?e31)) +(flet ($e99 (= ?e21 (sign_extend[2] ?e24))) +(flet ($e100 (= (zero_extend[3] ?e19) ?e22)) +(flet ($e101 (= ?e22 (sign_extend[3] ?e15))) +(flet ($e102 (= ?e11 ?e24)) +(flet ($e103 (= ?e34 (zero_extend[2] ?e16))) +(flet ($e104 (= ?e12 v2)) +(flet ($e105 (= ?e12 ?e37)) +(flet ($e106 (= ?e26 (zero_extend[1] ?e15))) +(flet ($e107 (= (zero_extend[2] ?e26) ?e22)) +(flet ($e108 (= (zero_extend[3] v2) ?e9)) +(flet ($e109 (= (sign_extend[5] ?e32) ?e8)) +(flet ($e110 (= ?e24 ?e17)) +(flet ($e111 (= ?e20 (sign_extend[1] ?e28))) +(flet ($e112 (= (sign_extend[6] ?e27) ?e5)) +(flet ($e113 (= (zero_extend[6] ?e34) ?e8)) +(flet ($e114 (= (sign_extend[7] ?e25) ?e8)) +(flet ($e115 (= ?e8 (zero_extend[7] ?e20))) +(flet ($e116 (= ?e20 (sign_extend[1] ?e36))) +(flet ($e117 (= ?e20 (sign_extend[1] ?e37))) +(flet ($e118 (= (sign_extend[7] ?e10) ?e39)) +(flet ($e119 (= ?e36 ?e16)) +(flet ($e120 (= ?e21 (zero_extend[1] ?e10))) +(flet ($e121 (= ?e38 ?e11)) +(flet ($e122 (= (sign_extend[1] ?e20) ?e34)) +(flet ($e123 (= ?e5 (zero_extend[4] ?e13))) +(flet ($e124 (not $e79)) +(flet ($e125 (if_then_else $e50 $e63 $e115)) +(flet ($e126 (if_then_else $e54 $e120 $e40)) +(flet ($e127 (if_then_else $e85 $e117 $e87)) +(flet ($e128 (iff $e127 $e95)) +(flet ($e129 (and $e76 $e46)) +(flet ($e130 (if_then_else $e93 $e42 $e65)) +(flet ($e131 (implies $e113 $e92)) +(flet ($e132 (not $e125)) +(flet ($e133 (implies $e62 $e61)) +(flet ($e134 (iff $e74 $e110)) +(flet ($e135 (and $e66 $e56)) +(flet ($e136 (if_then_else $e78 $e64 $e83)) +(flet ($e137 (if_then_else $e84 $e124 $e43)) +(flet ($e138 (if_then_else $e128 $e89 $e67)) +(flet ($e139 (not $e136)) +(flet ($e140 (or $e73 $e121)) +(flet ($e141 (if_then_else $e129 $e138 $e101)) +(flet ($e142 (and $e131 $e139)) +(flet ($e143 (if_then_else $e41 $e123 $e130)) +(flet ($e144 (xor $e100 $e81)) +(flet ($e145 (implies $e98 $e97)) +(flet ($e146 (xor $e71 $e143)) +(flet ($e147 (xor $e126 $e80)) +(flet ($e148 (if_then_else $e99 $e111 $e103)) +(flet ($e149 (implies $e47 $e88)) +(flet ($e150 (not $e140)) +(flet ($e151 (xor $e146 $e86)) +(flet ($e152 (and $e119 $e148)) +(flet ($e153 (not $e106)) +(flet ($e154 (xor $e114 $e104)) +(flet ($e155 (and $e58 $e91)) +(flet ($e156 (xor $e44 $e57)) +(flet ($e157 (if_then_else $e141 $e154 $e135)) +(flet ($e158 (if_then_else $e134 $e102 $e132)) +(flet ($e159 (iff $e108 $e109)) +(flet ($e160 (or $e90 $e53)) +(flet ($e161 (not $e77)) +(flet ($e162 (not $e157)) +(flet ($e163 (implies $e55 $e82)) +(flet ($e164 (implies $e69 $e51)) +(flet ($e165 (and $e164 $e116)) +(flet ($e166 (and $e133 $e161)) +(flet ($e167 (not $e165)) +(flet ($e168 (or $e159 $e162)) +(flet ($e169 (or $e112 $e153)) +(flet ($e170 (iff $e149 $e94)) +(flet ($e171 (or $e156 $e49)) +(flet ($e172 (and $e105 $e170)) +(flet ($e173 (and $e168 $e48)) +(flet ($e174 (iff $e172 $e151)) +(flet ($e175 (or $e60 $e118)) +(flet ($e176 (if_then_else $e155 $e142 $e175)) +(flet ($e177 (implies $e150 $e137)) +(flet ($e178 (if_then_else $e173 $e158 $e158)) +(flet ($e179 (not $e152)) +(flet ($e180 (not $e176)) +(flet ($e181 (xor $e144 $e59)) +(flet ($e182 (not $e171)) +(flet ($e183 (implies $e70 $e75)) +(flet ($e184 (and $e166 $e182)) +(flet ($e185 (and $e184 $e169)) +(flet ($e186 (not $e183)) +(flet ($e187 (not $e68)) +(flet ($e188 (implies $e185 $e180)) +(flet ($e189 (and $e122 $e188)) +(flet ($e190 (not $e181)) +(flet ($e191 (not $e174)) +(flet ($e192 (or $e145 $e72)) +(flet ($e193 (not $e160)) +(flet ($e194 (if_then_else $e177 $e178 $e45)) +(flet ($e195 (xor $e193 $e147)) +(flet ($e196 (or $e190 $e190)) +(flet ($e197 (xor $e179 $e192)) +(flet ($e198 (iff $e52 $e195)) +(flet ($e199 (or $e187 $e196)) +(flet ($e200 (implies $e194 $e96)) +(flet ($e201 (not $e189)) +(flet ($e202 (or $e191 $e167)) +(flet ($e203 (if_then_else $e198 $e186 $e202)) +(flet ($e204 (iff $e163 $e201)) +(flet ($e205 (if_then_else $e199 $e199 $e200)) +(flet ($e206 (implies $e197 $e204)) +(flet ($e207 (or $e203 $e107)) +(flet ($e208 (and $e205 $e206)) +(flet ($e209 (and $e208 $e208)) +(flet ($e210 (and $e209 $e207)) +$e210 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/bv/fuzz07.smt b/test/regress/regress0/bv/fuzz07.smt new file mode 100644 index 000000000..c813a31be --- /dev/null +++ b/test/regress/regress0/bv/fuzz07.smt @@ -0,0 +1,395 @@ +(benchmark fuzzsmt +:logic QF_BV +:status sat +:extrafuns ((v0 BitVec[5])) +:extrafuns ((v1 BitVec[2])) +:extrafuns ((v2 BitVec[4])) +:formula +(let (?e3 bv2[2]) +(let (?e4 bv2[2]) +(let (?e5 (bvnot ?e3)) +(let (?e6 (bvadd ?e4 v1)) +(let (?e7 (bvand ?e5 ?e6)) +(let (?e8 (bvashr v0 (sign_extend[3] ?e5))) +(let (?e9 (bvshl ?e4 ?e4)) +(let (?e10 (ite (bvsle ?e3 ?e6) bv1[1] bv0[1])) +(let (?e11 (bvxor ?e3 (sign_extend[1] ?e10))) +(let (?e12 (ite (= (sign_extend[3] ?e7) ?e8) bv1[1] bv0[1])) +(let (?e13 (bvor (zero_extend[1] ?e10) ?e5)) +(let (?e14 (concat ?e12 v0)) +(let (?e15 (bvand (zero_extend[1] ?e12) ?e6)) +(let (?e16 (bvnot ?e15)) +(let (?e17 (ite (bvsgt ?e8 (zero_extend[3] ?e13)) bv1[1] bv0[1])) +(let (?e18 (extract[0:0] ?e9)) +(let (?e19 (repeat[1] ?e7)) +(let (?e20 (ite (distinct ?e5 (zero_extend[1] ?e17)) bv1[1] bv0[1])) +(let (?e21 (bvlshr ?e3 (zero_extend[1] ?e12))) +(let (?e22 (bvcomp (zero_extend[1] ?e10) ?e6)) +(let (?e23 (sign_extend[2] ?e10)) +(let (?e24 (ite (bvule ?e16 ?e11) bv1[1] bv0[1])) +(let (?e25 (bvcomp ?e20 ?e10)) +(let (?e26 (bvshl (sign_extend[1] ?e17) ?e21)) +(let (?e27 (bvnot ?e11)) +(let (?e28 (bvsub (sign_extend[4] ?e16) ?e14)) +(let (?e29 (bvlshr ?e21 ?e27)) +(let (?e30 (bvneg ?e14)) +(let (?e31 (ite (bvugt ?e22 ?e17) bv1[1] bv0[1])) +(let (?e32 (ite (bvsge ?e19 ?e6) bv1[1] bv0[1])) +(let (?e33 (bvlshr ?e15 (sign_extend[1] ?e31))) +(let (?e34 (bvcomp (sign_extend[4] ?e15) ?e28)) +(let (?e35 (bvcomp (zero_extend[4] ?e26) ?e14)) +(let (?e36 (ite (bvsge ?e16 ?e13) bv1[1] bv0[1])) +(let (?e37 (rotate_right[0] ?e22)) +(let (?e38 (rotate_left[0] ?e35)) +(let (?e39 (bvsub ?e15 (sign_extend[1] ?e35))) +(let (?e40 (ite (= bv1[1] (extract[0:0] ?e31)) ?e6 ?e5)) +(let (?e41 (bvand (sign_extend[1] ?e31) ?e33)) +(let (?e42 (bvxor (zero_extend[3] ?e41) ?e8)) +(let (?e43 (bvmul ?e3 (zero_extend[1] ?e12))) +(let (?e44 (ite (bvsle (sign_extend[1] ?e18) ?e41) bv1[1] bv0[1])) +(let (?e45 (bvnand ?e26 ?e3)) +(let (?e46 (ite (bvsgt ?e23 (zero_extend[1] ?e4)) bv1[1] bv0[1])) +(let (?e47 (bvand ?e38 ?e37)) +(let (?e48 (bvneg ?e27)) +(let (?e49 (ite (= bv1[1] (extract[1:1] ?e13)) ?e3 (sign_extend[1] ?e24))) +(let (?e50 (concat ?e5 ?e38)) +(let (?e51 (bvadd ?e13 (sign_extend[1] ?e10))) +(let (?e52 (bvxnor (zero_extend[1] ?e6) ?e50)) +(let (?e53 (concat v1 ?e35)) +(let (?e54 (bvlshr ?e27 ?e41)) +(let (?e55 (ite (bvsle ?e29 ?e40) bv1[1] bv0[1])) +(let (?e56 (ite (bvugt (sign_extend[3] ?e45) ?e42) bv1[1] bv0[1])) +(let (?e57 (zero_extend[12] ?e5)) +(let (?e58 (bvcomp (sign_extend[3] ?e40) v0)) +(let (?e59 (ite (distinct ?e23 (zero_extend[2] ?e35)) bv1[1] bv0[1])) +(let (?e60 (bvor (sign_extend[1] ?e17) ?e26)) +(let (?e61 (ite (distinct ?e55 ?e38) bv1[1] bv0[1])) +(let (?e62 (bvnot ?e21)) +(let (?e63 (ite (bvuge (zero_extend[1] ?e32) ?e21) bv1[1] bv0[1])) +(let (?e64 (bvneg ?e17)) +(let (?e65 (rotate_right[0] ?e20)) +(let (?e66 (sign_extend[13] ?e15)) +(let (?e67 (ite (= ?e61 ?e55) bv1[1] bv0[1])) +(let (?e68 (bvor (sign_extend[1] ?e65) ?e49)) +(let (?e69 (zero_extend[4] ?e64)) +(let (?e70 (ite (bvugt ?e23 (zero_extend[1] ?e19)) bv1[1] bv0[1])) +(let (?e71 (bvneg ?e68)) +(let (?e72 (sign_extend[14] ?e54)) +(let (?e73 (ite (bvslt ?e14 (zero_extend[5] ?e37)) bv1[1] bv0[1])) +(let (?e74 (bvshl ?e53 (zero_extend[1] ?e7))) +(let (?e75 (repeat[4] ?e16)) +(let (?e76 (repeat[3] ?e51)) +(let (?e77 (ite (bvsle ?e28 ?e76) bv1[1] bv0[1])) +(let (?e78 (rotate_right[1] ?e42)) +(let (?e79 (bvor ?e65 ?e20)) +(let (?e80 (bvashr ?e19 ?e3)) +(let (?e81 (ite (distinct ?e23 (zero_extend[2] ?e44)) bv1[1] bv0[1])) +(let (?e82 (rotate_right[0] ?e15)) +(let (?e83 (bvashr ?e35 ?e35)) +(let (?e84 (bvsub ?e78 (sign_extend[2] ?e53))) +(let (?e85 (bvsub ?e11 (zero_extend[1] ?e36))) +(let (?e86 (ite (bvugt ?e53 (zero_extend[1] ?e33)) bv1[1] bv0[1])) +(let (?e87 (ite (bvugt (zero_extend[6] ?e48) ?e75) bv1[1] bv0[1])) +(let (?e88 (bvmul (zero_extend[3] ?e3) v0)) +(let (?e89 (concat ?e9 ?e14)) +(let (?e90 (ite (bvsle v2 v2) bv1[1] bv0[1])) +(flet ($e91 (= ?e54 ?e26)) +(flet ($e92 (= ?e3 (sign_extend[1] ?e77))) +(flet ($e93 (= ?e49 (sign_extend[1] ?e10))) +(flet ($e94 (= ?e85 (sign_extend[1] ?e73))) +(flet ($e95 (= ?e52 (sign_extend[2] ?e73))) +(flet ($e96 (= (sign_extend[1] ?e47) v1)) +(flet ($e97 (= (zero_extend[7] ?e20) ?e75)) +(flet ($e98 (= ?e57 (zero_extend[12] ?e15))) +(flet ($e99 (= ?e25 ?e90)) +(flet ($e100 (= ?e26 (sign_extend[1] ?e46))) +(flet ($e101 (= v1 (sign_extend[1] ?e31))) +(flet ($e102 (= ?e89 (zero_extend[7] ?e77))) +(flet ($e103 (= (zero_extend[4] ?e41) ?e30)) +(flet ($e104 (= ?e71 v1)) +(flet ($e105 (= (sign_extend[1] ?e83) ?e51)) +(flet ($e106 (= ?e32 ?e56)) +(flet ($e107 (= ?e25 ?e24)) +(flet ($e108 (= (sign_extend[1] ?e27) ?e74)) +(flet ($e109 (= ?e7 ?e15)) +(flet ($e110 (= (zero_extend[1] ?e70) ?e49)) +(flet ($e111 (= (sign_extend[1] ?e44) ?e15)) +(flet ($e112 (= ?e24 ?e63)) +(flet ($e113 (= ?e39 (sign_extend[1] ?e83))) +(flet ($e114 (= v1 (sign_extend[1] ?e70))) +(flet ($e115 (= ?e76 (sign_extend[1] v0))) +(flet ($e116 (= ?e77 ?e22)) +(flet ($e117 (= v1 (sign_extend[1] ?e59))) +(flet ($e118 (= ?e3 (sign_extend[1] ?e67))) +(flet ($e119 (= ?e39 ?e45)) +(flet ($e120 (= ?e42 (zero_extend[2] ?e50))) +(flet ($e121 (= (zero_extend[8] ?e14) ?e57)) +(flet ($e122 (= ?e28 (sign_extend[3] ?e23))) +(flet ($e123 (= (zero_extend[1] ?e37) ?e40)) +(flet ($e124 (= (sign_extend[5] ?e63) ?e30)) +(flet ($e125 (= ?e16 (sign_extend[1] ?e37))) +(flet ($e126 (= ?e81 ?e24)) +(flet ($e127 (= (zero_extend[1] ?e46) ?e54)) +(flet ($e128 (= ?e3 (sign_extend[1] ?e90))) +(flet ($e129 (= (zero_extend[1] ?e12) ?e21)) +(flet ($e130 (= ?e89 (zero_extend[3] ?e88))) +(flet ($e131 (= ?e31 ?e63)) +(flet ($e132 (= ?e15 ?e16)) +(flet ($e133 (= ?e72 (zero_extend[15] ?e81))) +(flet ($e134 (= ?e27 ?e41)) +(flet ($e135 (= ?e67 ?e12)) +(flet ($e136 (= (sign_extend[1] ?e65) ?e41)) +(flet ($e137 (= ?e69 (sign_extend[4] ?e81))) +(flet ($e138 (= ?e40 (zero_extend[1] ?e87))) +(flet ($e139 (= ?e59 ?e44)) +(flet ($e140 (= (zero_extend[5] ?e67) ?e28)) +(flet ($e141 (= ?e68 (sign_extend[1] ?e86))) +(flet ($e142 (= (zero_extend[2] ?e37) ?e23)) +(flet ($e143 (= (zero_extend[13] ?e6) ?e66)) +(flet ($e144 (= (zero_extend[5] ?e25) ?e76)) +(flet ($e145 (= ?e14 (zero_extend[4] ?e71))) +(flet ($e146 (= ?e5 ?e26)) +(flet ($e147 (= ?e17 ?e44)) +(flet ($e148 (= ?e64 ?e81)) +(flet ($e149 (= ?e60 (zero_extend[1] ?e83))) +(flet ($e150 (= ?e28 (sign_extend[5] ?e22))) +(flet ($e151 (= ?e50 (zero_extend[2] ?e87))) +(flet ($e152 (= ?e34 ?e47)) +(flet ($e153 (= (zero_extend[1] ?e65) ?e60)) +(flet ($e154 (= (zero_extend[1] ?e44) ?e5)) +(flet ($e155 (= ?e40 (sign_extend[1] ?e31))) +(flet ($e156 (= ?e78 ?e78)) +(flet ($e157 (= ?e76 (zero_extend[4] ?e49))) +(flet ($e158 (= ?e34 ?e67)) +(flet ($e159 (= ?e33 ?e45)) +(flet ($e160 (= ?e26 ?e4)) +(flet ($e161 (= ?e89 (sign_extend[6] ?e11))) +(flet ($e162 (= ?e86 ?e47)) +(flet ($e163 (= ?e32 ?e46)) +(flet ($e164 (= (zero_extend[2] ?e58) ?e23)) +(flet ($e165 (= ?e24 ?e64)) +(flet ($e166 (= ?e10 ?e24)) +(flet ($e167 (= ?e78 (zero_extend[3] ?e19))) +(flet ($e168 (= (sign_extend[6] ?e54) ?e89)) +(flet ($e169 (= ?e89 (sign_extend[7] ?e37))) +(flet ($e170 (= ?e42 (zero_extend[3] ?e13))) +(flet ($e171 (= ?e54 (sign_extend[1] ?e56))) +(flet ($e172 (= ?e27 ?e62)) +(flet ($e173 (= ?e75 (sign_extend[6] ?e4))) +(flet ($e174 (= ?e33 ?e80)) +(flet ($e175 (= (sign_extend[1] ?e17) ?e16)) +(flet ($e176 (= ?e17 ?e17)) +(flet ($e177 (= ?e80 ?e68)) +(flet ($e178 (= ?e15 ?e26)) +(flet ($e179 (= ?e82 (zero_extend[1] ?e22))) +(flet ($e180 (= (zero_extend[1] ?e79) ?e45)) +(flet ($e181 (= ?e50 (sign_extend[2] ?e90))) +(flet ($e182 (= ?e62 ?e80)) +(flet ($e183 (= ?e4 (zero_extend[1] ?e18))) +(flet ($e184 (= ?e60 (sign_extend[1] ?e36))) +(flet ($e185 (= ?e56 ?e32)) +(flet ($e186 (= ?e15 (sign_extend[1] ?e61))) +(flet ($e187 (= ?e59 ?e37)) +(flet ($e188 (= ?e36 ?e65)) +(flet ($e189 (= (sign_extend[2] v2) ?e14)) +(flet ($e190 (= ?e36 ?e35)) +(flet ($e191 (= (zero_extend[5] ?e53) ?e75)) +(flet ($e192 (= (sign_extend[13] ?e55) ?e57)) +(flet ($e193 (= (sign_extend[3] ?e84) ?e89)) +(flet ($e194 (= ?e27 (zero_extend[1] ?e77))) +(flet ($e195 (= (sign_extend[2] ?e43) v2)) +(flet ($e196 (= ?e62 (zero_extend[1] ?e47))) +(flet ($e197 (= ?e14 (zero_extend[5] ?e59))) +(flet ($e198 (= ?e75 (sign_extend[6] ?e43))) +(flet ($e199 (= (zero_extend[12] v1) ?e57)) +(flet ($e200 (= ?e23 ?e50)) +(flet ($e201 (= (sign_extend[1] ?e70) ?e54)) +(flet ($e202 (= ?e45 ?e26)) +(flet ($e203 (= v2 (sign_extend[2] ?e41))) +(flet ($e204 (= ?e45 ?e62)) +(flet ($e205 (= (zero_extend[1] ?e32) ?e19)) +(flet ($e206 (= ?e49 (zero_extend[1] ?e81))) +(flet ($e207 (= ?e89 (zero_extend[6] ?e26))) +(flet ($e208 (= (sign_extend[4] ?e87) v0)) +(flet ($e209 (= ?e13 ?e4)) +(flet ($e210 (= v2 (sign_extend[2] ?e33))) +(flet ($e211 (= ?e66 (zero_extend[14] ?e61))) +(flet ($e212 (= (zero_extend[1] ?e24) ?e80)) +(flet ($e213 (= ?e5 ?e21)) +(flet ($e214 (= ?e21 ?e16)) +(flet ($e215 (= (zero_extend[13] ?e22) ?e57)) +(flet ($e216 (= ?e33 (zero_extend[1] ?e47))) +(flet ($e217 (= (sign_extend[4] ?e71) ?e76)) +(flet ($e218 (= (zero_extend[4] ?e86) ?e69)) +(flet ($e219 (= ?e63 ?e63)) +(flet ($e220 (= (zero_extend[1] ?e44) ?e33)) +(flet ($e221 (= ?e8 (zero_extend[3] ?e62))) +(flet ($e222 (= ?e71 ?e60)) +(flet ($e223 (= ?e56 ?e55)) +(flet ($e224 (= ?e48 ?e85)) +(flet ($e225 (= ?e52 (zero_extend[1] ?e27))) +(flet ($e226 (= ?e4 (sign_extend[1] ?e36))) +(flet ($e227 (= (sign_extend[1] ?e38) ?e49)) +(flet ($e228 (= ?e7 ?e11)) +(flet ($e229 (= (zero_extend[3] ?e44) v2)) +(flet ($e230 (= (zero_extend[4] ?e58) ?e88)) +(flet ($e231 (= ?e85 ?e5)) +(flet ($e232 (= ?e16 (zero_extend[1] ?e86))) +(flet ($e233 (= ?e75 (sign_extend[7] ?e12))) +(flet ($e234 (= ?e9 ?e9)) +(flet ($e235 (= ?e4 (sign_extend[1] ?e22))) +(flet ($e236 (= ?e84 (zero_extend[4] ?e70))) +(flet ($e237 (= ?e41 ?e29)) +(flet ($e238 (and $e142 $e200)) +(flet ($e239 (xor $e187 $e214)) +(flet ($e240 (or $e136 $e160)) +(flet ($e241 (xor $e144 $e224)) +(flet ($e242 (and $e151 $e181)) +(flet ($e243 (if_then_else $e158 $e141 $e148)) +(flet ($e244 (iff $e218 $e164)) +(flet ($e245 (iff $e92 $e156)) +(flet ($e246 (xor $e183 $e155)) +(flet ($e247 (xor $e134 $e185)) +(flet ($e248 (xor $e219 $e178)) +(flet ($e249 (if_then_else $e174 $e132 $e212)) +(flet ($e250 (implies $e152 $e246)) +(flet ($e251 (or $e194 $e215)) +(flet ($e252 (iff $e204 $e137)) +(flet ($e253 (and $e249 $e135)) +(flet ($e254 (xor $e115 $e171)) +(flet ($e255 (implies $e192 $e105)) +(flet ($e256 (or $e201 $e95)) +(flet ($e257 (or $e250 $e175)) +(flet ($e258 (xor $e213 $e113)) +(flet ($e259 (if_then_else $e248 $e143 $e248)) +(flet ($e260 (implies $e179 $e163)) +(flet ($e261 (and $e220 $e227)) +(flet ($e262 (xor $e261 $e193)) +(flet ($e263 (iff $e190 $e233)) +(flet ($e264 (or $e239 $e159)) +(flet ($e265 (or $e221 $e149)) +(flet ($e266 (not $e150)) +(flet ($e267 (or $e103 $e109)) +(flet ($e268 (implies $e139 $e262)) +(flet ($e269 (implies $e231 $e217)) +(flet ($e270 (not $e138)) +(flet ($e271 (or $e235 $e147)) +(flet ($e272 (and $e131 $e166)) +(flet ($e273 (xor $e207 $e191)) +(flet ($e274 (or $e123 $e91)) +(flet ($e275 (implies $e259 $e222)) +(flet ($e276 (not $e275)) +(flet ($e277 (if_then_else $e114 $e165 $e276)) +(flet ($e278 (and $e243 $e264)) +(flet ($e279 (implies $e154 $e273)) +(flet ($e280 (if_then_else $e119 $e236 $e226)) +(flet ($e281 (or $e228 $e176)) +(flet ($e282 (not $e229)) +(flet ($e283 (not $e208)) +(flet ($e284 (not $e128)) +(flet ($e285 (or $e230 $e254)) +(flet ($e286 (xor $e118 $e253)) +(flet ($e287 (not $e146)) +(flet ($e288 (not $e98)) +(flet ($e289 (or $e210 $e121)) +(flet ($e290 (not $e189)) +(flet ($e291 (and $e279 $e157)) +(flet ($e292 (implies $e117 $e281)) +(flet ($e293 (iff $e206 $e282)) +(flet ($e294 (iff $e101 $e172)) +(flet ($e295 (iff $e184 $e173)) +(flet ($e296 (or $e272 $e257)) +(flet ($e297 (and $e104 $e244)) +(flet ($e298 (if_then_else $e122 $e284 $e202)) +(flet ($e299 (not $e140)) +(flet ($e300 (not $e145)) +(flet ($e301 (not $e274)) +(flet ($e302 (implies $e170 $e205)) +(flet ($e303 (xor $e153 $e97)) +(flet ($e304 (if_then_else $e265 $e300 $e96)) +(flet ($e305 (xor $e255 $e296)) +(flet ($e306 (and $e294 $e267)) +(flet ($e307 (xor $e297 $e209)) +(flet ($e308 (or $e127 $e278)) +(flet ($e309 (if_then_else $e238 $e232 $e280)) +(flet ($e310 (or $e129 $e182)) +(flet ($e311 (iff $e100 $e216)) +(flet ($e312 (implies $e295 $e203)) +(flet ($e313 (if_then_else $e309 $e309 $e167)) +(flet ($e314 (iff $e162 $e289)) +(flet ($e315 (if_then_else $e130 $e234 $e304)) +(flet ($e316 (if_then_else $e251 $e94 $e195)) +(flet ($e317 (xor $e285 $e112)) +(flet ($e318 (or $e93 $e308)) +(flet ($e319 (or $e252 $e168)) +(flet ($e320 (not $e292)) +(flet ($e321 (if_then_else $e111 $e198 $e196)) +(flet ($e322 (not $e277)) +(flet ($e323 (if_then_else $e268 $e319 $e293)) +(flet ($e324 (or $e161 $e245)) +(flet ($e325 (or $e317 $e177)) +(flet ($e326 (if_then_else $e311 $e197 $e323)) +(flet ($e327 (or $e241 $e266)) +(flet ($e328 (and $e327 $e288)) +(flet ($e329 (not $e124)) +(flet ($e330 (and $e126 $e302)) +(flet ($e331 (if_then_else $e169 $e240 $e326)) +(flet ($e332 (if_then_else $e225 $e269 $e328)) +(flet ($e333 (and $e99 $e314)) +(flet ($e334 (not $e298)) +(flet ($e335 (implies $e263 $e283)) +(flet ($e336 (and $e313 $e331)) +(flet ($e337 (or $e258 $e325)) +(flet ($e338 (iff $e120 $e299)) +(flet ($e339 (xor $e211 $e306)) +(flet ($e340 (not $e106)) +(flet ($e341 (iff $e301 $e320)) +(flet ($e342 (if_then_else $e223 $e287 $e223)) +(flet ($e343 (or $e188 $e307)) +(flet ($e344 (xor $e247 $e199)) +(flet ($e345 (if_then_else $e260 $e286 $e318)) +(flet ($e346 (implies $e256 $e337)) +(flet ($e347 (and $e329 $e186)) +(flet ($e348 (if_then_else $e291 $e339 $e107)) +(flet ($e349 (not $e316)) +(flet ($e350 (if_then_else $e305 $e116 $e348)) +(flet ($e351 (not $e125)) +(flet ($e352 (and $e335 $e321)) +(flet ($e353 (not $e338)) +(flet ($e354 (iff $e336 $e180)) +(flet ($e355 (and $e345 $e347)) +(flet ($e356 (not $e350)) +(flet ($e357 (iff $e102 $e237)) +(flet ($e358 (if_then_else $e312 $e322 $e133)) +(flet ($e359 (or $e344 $e333)) +(flet ($e360 (xor $e332 $e315)) +(flet ($e361 (implies $e110 $e324)) +(flet ($e362 (implies $e360 $e349)) +(flet ($e363 (or $e342 $e330)) +(flet ($e364 (implies $e270 $e270)) +(flet ($e365 (and $e361 $e108)) +(flet ($e366 (and $e341 $e346)) +(flet ($e367 (xor $e352 $e343)) +(flet ($e368 (iff $e353 $e362)) +(flet ($e369 (iff $e310 $e357)) +(flet ($e370 (if_then_else $e355 $e303 $e354)) +(flet ($e371 (iff $e364 $e370)) +(flet ($e372 (not $e367)) +(flet ($e373 (if_then_else $e368 $e371 $e366)) +(flet ($e374 (or $e340 $e351)) +(flet ($e375 (xor $e334 $e271)) +(flet ($e376 (and $e373 $e374)) +(flet ($e377 (if_then_else $e369 $e242 $e358)) +(flet ($e378 (implies $e363 $e363)) +(flet ($e379 (xor $e365 $e378)) +(flet ($e380 (iff $e375 $e377)) +(flet ($e381 (or $e372 $e372)) +(flet ($e382 (xor $e380 $e356)) +(flet ($e383 (implies $e379 $e359)) +(flet ($e384 (implies $e376 $e290)) +(flet ($e385 (iff $e384 $e383)) +(flet ($e386 (implies $e382 $e385)) +(flet ($e387 (or $e381 $e386)) +$e387 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/bv/fuzz08.smt b/test/regress/regress0/bv/fuzz08.smt new file mode 100644 index 000000000..e2a73db50 --- /dev/null +++ b/test/regress/regress0/bv/fuzz08.smt @@ -0,0 +1,19 @@ +(benchmark fuzzsmt +:logic QF_BV +:extrafuns ((v1 BitVec[9])) +:status sat +:formula +(let (?n1 bv0[6]) +(let (?n2 bv0[9]) +(flet ($n3 (bvult ?n2 v1)) +(let (?n4 bv1[1]) +(let (?n5 bv0[1]) +(let (?n6 (ite $n3 ?n4 ?n5)) +(let (?n7 (sign_extend[5] ?n6)) +(flet ($n8 (bvsgt ?n1 ?n7)) +(let (?n9 (ite $n8 ?n4 ?n5)) +(let (?n10 (sign_extend[8] ?n9)) +(let (?n11 (bvcomp v1 ?n10)) +(flet ($n12 (= ?n9 ?n11)) +$n12 +))))))))))))) diff --git a/test/regress/regress0/bv/fuzz09.smt b/test/regress/regress0/bv/fuzz09.smt new file mode 100644 index 000000000..ce8e9bfd6 --- /dev/null +++ b/test/regress/regress0/bv/fuzz09.smt @@ -0,0 +1,370 @@ +(benchmark fuzzsmt +:logic QF_BV +:status sat +:extrafuns ((v0 BitVec[7])) +:extrafuns ((v1 BitVec[5])) +:extrafuns ((v2 BitVec[13])) +:extrafuns ((v3 BitVec[16])) +:formula +(let (?e4 bv15872[14]) +(let (?e5 bv148[12]) +(let (?e6 (repeat[1] v2)) +(let (?e7 (ite (bvugt (sign_extend[6] v0) ?e6) bv1[1] bv0[1])) +(let (?e8 (bvnor (sign_extend[2] v1) v0)) +(let (?e9 (sign_extend[1] v2)) +(let (?e10 (ite (bvsgt (sign_extend[6] v0) v2) bv1[1] bv0[1])) +(let (?e11 (concat v0 v1)) +(let (?e12 (bvneg ?e6)) +(let (?e13 (bvsub (sign_extend[8] v1) v2)) +(let (?e14 (ite (bvule (sign_extend[13] ?e7) ?e9) bv1[1] bv0[1])) +(let (?e15 (ite (bvult v1 (zero_extend[4] ?e7)) bv1[1] bv0[1])) +(let (?e16 (bvnand (sign_extend[1] ?e5) v2)) +(let (?e17 (bvor ?e9 (sign_extend[9] v1))) +(let (?e18 (bvxnor ?e9 (sign_extend[7] v0))) +(let (?e19 (bvmul (sign_extend[1] ?e11) ?e16)) +(let (?e20 (bvand ?e18 (sign_extend[13] ?e14))) +(let (?e21 (bvsub (zero_extend[12] ?e7) v2)) +(let (?e22 (bvmul ?e18 (zero_extend[7] v0))) +(let (?e23 (rotate_right[13] ?e20)) +(let (?e24 (ite (bvult ?e22 (zero_extend[1] v2)) bv1[1] bv0[1])) +(let (?e25 (bvneg ?e19)) +(let (?e26 (ite (bvult ?e5 (zero_extend[11] ?e10)) bv1[1] bv0[1])) +(let (?e27 (bvxor ?e22 ?e4)) +(let (?e28 (ite (distinct (sign_extend[1] ?e5) ?e21) bv1[1] bv0[1])) +(let (?e29 (bvlshr ?e6 (zero_extend[6] v0))) +(let (?e30 (bvashr ?e10 ?e28)) +(let (?e31 (bvmul ?e24 ?e26)) +(let (?e32 (bvnand (sign_extend[2] ?e5) ?e20)) +(let (?e33 (bvxor v1 (sign_extend[4] ?e31))) +(let (?e34 (bvor ?e26 ?e7)) +(let (?e35 (bvnot ?e6)) +(let (?e36 (extract[10:5] ?e21)) +(let (?e37 (ite (= ?e31 ?e15) bv1[1] bv0[1])) +(let (?e38 (bvnot ?e11)) +(let (?e39 (extract[5:5] ?e13)) +(let (?e40 (bvadd (zero_extend[12] ?e24) ?e29)) +(let (?e41 (bvshl ?e13 (zero_extend[12] ?e7))) +(let (?e42 (ite (bvuge ?e4 (zero_extend[1] ?e13)) bv1[1] bv0[1])) +(let (?e43 (bvor (sign_extend[13] ?e15) ?e22)) +(let (?e44 (ite (bvsle ?e25 (zero_extend[6] v0)) bv1[1] bv0[1])) +(let (?e45 (ite (bvslt ?e19 (sign_extend[8] v1)) bv1[1] bv0[1])) +(let (?e46 (bvshl (zero_extend[1] ?e35) ?e22)) +(let (?e47 (sign_extend[4] ?e7)) +(let (?e48 (bvxor ?e6 (zero_extend[12] ?e30))) +(let (?e49 (bvand v0 v0)) +(let (?e50 (bvand (sign_extend[12] ?e28) ?e16)) +(let (?e51 (bvmul (sign_extend[12] ?e34) ?e21)) +(let (?e52 (sign_extend[15] ?e45)) +(let (?e53 (bvnot ?e23)) +(let (?e54 (extract[5:3] ?e12)) +(let (?e55 (ite (bvslt (zero_extend[15] ?e42) ?e52) bv1[1] bv0[1])) +(let (?e56 (bvneg ?e6)) +(let (?e57 (repeat[3] ?e47)) +(let (?e58 (ite (bvsle ?e38 (sign_extend[11] ?e44)) bv1[1] bv0[1])) +(let (?e59 (sign_extend[0] ?e21)) +(let (?e60 (ite (bvsle ?e22 (zero_extend[13] ?e58)) bv1[1] bv0[1])) +(let (?e61 (bvadd ?e7 ?e37)) +(let (?e62 (bvnor v3 (zero_extend[3] ?e50))) +(flet ($e63 (= ?e46 (zero_extend[13] ?e7))) +(flet ($e64 (= (zero_extend[12] ?e30) ?e29)) +(flet ($e65 (= (zero_extend[10] ?e54) ?e6)) +(flet ($e66 (= ?e20 (sign_extend[13] ?e44))) +(flet ($e67 (= ?e43 (zero_extend[1] ?e19))) +(flet ($e68 (= ?e9 (sign_extend[8] ?e36))) +(flet ($e69 (= ?e56 (zero_extend[6] ?e49))) +(flet ($e70 (= ?e52 (sign_extend[3] v2))) +(flet ($e71 (= ?e6 (zero_extend[8] ?e47))) +(flet ($e72 (= ?e56 (zero_extend[6] v0))) +(flet ($e73 (= ?e33 (zero_extend[4] ?e34))) +(flet ($e74 (= ?e32 ?e27)) +(flet ($e75 (= ?e12 (sign_extend[12] ?e34))) +(flet ($e76 (= ?e21 ?e6)) +(flet ($e77 (= (sign_extend[12] ?e37) v2)) +(flet ($e78 (= ?e36 (sign_extend[5] ?e30))) +(flet ($e79 (= v2 ?e13)) +(flet ($e80 (= (zero_extend[12] ?e55) ?e56)) +(flet ($e81 (= ?e52 (zero_extend[2] ?e9))) +(flet ($e82 (= (sign_extend[12] ?e55) ?e13)) +(flet ($e83 (= ?e57 (sign_extend[1] ?e23))) +(flet ($e84 (= (zero_extend[7] v0) ?e27)) +(flet ($e85 (= (sign_extend[15] ?e14) v3)) +(flet ($e86 (= ?e62 (sign_extend[2] ?e9))) +(flet ($e87 (= (zero_extend[13] ?e31) ?e23)) +(flet ($e88 (= (zero_extend[2] ?e5) ?e46)) +(flet ($e89 (= ?e12 (zero_extend[1] ?e38))) +(flet ($e90 (= ?e13 (zero_extend[12] ?e61))) +(flet ($e91 (= (zero_extend[12] ?e30) ?e12)) +(flet ($e92 (= (zero_extend[4] ?e61) ?e33)) +(flet ($e93 (= ?e32 (sign_extend[1] ?e12))) +(flet ($e94 (= ?e40 (sign_extend[12] ?e31))) +(flet ($e95 (= (sign_extend[11] ?e28) ?e38)) +(flet ($e96 (= ?e36 (sign_extend[5] ?e26))) +(flet ($e97 (= ?e6 ?e35)) +(flet ($e98 (= ?e52 (zero_extend[9] ?e8))) +(flet ($e99 (= (sign_extend[7] ?e8) ?e53)) +(flet ($e100 (= (zero_extend[12] ?e42) ?e21)) +(flet ($e101 (= ?e46 (sign_extend[1] ?e51))) +(flet ($e102 (= ?e46 (zero_extend[13] ?e26))) +(flet ($e103 (= ?e31 ?e15)) +(flet ($e104 (= ?e59 (sign_extend[12] ?e7))) +(flet ($e105 (= (sign_extend[12] ?e45) ?e48)) +(flet ($e106 (= ?e4 ?e4)) +(flet ($e107 (= ?e52 (sign_extend[4] ?e38))) +(flet ($e108 (= ?e62 (sign_extend[3] ?e56))) +(flet ($e109 (= ?e37 ?e60)) +(flet ($e110 (= (sign_extend[1] ?e36) ?e8)) +(flet ($e111 (= (sign_extend[1] ?e29) ?e22)) +(flet ($e112 (= ?e53 (sign_extend[13] ?e44))) +(flet ($e113 (= ?e27 (sign_extend[13] ?e31))) +(flet ($e114 (= (sign_extend[1] ?e59) ?e9)) +(flet ($e115 (= (zero_extend[1] ?e16) ?e22)) +(flet ($e116 (= (zero_extend[13] ?e7) ?e9)) +(flet ($e117 (= ?e40 ?e35)) +(flet ($e118 (= (zero_extend[13] ?e60) ?e22)) +(flet ($e119 (= ?e50 (sign_extend[1] ?e38))) +(flet ($e120 (= ?e56 ?e35)) +(flet ($e121 (= ?e16 (sign_extend[12] ?e7))) +(flet ($e122 (= (zero_extend[1] ?e5) ?e59)) +(flet ($e123 (= (sign_extend[7] ?e8) ?e22)) +(flet ($e124 (= ?e9 (sign_extend[1] v2))) +(flet ($e125 (= (zero_extend[2] ?e39) ?e54)) +(flet ($e126 (= ?e36 (sign_extend[5] ?e34))) +(flet ($e127 (= (zero_extend[9] ?e8) v3)) +(flet ($e128 (= ?e23 (zero_extend[2] ?e11))) +(flet ($e129 (= (sign_extend[12] ?e55) ?e56)) +(flet ($e130 (= ?e57 (sign_extend[10] ?e33))) +(flet ($e131 (= ?e23 ?e32)) +(flet ($e132 (= ?e62 (zero_extend[15] ?e58))) +(flet ($e133 (= ?e30 ?e42)) +(flet ($e134 (= ?e26 ?e7)) +(flet ($e135 (= v2 ?e21)) +(flet ($e136 (= ?e53 ?e23)) +(flet ($e137 (= ?e23 (sign_extend[13] ?e37))) +(flet ($e138 (= (sign_extend[13] ?e24) ?e53)) +(flet ($e139 (= (zero_extend[1] ?e13) ?e17)) +(flet ($e140 (= ?e58 ?e7)) +(flet ($e141 (= ?e6 (zero_extend[12] ?e14))) +(flet ($e142 (= ?e15 ?e37)) +(flet ($e143 (= ?e16 (sign_extend[12] ?e39))) +(flet ($e144 (= (zero_extend[12] ?e58) ?e59)) +(flet ($e145 (= ?e52 (sign_extend[2] ?e27))) +(flet ($e146 (= (zero_extend[15] ?e15) ?e52)) +(flet ($e147 (= ?e43 (sign_extend[1] ?e56))) +(flet ($e148 (= (zero_extend[10] ?e54) ?e35)) +(flet ($e149 (= ?e20 (zero_extend[13] ?e34))) +(flet ($e150 (= (sign_extend[12] ?e44) ?e41)) +(flet ($e151 (= ?e41 (sign_extend[12] ?e34))) +(flet ($e152 (= ?e18 (zero_extend[13] ?e55))) +(flet ($e153 (= (zero_extend[2] ?e9) v3)) +(flet ($e154 (= (sign_extend[13] ?e45) ?e43)) +(flet ($e155 (= ?e40 ?e35)) +(flet ($e156 (= ?e19 (zero_extend[12] ?e61))) +(flet ($e157 (= (zero_extend[1] ?e5) ?e59)) +(flet ($e158 (= ?e35 (zero_extend[12] ?e37))) +(flet ($e159 (= ?e53 ?e43)) +(flet ($e160 (= ?e32 (zero_extend[2] ?e5))) +(flet ($e161 (= ?e54 (sign_extend[2] ?e55))) +(flet ($e162 (= ?e51 ?e12)) +(flet ($e163 (= (sign_extend[12] ?e34) ?e6)) +(flet ($e164 (= ?e17 ?e53)) +(flet ($e165 (= ?e53 ?e9)) +(flet ($e166 (= ?e8 (sign_extend[6] ?e10))) +(flet ($e167 (= ?e10 ?e24)) +(flet ($e168 (= (sign_extend[11] ?e47) ?e62)) +(flet ($e169 (= (zero_extend[12] ?e42) v2)) +(flet ($e170 (= (sign_extend[11] ?e15) ?e5)) +(flet ($e171 (= (zero_extend[12] ?e45) v2)) +(flet ($e172 (= (zero_extend[1] ?e56) ?e20)) +(flet ($e173 (= ?e5 (sign_extend[7] v1))) +(flet ($e174 (= ?e36 (sign_extend[3] ?e54))) +(flet ($e175 (= ?e6 (sign_extend[12] ?e31))) +(flet ($e176 (= (sign_extend[13] ?e42) ?e22)) +(flet ($e177 (= (sign_extend[2] ?e17) ?e62)) +(flet ($e178 (= (sign_extend[7] ?e33) ?e11)) +(flet ($e179 (= ?e27 (zero_extend[13] ?e14))) +(flet ($e180 (= (zero_extend[2] v2) ?e57)) +(flet ($e181 (= v3 (zero_extend[3] ?e40))) +(flet ($e182 (= ?e30 ?e24)) +(flet ($e183 (= (sign_extend[11] ?e30) ?e11)) +(flet ($e184 (= ?e17 (zero_extend[9] ?e33))) +(flet ($e185 (= (sign_extend[7] ?e36) ?e51)) +(flet ($e186 (= (zero_extend[13] ?e61) ?e23)) +(flet ($e187 (= (sign_extend[15] ?e44) ?e52)) +(flet ($e188 (= ?e39 ?e34)) +(flet ($e189 (= ?e59 (sign_extend[12] ?e55))) +(flet ($e190 (= v2 ?e16)) +(flet ($e191 (= ?e36 (zero_extend[5] ?e24))) +(flet ($e192 (= (sign_extend[12] ?e10) ?e41)) +(flet ($e193 (= ?e57 (zero_extend[2] ?e6))) +(flet ($e194 (= ?e31 ?e10)) +(flet ($e195 (= ?e38 (zero_extend[11] ?e58))) +(flet ($e196 (= ?e27 (zero_extend[13] ?e58))) +(flet ($e197 (= (zero_extend[13] ?e60) ?e4)) +(flet ($e198 (= ?e50 (sign_extend[12] ?e39))) +(flet ($e199 (= ?e20 ?e32)) +(flet ($e200 (= (zero_extend[1] ?e12) ?e22)) +(flet ($e201 (= ?e51 (sign_extend[12] ?e14))) +(flet ($e202 (= (sign_extend[2] ?e4) v3)) +(flet ($e203 (= (sign_extend[8] ?e36) ?e20)) +(flet ($e204 (= ?e62 (zero_extend[15] ?e42))) +(flet ($e205 (= ?e21 (sign_extend[8] v1))) +(flet ($e206 (= ?e33 (zero_extend[4] ?e60))) +(flet ($e207 (= ?e55 ?e45)) +(flet ($e208 (= ?e55 ?e45)) +(flet ($e209 (= (zero_extend[13] ?e44) ?e20)) +(flet ($e210 (= (zero_extend[1] ?e11) ?e51)) +(flet ($e211 (= v3 (zero_extend[2] ?e27))) +(flet ($e212 (= ?e25 ?e21)) +(flet ($e213 (iff $e200 $e110)) +(flet ($e214 (iff $e209 $e138)) +(flet ($e215 (if_then_else $e204 $e156 $e75)) +(flet ($e216 (xor $e191 $e126)) +(flet ($e217 (and $e175 $e151)) +(flet ($e218 (xor $e80 $e196)) +(flet ($e219 (xor $e202 $e187)) +(flet ($e220 (and $e114 $e163)) +(flet ($e221 (or $e63 $e203)) +(flet ($e222 (implies $e131 $e134)) +(flet ($e223 (iff $e152 $e108)) +(flet ($e224 (xor $e119 $e85)) +(flet ($e225 (not $e184)) +(flet ($e226 (implies $e88 $e213)) +(flet ($e227 (not $e161)) +(flet ($e228 (if_then_else $e201 $e103 $e112)) +(flet ($e229 (not $e118)) +(flet ($e230 (and $e82 $e122)) +(flet ($e231 (implies $e90 $e149)) +(flet ($e232 (implies $e120 $e193)) +(flet ($e233 (xor $e109 $e140)) +(flet ($e234 (or $e190 $e113)) +(flet ($e235 (or $e228 $e150)) +(flet ($e236 (or $e76 $e220)) +(flet ($e237 (iff $e144 $e155)) +(flet ($e238 (or $e142 $e159)) +(flet ($e239 (if_then_else $e222 $e158 $e100)) +(flet ($e240 (not $e129)) +(flet ($e241 (and $e164 $e179)) +(flet ($e242 (implies $e73 $e226)) +(flet ($e243 (xor $e166 $e66)) +(flet ($e244 (iff $e168 $e102)) +(flet ($e245 (not $e86)) +(flet ($e246 (if_then_else $e244 $e183 $e83)) +(flet ($e247 (if_then_else $e137 $e225 $e236)) +(flet ($e248 (if_then_else $e79 $e171 $e239)) +(flet ($e249 (xor $e217 $e176)) +(flet ($e250 (xor $e249 $e145)) +(flet ($e251 (implies $e194 $e195)) +(flet ($e252 (iff $e197 $e206)) +(flet ($e253 (xor $e95 $e243)) +(flet ($e254 (xor $e98 $e218)) +(flet ($e255 (not $e157)) +(flet ($e256 (if_then_else $e182 $e221 $e115)) +(flet ($e257 (or $e216 $e177)) +(flet ($e258 (iff $e139 $e235)) +(flet ($e259 (not $e172)) +(flet ($e260 (not $e77)) +(flet ($e261 (and $e180 $e125)) +(flet ($e262 (or $e91 $e87)) +(flet ($e263 (not $e135)) +(flet ($e264 (implies $e130 $e232)) +(flet ($e265 (if_then_else $e240 $e111 $e123)) +(flet ($e266 (not $e121)) +(flet ($e267 (xor $e199 $e147)) +(flet ($e268 (xor $e74 $e170)) +(flet ($e269 (implies $e192 $e267)) +(flet ($e270 (implies $e245 $e65)) +(flet ($e271 (implies $e230 $e148)) +(flet ($e272 (implies $e264 $e205)) +(flet ($e273 (and $e143 $e78)) +(flet ($e274 (not $e257)) +(flet ($e275 (xor $e261 $e167)) +(flet ($e276 (not $e268)) +(flet ($e277 (iff $e93 $e260)) +(flet ($e278 (if_then_else $e242 $e258 $e247)) +(flet ($e279 (if_then_else $e252 $e116 $e214)) +(flet ($e280 (implies $e259 $e189)) +(flet ($e281 (not $e141)) +(flet ($e282 (if_then_else $e96 $e208 $e127)) +(flet ($e283 (iff $e211 $e165)) +(flet ($e284 (implies $e255 $e185)) +(flet ($e285 (if_then_else $e278 $e162 $e272)) +(flet ($e286 (and $e128 $e282)) +(flet ($e287 (or $e263 $e273)) +(flet ($e288 (or $e106 $e215)) +(flet ($e289 (not $e71)) +(flet ($e290 (iff $e207 $e250)) +(flet ($e291 (or $e68 $e68)) +(flet ($e292 (implies $e72 $e212)) +(flet ($e293 (implies $e254 $e277)) +(flet ($e294 (not $e280)) +(flet ($e295 (not $e274)) +(flet ($e296 (implies $e256 $e233)) +(flet ($e297 (implies $e275 $e64)) +(flet ($e298 (or $e234 $e248)) +(flet ($e299 (or $e153 $e223)) +(flet ($e300 (if_then_else $e286 $e224 $e276)) +(flet ($e301 (or $e94 $e124)) +(flet ($e302 (or $e279 $e287)) +(flet ($e303 (if_then_else $e302 $e292 $e174)) +(flet ($e304 (if_then_else $e265 $e104 $e294)) +(flet ($e305 (or $e186 $e173)) +(flet ($e306 (if_then_else $e270 $e133 $e288)) +(flet ($e307 (and $e81 $e305)) +(flet ($e308 (xor $e293 $e291)) +(flet ($e309 (iff $e84 $e303)) +(flet ($e310 (xor $e262 $e284)) +(flet ($e311 (iff $e297 $e178)) +(flet ($e312 (iff $e198 $e132)) +(flet ($e313 (if_then_else $e169 $e304 $e146)) +(flet ($e314 (if_then_else $e306 $e285 $e307)) +(flet ($e315 (and $e281 $e289)) +(flet ($e316 (if_then_else $e309 $e299 $e97)) +(flet ($e317 (or $e266 $e117)) +(flet ($e318 (and $e227 $e301)) +(flet ($e319 (or $e300 $e317)) +(flet ($e320 (iff $e313 $e237)) +(flet ($e321 (or $e241 $e318)) +(flet ($e322 (and $e308 $e188)) +(flet ($e323 (xor $e269 $e154)) +(flet ($e324 (xor $e69 $e246)) +(flet ($e325 (or $e310 $e296)) +(flet ($e326 (implies $e136 $e311)) +(flet ($e327 (or $e326 $e160)) +(flet ($e328 (if_then_else $e295 $e238 $e229)) +(flet ($e329 (or $e316 $e322)) +(flet ($e330 (and $e319 $e89)) +(flet ($e331 (not $e298)) +(flet ($e332 (or $e219 $e92)) +(flet ($e333 (implies $e324 $e271)) +(flet ($e334 (iff $e251 $e323)) +(flet ($e335 (xor $e181 $e327)) +(flet ($e336 (implies $e331 $e210)) +(flet ($e337 (implies $e231 $e290)) +(flet ($e338 (iff $e312 $e99)) +(flet ($e339 (implies $e105 $e337)) +(flet ($e340 (implies $e325 $e339)) +(flet ($e341 (xor $e335 $e101)) +(flet ($e342 (iff $e253 $e330)) +(flet ($e343 (iff $e328 $e341)) +(flet ($e344 (and $e321 $e340)) +(flet ($e345 (and $e314 $e343)) +(flet ($e346 (iff $e333 $e329)) +(flet ($e347 (not $e70)) +(flet ($e348 (or $e283 $e107)) +(flet ($e349 (or $e336 $e345)) +(flet ($e350 (not $e332)) +(flet ($e351 (and $e315 $e342)) +(flet ($e352 (xor $e349 $e348)) +(flet ($e353 (xor $e67 $e344)) +(flet ($e354 (not $e334)) +(flet ($e355 (and $e354 $e352)) +(flet ($e356 (if_then_else $e351 $e355 $e347)) +(flet ($e357 (and $e346 $e320)) +(flet ($e358 (iff $e350 $e338)) +(flet ($e359 (not $e353)) +(flet ($e360 (or $e359 $e357)) +(flet ($e361 (xor $e360 $e356)) +(flet ($e362 (implies $e361 $e358)) +$e362 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |