more tests

tests/regress/mcsat/0e4fd0ab.smt2

@@ -0,0 +1,133 @@
+(set-info :source |fuzzsmt|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "random")
+(set-info :status unknown)
+(set-logic QF_AUFBV)
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 12))
+(declare-fun a2 () (Array  (_ BitVec 13)  (_ BitVec 14)))
+(assert (let ((e3(_ bv58043 16)))
+(let ((e4(_ bv4992 13)))
+(let ((e5 (bvurem ((_ sign_extend 1) v1) e4)))
+(let ((e6 (bvsub e3 ((_ sign_extend 3) e4))))
+(let ((e7 (ite (bvsge v0 e3) (_ bv1 1) (_ bv0 1))))
+(let ((e8 (store a2 ((_ extract 14 2) v0) ((_ sign_extend 2) v1))))
+(let ((e9 (store e8 e4 ((_ extract 14 1) e6))))
+(let ((e10 (store e8 e5 ((_ extract 15 2) e6))))
+(let ((e11 (select a2 ((_ sign_extend 12) e7))))
+(let ((e12 (select a2 ((_ sign_extend 12) e7))))
+(let ((e13 (select e9 ((_ extract 15 3) v0))))
+(let ((e14 (store e10 e5 ((_ sign_extend 13) e7))))
+(let ((e15 (select e10 ((_ sign_extend 12) e7))))
+(let ((e16 (store e10 e5 ((_ extract 15 2) e3))))
+(let ((e17 (select e10 ((_ extract 14 2) e3))))
+(let ((e18 (bvxnor e4 e5)))
+(let ((e19 (ite (bvule e15 e12) (_ bv1 1) (_ bv0 1))))
+(let ((e20 (ite (bvule v0 e3) (_ bv1 1) (_ bv0 1))))
+(let ((e21 (bvand e17 e12)))
+(let ((e22 (bvxor ((_ sign_extend 2) e15) v0)))
+(let ((e23 (bvmul e6 ((_ sign_extend 2) e11))))
+(let ((e24 (ite (bvugt ((_ sign_extend 4) v1) e6) (_ bv1 1) (_ bv0 1))))
+(let ((e25 (bvnand v0 ((_ sign_extend 3) e4))))
+(let ((e26 (bvneg e19)))
+(let ((e27 (bvlshr e25 v0)))
+(let ((e28 (bvashr e13 e17)))
+(let ((e29 (bvcomp ((_ sign_extend 13) e7) e12)))
+(let ((e30 (bvsge e6 ((_ zero_extend 2) e12))))
+(let ((e31 (bvsge ((_ sign_extend 2) e11) e6)))
+(let ((e32 (bvule e15 ((_ sign_extend 13) e26))))
+(let ((e33 (= e13 e13)))
+(let ((e34 (bvugt v0 ((_ sign_extend 2) e11))))
+(let ((e35 (bvslt ((_ sign_extend 2) v1) e13)))
+(let ((e36 (= e11 ((_ sign_extend 1) e5))))
+(let ((e37 (bvslt e15 ((_ zero_extend 1) e18))))
+(let ((e38 (bvule e11 ((_ sign_extend 13) e24))))
+(let ((e39 (bvsgt e27 e23)))
+(let ((e40 (bvuge e11 ((_ sign_extend 2) v1))))
+(let ((e41 (bvsgt ((_ sign_extend 2) e11) e27)))
+(let ((e42 (bvugt v1 ((_ zero_extend 11) e29))))
+(let ((e43 (bvslt e17 ((_ zero_extend 13) e19))))
+(let ((e44 (bvult ((_ zero_extend 1) e5) e11)))
+(let ((e45 (= e27 ((_ sign_extend 15) e19))))
+(let ((e46 (bvult v0 ((_ sign_extend 2) e11))))
+(let ((e47 (bvslt e25 ((_ sign_extend 3) e18))))
+(let ((e48 (bvsgt v1 v1)))
+(let ((e49 (bvult e17 ((_ sign_extend 13) e7))))
+(let ((e50 (bvsgt ((_ sign_extend 12) e7) e18)))
+(let ((e51 (bvsle e15 ((_ zero_extend 13) e7))))
+(let ((e52 (bvule ((_ sign_extend 13) e26) e13)))
+(let ((e53 (bvult ((_ zero_extend 2) e17) e3)))
+(let ((e54 (= ((_ sign_extend 4) v1) v0)))
+(let ((e55 (bvsle e23 ((_ sign_extend 15) e29))))
+(let ((e56 (bvule e17 e28)))
+(let ((e57 (bvsle ((_ zero_extend 15) e19) e6)))
+(let ((e58 (bvsge e22 ((_ sign_extend 3) e5))))
+(let ((e59 (distinct ((_ sign_extend 2) e17) v0)))
+(let ((e60 (bvult ((_ zero_extend 15) e7) e6)))
+(let ((e61 (bvslt ((_ sign_extend 2) e13) e6)))
+(let ((e62 (bvule ((_ zero_extend 12) e19) e4)))
+(let ((e63 (bvsgt e17 e17)))
+(let ((e64 (bvslt ((_ zero_extend 13) e20) e17)))
+(let ((e65 (bvult ((_ sign_extend 13) e19) e17)))
+(let ((e66 (bvule v0 ((_ sign_extend 2) e15))))
+(let ((e67 (bvsle e22 ((_ zero_extend 2) e12))))
+(let ((e68 (bvsgt e11 ((_ zero_extend 1) e18))))
+(let ((e69 (bvsge ((_ zero_extend 13) e7) e13)))
+(let ((e70 (bvsgt e3 ((_ sign_extend 15) e7))))
+(let ((e71 (distinct ((_ sign_extend 15) e19) e23)))
+(let ((e72 (bvult e23 ((_ zero_extend 2) e11))))
+(let ((e73 (bvslt e11 e15)))
+(let ((e74 (bvuge ((_ sign_extend 13) e24) e28)))
+(let ((e75 (bvule ((_ sign_extend 1) e5) e21)))
+(let ((e76 (xor e42 e74)))
+(let ((e77 (and e65 e49)))
+(let ((e78 (xor e35 e63)))
+(let ((e79 (xor e60 e57)))
+(let ((e80 (and e66 e48)))
+(let ((e81 (or e44 e36)))
+(let ((e82 (= e31 e51)))
+(let ((e83 (xor e52 e71)))
+(let ((e84 (ite e39 e62 e59)))
+(let ((e85 (and e38 e64)))
+(let ((e86 (ite e32 e76 e41)))
+(let ((e87 (xor e73 e43)))
+(let ((e88 (= e75 e79)))
+(let ((e89 (and e83 e80)))
+(let ((e90 (xor e78 e55)))
+(let ((e91 (ite e50 e46 e53)))
+(let ((e92 (and e77 e54)))
+(let ((e93 (or e45 e47)))
+(let ((e94 (not e85)))
+(let ((e95 (= e67 e86)))
+(let ((e96 (= e93 e81)))
+(let ((e97 (or e30 e84)))
+(let ((e98 (not e68)))
+(let ((e99 (= e37 e34)))
+(let ((e100 (or e88 e95)))
+(let ((e101 (not e91)))
+(let ((e102 (= e56 e97)))
+(let ((e103 (and e99 e100)))
+(let ((e104 (not e103)))
+(let ((e105 (ite e58 e72 e69)))
+(let ((e106 (and e105 e104)))
+(let ((e107 (xor e70 e94)))
+(let ((e108 (and e96 e92)))
+(let ((e109 (ite e107 e61 e33)))
+(let ((e110 (and e90 e40)))
+(let ((e111 (= e98 e87)))
+(let ((e112 (xor e106 e108)))
+(let ((e113 (and e112 e112)))
+(let ((e114 (and e110 e102)))
+(let ((e115 (=> e82 e114)))
+(let ((e116 (=> e109 e113)))
+(let ((e117 (=> e116 e116)))
+(let ((e118 (=> e111 e115)))
+(let ((e119 (xor e118 e117)))
+(let ((e120 (not e119)))
+(let ((e121 (ite e89 e120 e120)))
+(let ((e122 (and e121 e101)))
+(let ((e123 (and e122 (not (= e4 (_ bv0 13))))))
+e123
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+(check-sat)

tests/regress/mcsat/0e4fd0ab.smt2.gold

@@ -0,0 +1 @@
+unsat

tests/regress/mcsat/0e4fd0ab.smt2.options

@@ -0,0 +1 @@
+--mcsat

tests/regress/mcsat/80b4dce0.smt2

@@ -0,0 +1,240 @@
+(set-info :source |fuzzsmt|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "random")
+(set-info :status unknown)
+(set-logic QF_AUFBV)
+(declare-fun v0 () (_ BitVec 96))
+(declare-fun v1 () (_ BitVec 115))
+(declare-fun v2 () (_ BitVec 41))
+(declare-fun v3 () (_ BitVec 35))
+(declare-fun a4 () (Array  (_ BitVec 6)  (_ BitVec 95)))
+(declare-fun a5 () (Array  (_ BitVec 12)  (_ BitVec 45)))
+(declare-fun a6 () (Array  (_ BitVec 59)  (_ BitVec 118)))
+(assert (let ((e7(_ bv142 10)))
+(let ((e8(_ bv2530726519770239 52)))
+(let ((e9 (bvsrem ((_ sign_extend 63) e8) v1)))
+(let ((e10 (bvsdiv ((_ sign_extend 61) v3) v0)))
+(let ((e11 (bvxor e9 ((_ zero_extend 80) v3))))
+(let ((e12 ((_ zero_extend 5) e7)))
+(let ((e13 (bvcomp e12 e12)))
+(let ((e14 (ite (bvult e11 ((_ sign_extend 19) v0)) (_ bv1 1) (_ bv0 1))))
+(let ((e15 (bvadd v0 ((_ zero_extend 81) e12))))
+(let ((e16 (bvxor e8 ((_ zero_extend 17) v3))))
+(let ((e17 ((_ rotate_right 33) v2)))
+(let ((e18 (store a6 ((_ zero_extend 18) e17) ((_ sign_extend 22) e10))))
+(let ((e19 (store a5 ((_ extract 50 39) e16) ((_ sign_extend 35) e7))))
+(let ((e20 (select a4 ((_ extract 12 7) v3))))
+(let ((e21 (select a6 ((_ zero_extend 58) e13))))
+(let ((e22 (select e18 ((_ extract 77 19) e10))))
+(let ((e23 (store e19 ((_ extract 72 61) e20) ((_ sign_extend 4) v2))))
+(let ((e24 (select a4 ((_ extract 38 33) e15))))
+(let ((e25 (store a4 ((_ extract 8 3) e12) ((_ sign_extend 80) e12))))
+(let ((e26 (select e25 ((_ extract 54 49) e24))))
+(let ((e27 (bvnand ((_ sign_extend 43) e16) e24)))
+(let ((e28 (ite (bvuge ((_ sign_extend 86) e7) v0) (_ bv1 1) (_ bv0 1))))
+(let ((e29 (bvsrem e15 v0)))
+(let ((e30 (bvxor e20 e27)))
+(let ((e31 ((_ repeat 1) e11)))
+(let ((e32 (bvxor e9 ((_ sign_extend 63) e8))))
+(let ((e33 ((_ rotate_left 17) e22)))
+(let ((e34 (bvxor e16 ((_ sign_extend 11) v2))))
+(let ((e35 (bvmul ((_ zero_extend 77) e17) e22)))
+(let ((e36 (bvneg e21)))
+(let ((e37 (ite (= v1 ((_ zero_extend 20) e27)) (_ bv1 1) (_ bv0 1))))
+(let ((e38 (ite (bvugt e33 ((_ zero_extend 117) e28)) (_ bv1 1) (_ bv0 1))))
+(let ((e39 ((_ extract 0 0) e13)))
+(let ((e40 (bvsdiv ((_ zero_extend 9) e14) e7)))
+(let ((e41 (ite (bvsgt e10 ((_ sign_extend 81) e12)) (_ bv1 1) (_ bv0 1))))
+(let ((e42 (bvashr e39 e13)))
+(let ((e43 (bvand ((_ zero_extend 60) v3) e30)))
+(let ((e44 (bvsdiv e26 e27)))
+(let ((e45 (bvuge ((_ zero_extend 66) e34) e21)))
+(let ((e46 (bvsgt e44 ((_ zero_extend 94) e41))))
+(let ((e47 (bvule ((_ zero_extend 80) e12) e26)))
+(let ((e48 (distinct e33 ((_ sign_extend 3) e32))))
+(let ((e49 (bvslt e44 ((_ sign_extend 94) e39))))
+(let ((e50 (distinct e22 ((_ zero_extend 22) e10))))
+(let ((e51 (bvugt e15 ((_ zero_extend 95) e28))))
+(let ((e52 (distinct ((_ sign_extend 114) e14) e9)))
+(let ((e53 (bvule e37 e37)))
+(let ((e54 (bvule e36 ((_ sign_extend 23) e26))))
+(let ((e55 (bvule ((_ zero_extend 61) v3) e15)))
+(let ((e56 (bvult ((_ zero_extend 114) e13) e32)))
+(let ((e57 (distinct e35 ((_ sign_extend 3) e9))))
+(let ((e58 (bvsle v1 ((_ zero_extend 20) e43))))
+(let ((e59 (bvule ((_ zero_extend 1) e20) e15)))
+(let ((e60 (bvsgt e30 e24)))
+(let ((e61 (bvsgt ((_ sign_extend 20) e26) e11)))
+(let ((e62 (bvult ((_ zero_extend 77) v2) e36)))
+(let ((e63 (distinct e32 ((_ zero_extend 19) e10))))
+(let ((e64 (bvugt e22 ((_ zero_extend 23) e43))))
+(let ((e65 (bvule ((_ zero_extend 40) e37) e17)))
+(let ((e66 (= e39 e37)))
+(let ((e67 (bvuge ((_ zero_extend 23) e26) e35)))
+(let ((e68 (bvsle e9 ((_ zero_extend 63) e8))))
+(let ((e69 (bvsge e34 ((_ zero_extend 51) e28))))
+(let ((e70 (bvule ((_ zero_extend 94) e38) e30)))
+(let ((e71 (bvslt ((_ zero_extend 17) v3) e34)))
+(let ((e72 (bvugt ((_ sign_extend 117) e13) e36)))
+(let ((e73 (bvsle e36 ((_ zero_extend 117) e28))))
+(let ((e74 (bvsge ((_ zero_extend 66) e8) e21)))
+(let ((e75 (bvult e17 ((_ sign_extend 26) e12))))
+(let ((e76 (bvule ((_ sign_extend 3) e9) e22)))
+(let ((e77 (bvult e36 e35)))
+(let ((e78 (bvsgt e43 ((_ sign_extend 94) e42))))
+(let ((e79 (bvuge ((_ zero_extend 95) e41) e15)))
+(let ((e80 (bvule e36 ((_ zero_extend 83) v3))))
+(let ((e81 (bvule ((_ sign_extend 66) e8) e36)))
+(let ((e82 (bvslt ((_ zero_extend 94) e37) e44)))
+(let ((e83 (= ((_ zero_extend 3) e32) e35)))
+(let ((e84 (distinct e22 ((_ sign_extend 3) e11))))
+(let ((e85 (= e35 ((_ zero_extend 66) e16))))
+(let ((e86 (bvuge e9 ((_ zero_extend 19) e15))))
+(let ((e87 (bvsgt ((_ zero_extend 85) e40) e30)))
+(let ((e88 (bvult ((_ zero_extend 117) e38) e36)))
+(let ((e89 (bvule ((_ zero_extend 51) e37) e16)))
+(let ((e90 (bvslt e21 ((_ sign_extend 77) v2))))
+(let ((e91 (bvule ((_ zero_extend 74) e17) e11)))
+(let ((e92 (bvule e36 ((_ sign_extend 22) e10))))
+(let ((e93 (bvslt e8 e8)))
+(let ((e94 (bvugt e13 e39)))
+(let ((e95 (bvult ((_ zero_extend 117) e37) e36)))
+(let ((e96 (bvule ((_ sign_extend 20) e20) e32)))
+(let ((e97 (bvslt ((_ sign_extend 83) v3) e33)))
+(let ((e98 (= e40 ((_ sign_extend 9) e37))))
+(let ((e99 (= e29 ((_ sign_extend 1) e20))))
+(let ((e100 (distinct ((_ sign_extend 114) e28) e9)))
+(let ((e101 (bvsle e15 v0)))
+(let ((e102 (bvsgt ((_ zero_extend 86) e7) e29)))
+(let ((e103 (bvule e20 ((_ zero_extend 54) v2))))
+(let ((e104 (bvuge e11 ((_ zero_extend 114) e13))))
+(let ((e105 (bvugt e44 ((_ sign_extend 54) v2))))
+(let ((e106 (bvslt ((_ sign_extend 77) e17) e35)))
+(let ((e107 (= e32 ((_ zero_extend 20) e30))))
+(let ((e108 (bvule ((_ sign_extend 11) e17) e34)))
+(let ((e109 (= ((_ sign_extend 23) e20) e21)))
+(let ((e110 (bvsle e20 ((_ zero_extend 94) e39))))
+(let ((e111 (bvslt e36 ((_ zero_extend 117) e42))))
+(let ((e112 (bvslt ((_ zero_extend 40) e14) e17)))
+(let ((e113 (distinct ((_ zero_extend 1) e24) e15)))
+(let ((e114 (= e32 ((_ sign_extend 19) e15))))
+(let ((e115 (bvule e15 ((_ zero_extend 95) e38))))
+(let ((e116 (bvslt e17 v2)))
+(let ((e117 (bvule ((_ zero_extend 117) e39) e35)))
+(let ((e118 (bvule e9 e9)))
+(let ((e119 (bvult e35 e33)))
+(let ((e120 (bvugt ((_ sign_extend 22) e10) e35)))
+(let ((e121 (bvsge ((_ zero_extend 114) e38) v1)))
+(let ((e122 (bvsge ((_ sign_extend 94) e13) e26)))
+(let ((e123 (bvuge ((_ sign_extend 60) v3) e24)))
+(let ((e124 (bvsge e15 ((_ sign_extend 44) e34))))
+(let ((e125 (bvuge e11 ((_ sign_extend 63) e16))))
+(let ((e126 (bvsgt ((_ zero_extend 40) e28) e17)))
+(let ((e127 (bvsgt ((_ zero_extend 23) e27) e36)))
+(let ((e128 (bvsle ((_ sign_extend 108) e40) e35)))
+(let ((e129 (bvsle e39 e41)))
+(let ((e130 (bvsle ((_ zero_extend 77) v2) e33)))
+(let ((e131 (bvugt e21 ((_ zero_extend 77) v2))))
+(let ((e132 (bvult ((_ sign_extend 80) v3) v1)))
+(let ((e133 (bvsge v0 ((_ sign_extend 1) e24))))
+(let ((e134 (bvuge v1 e9)))
+(let ((e135 (bvule v1 e31)))
+(let ((e136 (=> e98 e97)))
+(let ((e137 (=> e79 e55)))
+(let ((e138 (xor e128 e133)))
+(let ((e139 (= e66 e116)))
+(let ((e140 (and e80 e124)))
+(let ((e141 (= e96 e111)))
+(let ((e142 (not e82)))
+(let ((e143 (ite e113 e136 e90)))
+(let ((e144 (not e125)))
+(let ((e145 (=> e143 e119)))
+(let ((e146 (or e64 e78)))
+(let ((e147 (xor e101 e122)))
+(let ((e148 (xor e114 e70)))
+(let ((e149 (and e61 e121)))
+(let ((e150 (and e69 e105)))
+(let ((e151 (or e45 e117)))
+(let ((e152 (ite e139 e110 e88)))
+(let ((e153 (=> e89 e68)))
+(let ((e154 (ite e50 e84 e102)))
+(let ((e155 (or e77 e137)))
+(let ((e156 (ite e108 e154 e142)))
+(let ((e157 (not e129)))
+(let ((e158 (or e87 e87)))
+(let ((e159 (or e92 e118)))
+(let ((e160 (ite e156 e76 e138)))
+(let ((e161 (= e67 e131)))
+(let ((e162 (or e127 e157)))
+(let ((e163 (= e141 e140)))
+(let ((e164 (xor e94 e99)))
+(let ((e165 (xor e85 e126)))
+(let ((e166 (ite e75 e49 e73)))
+(let ((e167 (and e54 e115)))
+(let ((e168 (or e148 e153)))
+(let ((e169 (ite e109 e72 e164)))
+(let ((e170 (xor e60 e135)))
+(let ((e171 (and e86 e165)))
+(let ((e172 (ite e71 e51 e120)))
+(let ((e173 (not e48)))
+(let ((e174 (not e95)))
+(let ((e175 (and e52 e168)))
+(let ((e176 (= e106 e151)))
+(let ((e177 (not e146)))
+(let ((e178 (or e59 e155)))
+(let ((e179 (= e145 e149)))
+(let ((e180 (not e159)))
+(let ((e181 (= e53 e169)))
+(let ((e182 (= e134 e65)))
+(let ((e183 (ite e175 e162 e103)))
+(let ((e184 (and e158 e170)))
+(let ((e185 (and e47 e179)))
+(let ((e186 (ite e74 e123 e178)))
+(let ((e187 (and e186 e56)))
+(let ((e188 (not e57)))
+(let ((e189 (xor e100 e163)))
+(let ((e190 (= e132 e181)))
+(let ((e191 (=> e91 e177)))
+(let ((e192 (and e185 e93)))
+(let ((e193 (= e112 e176)))
+(let ((e194 (=> e83 e58)))
+(let ((e195 (=> e191 e192)))
+(let ((e196 (xor e195 e187)))
+(let ((e197 (xor e167 e193)))
+(let ((e198 (xor e150 e173)))
+(let ((e199 (and e161 e46)))
+(let ((e200 (ite e171 e152 e144)))
+(let ((e201 (and e197 e166)))
+(let ((e202 (not e198)))
+(let ((e203 (ite e201 e63 e62)))
+(let ((e204 (ite e81 e184 e200)))
+(let ((e205 (=> e180 e199)))
+(let ((e206 (=> e203 e204)))
+(let ((e207 (or e190 e189)))
+(let ((e208 (and e172 e205)))
+(let ((e209 (=> e202 e208)))
+(let ((e210 (and e104 e194)))
+(let ((e211 (and e183 e130)))
+(let ((e212 (ite e206 e147 e207)))
+(let ((e213 (= e188 e210)))
+(let ((e214 (=> e174 e213)))
+(let ((e215 (= e182 e196)))
+(let ((e216 (and e107 e209)))
+(let ((e217 (xor e212 e215)))
+(let ((e218 (and e216 e160)))
+(let ((e219 (=> e214 e217)))
+(let ((e220 (= e218 e211)))
+(let ((e221 (not e219)))
+(let ((e222 (=> e221 e220)))
+(let ((e223 (and e222 (not (= e7 (_ bv0 10))))))
+(let ((e224 (and e223 (not (= e7 (bvnot (_ bv0 10)))))))
+(let ((e225 (and e224 (not (= v0 (_ bv0 96))))))
+(let ((e226 (and e225 (not (= v0 (bvnot (_ bv0 96)))))))
+(let ((e227 (and e226 (not (= v1 (_ bv0 115))))))
+(let ((e228 (and e227 (not (= v1 (bvnot (_ bv0 115)))))))
+(let ((e229 (and e228 (not (= e27 (_ bv0 95))))))
+(let ((e230 (and e229 (not (= e27 (bvnot (_ bv0 95)))))))
+e230
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+(check-sat)

tests/regress/mcsat/80b4dce0.smt2.gold

@@ -0,0 +1 @@
+sat

tests/regress/mcsat/80b4dce0.smt2.options

@@ -0,0 +1 @@
+--mcsat