search

uuverifiers / eldarica

The Eldarica model checker
Other
81 stars 23 forks source link

Internal Exception on CHC(BV) formula #27

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following instance,

(set-logic HORN)
(assert (forall ((q0 (_ BitVec 12)) (q1 (_ BitVec 12)) (q2 (_ BitVec 32))) (=> (= q1 q0) (bvslt (bvurem (bvsrem (bvsrem q2 q2) q2) q2) q2))))
(assert (forall ((q3 (_ BitVec 12)) (q4 (_ BitVec 12)) (q5 (_ BitVec 12)) (q6 (_ BitVec 12)) (q7 (_ BitVec 12)) (q8 (_ BitVec 12)) (q9 (_ BitVec 12)) (q10 (_ BitVec 12)) (q11 (_ BitVec 12)) (q12 (_ BitVec 12)) (q13 (_ BitVec 12)) (q14 (_ BitVec 12)) (q15 (_ BitVec 12)) (q16 (_ BitVec 10))) (=> (= q14 q8) (distinct q16 (bvnot q16)))))
(assert (forall ((q17 (_ BitVec 12)) (q18 (_ BitVec 12)) (q19 (_ BitVec 12)) (q20 (_ BitVec 12)) (q21 (_ BitVec 12)) (q22 (_ BitVec 12)) (q23 (_ BitVec 12)) (q24 (_ BitVec 32))) (=> (distinct q24 (bvsdiv q24 q24)) (= (bvsmod q19 q17) q17))))
(assert (forall ((q25 (_ BitVec 12)) (q26 (_ BitVec 12)) (q27 (_ BitVec 12)) (q28 (_ BitVec 12)) (q29 (_ BitVec 12)) (q30 (_ BitVec 12)) (q31 (_ BitVec 12)) (q32 (_ BitVec 20))) (=> (= q32 (bvnand q32 q32)) (= q25 q26))))
(assert (forall ((q33 (_ BitVec 12)) (q34 (_ BitVec 12)) (q35 (_ BitVec 12)) (q36 (_ BitVec 12)) (q37 (_ BitVec 12)) (q38 (_ BitVec 12)) (q39 (_ BitVec 12)) (q40 (_ BitVec 12)) (q41 (_ BitVec 7))) (=> (bvuge (bvsdiv q41 q41) (bvsdiv q41 q41)) (distinct q33 q38))))
(assert (forall ((q42 (_ BitVec 12)) (q43 (_ BitVec 12)) (q44 (_ BitVec 12)) (q45 (_ BitVec 12)) (q46 (_ BitVec 12)) (q47 (_ BitVec 12)) (q48 (_ BitVec 12)) (q49 (_ BitVec 12)) (q50 (_ BitVec 12)) (q51 (_ BitVec 12)) (q52 (_ BitVec 12)) (q53 (_ BitVec 12)) (q54 (_ BitVec 12)) (q55 (_ BitVec 7))) (=> (distinct q54 q53) (= (bvsmod (bvneg q55) (bvneg q55)) (bvneg q55)))))
(assert (forall ((q56 (_ BitVec 12)) (q57 (_ BitVec 12)) (q58 (_ BitVec 39))) (=> (= q58 ((_ sign_extend 0) q58)) (bvult (bvudiv q56 q57) (bvlshr (bvudiv q56 q57) q56)))))
(assert (forall ((q59 (_ BitVec 12)) (q60 (_ BitVec 12)) (q61 (_ BitVec 39))) (=> (distinct q61 q61) (bvsge (bvudiv q60 q60) (bvsub q60 q59)))))
(assert (forall ((q62 (_ BitVec 12)) (q63 (_ BitVec 12)) (q64 (_ BitVec 12)) (q65 (_ BitVec 12)) (q66 (_ BitVec 12)) (q67 (_ BitVec 12)) (q68 Bool)) (=> (= q63 q62) (=> q68 q68))))
(assert (forall ((q69 (_ BitVec 12)) (q70 (_ BitVec 12)) (q71 (_ BitVec 12)) (q72 (_ BitVec 12)) (q73 (_ BitVec 12)) (q74 (_ BitVec 12)) (q75 (_ BitVec 12)) (q76 (_ BitVec 12)) (q77 (_ BitVec 12)) (q78 (_ BitVec 12)) (q79 (_ BitVec 12)) (q80 (_ BitVec 12)) (q81 (_ BitVec 12)) (q82 Bool)) (=> (distinct q80 q74) (xor q82 q82 q82 q82 q82 q82))))
(assert (forall ((q83 (_ BitVec 12)) (q84 (_ BitVec 12)) (q85 (_ BitVec 12)) (q86 (_ BitVec 12)) (q87 (_ BitVec 12)) (q88 (_ BitVec 12)) (q89 (_ BitVec 12)) (q90 (_ BitVec 12)) (q91 (_ BitVec 7))) (=> (= q85 q88) (= q91 (bvnand q91 q91)))))
(assert (forall ((q92 (_ BitVec 12)) (q93 (_ BitVec 12)) (q94 (_ BitVec 12)) (q95 (_ BitVec 12)) (q96 (_ BitVec 12)) (q97 (_ BitVec 12)) (q98 (_ BitVec 12)) (q99 (_ BitVec 39))) (=> (bvsge (bvand q99 q99) q99) (bvsgt q92 q92))))
(assert (forall ((q100 (_ BitVec 12)) (q101 (_ BitVec 12)) (q102 (_ BitVec 12)) (q103 (_ BitVec 12)) (q104 (_ BitVec 12)) (q105 (_ BitVec 12)) (q106 (_ BitVec 12)) (q107 (_ BitVec 8))) (=> (= q107 (bvnand q107 q107)) (distinct q100 q102))))
(assert (forall ((q108 (_ BitVec 12)) (q109 (_ BitVec 12)) (q110 (_ BitVec 12)) (q111 (_ BitVec 12)) (q112 (_ BitVec 12)) (q113 (_ BitVec 12)) (q114 (_ BitVec 12)) (q115 (_ BitVec 12)) (q116 (_ BitVec 12)) (q117 (_ BitVec 12)) (q118 (_ BitVec 12)) (q119 (_ BitVec 12)) (q120 (_ BitVec 12)) (q121 (_ BitVec 8))) (=> (= q111 (bvsub q110 q119)) (distinct q121 (bvashr q121 q121)))))
(assert (forall ((q122 (_ BitVec 12)) (q123 (_ BitVec 12)) (q124 (_ BitVec 12)) (q125 (_ BitVec 12)) (q126 (_ BitVec 12)) (q127 (_ BitVec 12)) (q128 (_ BitVec 12)) (q129 (_ BitVec 12)) (q130 (_ BitVec 12)) (q131 (_ BitVec 12)) (q132 (_ BitVec 8))) (=> (distinct q125 q126) (distinct (bvurem q132 q132) (bvnor q132 q132)))))
(assert (forall ((q133 (_ BitVec 12)) (q134 (_ BitVec 12)) (q135 (_ BitVec 12)) (q136 (_ BitVec 12)) (q137 (_ BitVec 12)) (q138 (_ BitVec 12)) (q139 (_ BitVec 12)) (q140 (_ BitVec 12)) (q141 (_ BitVec 12)) (q142 (_ BitVec 12)) (q143 (_ BitVec 12)) (q144 Bool)) (=> (bvsgt q136 q141) (or q144 q144 q144 q144))))
(assert (forall ((q159 (_ BitVec 12)) (q160 (_ BitVec 12)) (q161 (_ BitVec 12)) (q162 (_ BitVec 12)) (q163 (_ BitVec 12)) (q164 (_ BitVec 12)) (q165 (_ BitVec 8))) (=> (= (bvsub q162 q159) (bvsub q162 q159)) (distinct (bvsub q165 q165) (bvsub q165 q165)))))
(assert (forall ((q166 (_ BitVec 12)) (q167 (_ BitVec 12)) (q168 (_ BitVec 12)) (q169 (_ BitVec 12)) (q170 (_ BitVec 12)) (q171 (_ BitVec 12)) (q172 (_ BitVec 32))) (=> (bvsle q172 (bvadd q172 q172)) (bvsge q171 q168))))
(assert (forall ((q173 (_ BitVec 12)) (q174 (_ BitVec 12)) (q175 (_ BitVec 12)) (q176 (_ BitVec 12)) (q177 (_ BitVec 12)) (q178 (_ BitVec 12)) (q179 (_ BitVec 12)) (q180 (_ BitVec 12)) (q181 (_ BitVec 12)) (q182 (_ BitVec 7))) (=> (= q178 q180) (distinct q182 q182))))
(assert (forall ((q183 (_ BitVec 12)) (q184 (_ BitVec 12)) (q185 (_ BitVec 10))) (=> (bvslt q185 q185) (= q184 q183))))
(assert (forall ((q186 (_ BitVec 12)) (q187 (_ BitVec 12)) (q188 (_ BitVec 12)) (q189 (_ BitVec 12)) (q190 (_ BitVec 12)) (q191 (_ BitVec 12)) (q192 (_ BitVec 12)) (q193 (_ BitVec 12)) (q194 (_ BitVec 12)) (q195 (_ BitVec 12)) (q196 (_ BitVec 12)) (q197 (_ BitVec 12)) (q198 (_ BitVec 12)) (q199 (_ BitVec 12)) (q200 (_ BitVec 31))) (=> (bvslt q196 q195) (= q200 (bvnot q200)))))
(assert (forall ((q201 (_ BitVec 12)) (q202 (_ BitVec 12)) (q203 (_ BitVec 12)) (q204 (_ BitVec 12)) (q205 (_ BitVec 12)) (q206 (_ BitVec 12)) (q207 (_ BitVec 12)) (q208 (_ BitVec 12)) (q209 (_ BitVec 39))) (=> (bvsgt q209 q209) (= (bvnor q202 (bvadd q207 q206)) (bvshl q201 q208)))))
(assert (forall ((q210 (_ BitVec 12)) (q211 (_ BitVec 12)) (q212 (_ BitVec 12)) (q213 (_ BitVec 12)) (q214 (_ BitVec 12)) (q215 (_ BitVec 12)) (q216 (_ BitVec 12)) (q217 (_ BitVec 12)) (q218 (_ BitVec 12)) (q219 (_ BitVec 12)) (q220 (_ BitVec 31))) (=> (bvult q211 q219) (distinct (bvsrem q220 q220) (bvurem (bvsrem q220 q220) q220)))))
(assert (forall ((q221 (_ BitVec 12)) (q222 (_ BitVec 12)) (q223 (_ BitVec 12)) (q224 (_ BitVec 12)) (q225 (_ BitVec 12)) (q226 (_ BitVec 12)) (q227 (_ BitVec 12)) (q228 (_ BitVec 12)) (q229 (_ BitVec 12)) (q230 (_ BitVec 12)) (q231 (_ BitVec 12)) (q232 (_ BitVec 12)) (q233 (_ BitVec 10))) (=> (distinct q231 q223) (distinct (bvnand (bvmul q233 q233) q233) (bvor (bvmul q233 q233) (bvnand (bvmul q233 q233) q233))))))
(assert (forall ((q253 (_ BitVec 12)) (q254 (_ BitVec 12)) (q255 (_ BitVec 12)) (q256 (_ BitVec 12)) (q257 (_ BitVec 7))) (=> (= (bvsdiv q253 q255) q253) (= (bvudiv q257 q257) (bvudiv q257 q257)))))
(assert (forall ((q258 (_ BitVec 12)) (q259 (_ BitVec 12)) (q260 (_ BitVec 12)) (q261 (_ BitVec 12)) (q262 (_ BitVec 12)) (q263 (_ BitVec 12)) (q264 (_ BitVec 12)) (q265 (_ BitVec 12)) (q266 (_ BitVec 12)) (q267 (_ BitVec 12)) (q268 (_ BitVec 12)) (q269 (_ BitVec 12)) (q270 (_ BitVec 12)) (q271 (_ BitVec 7))) (=> (= q270 q261) (bvslt q271 (bvashr q271 q271)))))
(assert (forall ((q272 (_ BitVec 12)) (q273 (_ BitVec 12)) (q274 (_ BitVec 12)) (q275 (_ BitVec 12)) (q276 (_ BitVec 12)) (q277 (_ BitVec 12)) (q278 (_ BitVec 12)) (q279 (_ BitVec 12)) (q280 (_ BitVec 12)) (q281 Bool)) (=> (and q281 q281 q281 q281 q281 q281 q281 q281 q281) (= q279 q275))))
(assert (forall ((q282 (_ BitVec 12)) (q283 (_ BitVec 12)) (q284 (_ BitVec 12)) (q285 (_ BitVec 12)) (q286 (_ BitVec 12)) (q287 (_ BitVec 12)) (q288 (_ BitVec 12)) (q289 (_ BitVec 12)) (q290 (_ BitVec 12)) (q291 (_ BitVec 20))) (=> (= (bvsdiv q291 q291) q291) (= q286 (bvor q290 q289)))))
(assert (forall ((q293 (_ BitVec 12)) (q294 (_ BitVec 12)) (q295 (_ BitVec 12)) (q296 (_ BitVec 12)) (q297 (_ BitVec 12)) (q298 Bool)) (=> (not q298) (= q294 q293))))
(assert (forall ((q299 (_ BitVec 12)) (q300 (_ BitVec 12)) (q301 (_ BitVec 12)) (q302 (_ BitVec 8))) (=> (bvult q302 q302) (bvsge q301 q301))))
(assert (forall ((q303 (_ BitVec 12)) (q304 (_ BitVec 12)) (q305 (_ BitVec 12)) (q306 (_ BitVec 12)) (q307 (_ BitVec 12)) (q308 (_ BitVec 12)) (q309 (_ BitVec 7))) (=> (distinct q305 q303) (bvslt q309 q309))))
(assert (forall ((q310 (_ BitVec 12)) (q311 (_ BitVec 12)) (q312 (_ BitVec 12)) (q313 (_ BitVec 12)) (q314 (_ BitVec 12)) (q315 (_ BitVec 31))) (=> (= (bvshl q314 q314) (bvshl q314 q314)) (distinct q315 q315))))
(assert (forall ((q316 (_ BitVec 12)) (q317 (_ BitVec 12)) (q318 (_ BitVec 12)) (q319 (_ BitVec 12)) (q320 (_ BitVec 12)) (q321 (_ BitVec 12)) (q322 (_ BitVec 12)) (q323 (_ BitVec 12)) (q324 (_ BitVec 12)) (q325 (_ BitVec 12)) (q326 (_ BitVec 12)) (q327 (_ BitVec 12)) (q328 (_ BitVec 20))) (=> (= q323 (bvnor q325 q326)) (distinct (bvashr (bvsub q328 q328) q328) q328))))
(assert (forall ((q330 (_ BitVec 12)) (q331 (_ BitVec 12)) (q332 (_ BitVec 9))) (=> (bvsgt q330 (bvshl q330 q331)) (distinct q332 q332))))
(assert (forall ((q333 (_ BitVec 12)) (q334 (_ BitVec 12)) (q335 (_ BitVec 12)) (q336 (_ BitVec 12)) (q337 (_ BitVec 12)) (q338 (_ BitVec 12)) (q339 (_ BitVec 12)) (q340 (_ BitVec 12)) (q341 (_ BitVec 12)) (q342 (_ BitVec 15))) (=> (distinct q338 q336) (= (bvlshr q342 q342) (bvlshr q342 q342)))))
(assert (forall ((q343 (_ BitVec 12)) (q344 (_ BitVec 12)) (q345 (_ BitVec 12)) (q346 (_ BitVec 12)) (q347 (_ BitVec 12)) (q348 (_ BitVec 31))) (=> (= q348 (bvand q348 (bvsmod q348 q348))) (distinct q347 q344))))
(assert (forall ((q349 (_ BitVec 12)) (q350 (_ BitVec 12)) (q351 (_ BitVec 12)) (q352 (_ BitVec 12)) (q353 (_ BitVec 12)) (q354 (_ BitVec 12)) (q355 (_ BitVec 12)) (q356 (_ BitVec 12)) (q357 (_ BitVec 12)) (q358 (_ BitVec 12)) (q359 (_ BitVec 12)) (q360 (_ BitVec 12)) (q361 (_ BitVec 8))) (=> (bvslt (bvor q361 q361) (bvor q361 q361)) (bvsle q360 q353))))
(assert (forall ((q362 (_ BitVec 12)) (q363 (_ BitVec 12)) (q364 (_ BitVec 12)) (q365 (_ BitVec 12)) (q366 (_ BitVec 12)) (q367 (_ BitVec 12)) (q368 (_ BitVec 12)) (q369 (_ BitVec 12)) (q370 (_ BitVec 39))) (=> (= (bvsrem q370 q370) (bvsrem q370 q370)) (distinct q368 q367))))
(assert (forall ((q371 (_ BitVec 12)) (q372 (_ BitVec 12)) (q373 (_ BitVec 12)) (q374 (_ BitVec 12)) (q375 (_ BitVec 12)) (q376 (_ BitVec 12)) (q377 (_ BitVec 12)) (q378 (_ BitVec 12)) (q379 (_ BitVec 12)) (q380 (_ BitVec 12)) (q381 (_ BitVec 12)) (q382 (_ BitVec 12)) (q383 (_ BitVec 10))) (=> (= q383 (bvashr q383 q383)) (distinct q371 (bvnot (bvsdiv q375 q375))))))
(assert (forall ((q384 (_ BitVec 12)) (q385 (_ BitVec 12)) (q386 (_ BitVec 12)) (q387 (_ BitVec 12)) (q388 (_ BitVec 9))) (=> (distinct q385 q385) (= (bvshl q388 q388) (bvadd q388 q388)))))
(assert (forall ((q389 (_ BitVec 12)) (q390 (_ BitVec 12)) (q391 (_ BitVec 12)) (q392 Bool)) (=> (distinct q392 q392 q392 q392 q392 q392 q392 q392 q392) (= q390 (bvlshr q391 (bvshl q390 q390))))))
(assert (forall ((q393 (_ BitVec 12)) (q394 (_ BitVec 12)) (q395 (_ BitVec 12)) (q396 (_ BitVec 12)) (q397 (_ BitVec 12)) (q398 (_ BitVec 12)) (q399 (_ BitVec 12)) (q400 (_ BitVec 12)) (q401 (_ BitVec 12)) (q402 (_ BitVec 12)) (q403 (_ BitVec 12)) (q404 (_ BitVec 12)) (q405 (_ BitVec 12)) (q406 (_ BitVec 12)) (q407 (_ BitVec 1))) (=> (distinct q407 q407) (bvsgt q402 q395))))
(assert (forall ((q409 (_ BitVec 12)) (q410 (_ BitVec 12)) (q411 (_ BitVec 12)) (q412 (_ BitVec 12)) (q413 (_ BitVec 12)) (q414 (_ BitVec 12)) (q415 (_ BitVec 12)) (q416 (_ BitVec 12)) (q417 (_ BitVec 12)) (q418 (_ BitVec 12)) (q419 (_ BitVec 12)) (q420 (_ BitVec 12)) (q421 (_ BitVec 12)) (q422 Bool)) (=> (distinct q409 q411) (and q422 q422 q422 q422 q422))))
(assert (forall ((q423 (_ BitVec 12)) (q424 (_ BitVec 12)) (q425 (_ BitVec 12)) (q426 (_ BitVec 12)) (q427 (_ BitVec 12)) (q428 (_ BitVec 12)) (q429 (_ BitVec 12)) (q430 (_ BitVec 12)) (q431 (_ BitVec 12)) (q432 (_ BitVec 12)) (q433 (_ BitVec 12)) (q434 (_ BitVec 12)) (q435 (_ BitVec 12)) (q436 (_ BitVec 20))) (=> (= q426 q426) (distinct q436 q436))))
(assert (forall ((q438 (_ BitVec 12)) (q439 (_ BitVec 12)) (q440 (_ BitVec 12)) (q441 (_ BitVec 12)) (q442 (_ BitVec 12)) (q443 (_ BitVec 12)) (q444 (_ BitVec 8))) (=> (bvugt q443 q439) (bvslt (bvsdiv q444 q444) (bvsdiv q444 q444)))))
(assert (forall ((q445 (_ BitVec 12)) (q446 (_ BitVec 12)) (q447 (_ BitVec 12)) (q448 (_ BitVec 12)) (q449 (_ BitVec 12)) (q450 (_ BitVec 12)) (q451 (_ BitVec 12)) (q452 (_ BitVec 12)) (q453 (_ BitVec 12)) (q454 (_ BitVec 12)) (q455 (_ BitVec 12)) (q456 (_ BitVec 12)) (q457 (_ BitVec 12)) (q458 (_ BitVec 9))) (=> (= q458 (bvsub (bvand q458 q458) q458)) (bvuge q447 q445))))
(assert (forall ((q459 (_ BitVec 12)) (q460 (_ BitVec 12)) (q461 (_ BitVec 12)) (q462 (_ BitVec 12)) (q463 (_ BitVec 12)) (q464 (_ BitVec 12)) (q465 (_ BitVec 12)) (q466 (_ BitVec 12)) (q467 (_ BitVec 20))) (=> (distinct q461 q466) (bvule (bvsmod q467 (bvsub q467 q467)) (bvsub q467 q467)))))
(check-sat)

eldarica 31d9075

Theories: GroebnerMultiplication, ModuloArithmetic
 (error "Internal exception: java.lang.AssertionError: assertion failed")
pruemmer commented 4 years ago

I cannot reproduce this problem any more in version f817bc3, so hopefully this was fixed as well.

rainoftime commented 4 years ago

A new test

(set-logic HORN)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const bv_28-0 (_ BitVec 28))
(declare-const bv_7-0 (_ BitVec 7))
(declare-const bv_2-0 (_ BitVec 2))
(assert (forall ((q0 (_ BitVec 28)) (q1 (_ BitVec 28)) (q2 Bool)) (=> (and q2 q2) (bvsge (bvor (bvadd q1 q0) q0) (bvudiv q0 (bvadd q1 q0))))))
(assert (forall ((q3 (_ BitVec 28)) (q4 (_ BitVec 28)) (q5 (_ BitVec 12))) (=> (= q4 q4) (bvult (bvmul q5 q5) q5))))
(assert (forall ((q6 (_ BitVec 28)) (q7 (_ BitVec 28)) (q8 (_ BitVec 28)) (q9 (_ BitVec 28)) (q10 (_ BitVec 9))) (=> (distinct (bvsub (bvudiv q10 q10) (bvudiv q10 q10)) (bvsub (bvudiv q10 q10) (bvudiv q10 q10))) (distinct q6 q8))))
(assert (forall ((q11 (_ BitVec 28)) (q12 (_ BitVec 28)) (q13 (_ BitVec 28)) (q14 (_ BitVec 28)) (q15 (_ BitVec 28)) (q16 (_ BitVec 28)) (q17 (_ BitVec 28)) (q18 (_ BitVec 28)) (q19 (_ BitVec 11))) (=> (= q17 q18) (= q19 (bvnor q19 q19)))))
(declare-const bv_13-0 (_ BitVec 13))
(assert (forall ((q38 (_ BitVec 28)) (q39 (_ BitVec 28)) (q40 (_ BitVec 9))) (=> (= q40 (bvnor q40 q40)) (bvsgt (bvshl q38 q38) (bvneg q38)))))
(assert (forall ((q41 (_ BitVec 28)) (q42 (_ BitVec 28)) (q43 (_ BitVec 28)) (q44 (_ BitVec 28)) (q45 Bool)) (=> (not q45) (bvslt q42 q43))))
(check-sat)
~