search

uuverifiers / eldarica

The Eldarica model checker
Other
80 stars 22 forks source link

AssertionError at Predef.scala:156 (Debug.scala:111) #23

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi , for the following instance,

(set-logic HORN)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const bv_17-0 (_ BitVec 17))
(declare-const bv_29-0 (_ BitVec 29))
(assert (forall ((q0 (_ BitVec 10)) (q1 (_ BitVec 10)) (q2 (_ BitVec 10)) (q3 (_ BitVec 10)) (q4 (_ BitVec 10)) (q5 (_ BitVec 10)) (q6 (_ BitVec 10)) (q7 (_ BitVec 4))) (=> (bvsgt (bvsub q0 q5) q6) (bvuge q7 (bvsmod q7 (bvshl q7 q7))))))
(assert (forall ((q8 (_ BitVec 10)) (q9 (_ BitVec 10)) (q10 (_ BitVec 10)) (q11 (_ BitVec 10)) (q12 Bool)) (=> (distinct q12 q12 q12 q12 q12) (distinct (bvnor q10 q8) q10))))
(assert (forall ((q31 (_ BitVec 10)) (q32 (_ BitVec 10)) (q33 (_ BitVec 10)) (q34 (_ BitVec 10)) (q35 (_ BitVec 10)) (q36 (_ BitVec 10)) (q37 (_ BitVec 10)) (q38 (_ BitVec 10)) (q39 (_ BitVec 10)) (q40 (_ BitVec 10)) (q41 (_ BitVec 10)) (q42 (_ BitVec 10)) (q43 Bool)) (=> (xor q43 q43) (distinct (bvand q36 q37) (bvlshr q31 q37)))))
(assert (forall ((q44 (_ BitVec 10)) (q45 (_ BitVec 10)) (q46 (_ BitVec 10)) (q47 (_ BitVec 10)) (q48 (_ BitVec 10)) (q49 (_ BitVec 10)) (q50 (_ BitVec 10)) (q51 (_ BitVec 10)) (q52 (_ BitVec 10)) (q53 (_ BitVec 10)) (q54 (_ BitVec 10)) (q55 (_ BitVec 10)) (q56 (_ BitVec 10)) (q57 (_ BitVec 10)) (q58 (_ BitVec 10)) (q59 (_ BitVec 3))) (=> (bvsge q55 q53) (distinct q59 q59))))
(assert (forall ((q60 (_ BitVec 10)) (q61 (_ BitVec 10)) (q62 (_ BitVec 10)) (q63 (_ BitVec 10)) (q64 (_ BitVec 10)) (q65 (_ BitVec 10)) (q66 (_ BitVec 10)) (q67 (_ BitVec 10)) (q68 (_ BitVec 10)) (q69 (_ BitVec 10)) (q70 (_ BitVec 10)) (q71 (_ BitVec 10)) (q72 (_ BitVec 10)) (q73 (_ BitVec 10)) (q74 (_ BitVec 10)) (q75 (_ BitVec 4))) (=> (distinct (bvsrem q75 q75) q75) (distinct q63 (bvmul q68 q61)))))
(assert (forall ((q77 (_ BitVec 10)) (q78 (_ BitVec 10)) (q79 (_ BitVec 10)) (q80 (_ BitVec 10)) (q81 (_ BitVec 10)) (q82 (_ BitVec 10)) (q83 (_ BitVec 10)) (q84 (_ BitVec 10)) (q85 (_ BitVec 10)) (q86 (_ BitVec 10)) (q87 (_ BitVec 10)) (q88 (_ BitVec 10)) (q89 (_ BitVec 10)) (q90 (_ BitVec 10)) (q91 (_ BitVec 10)) (q92 (_ BitVec 10)) (q93 (_ BitVec 10)) (q94 (_ BitVec 10)) (q95 (_ BitVec 9))) (=> (= q87 q89) (distinct (bvnand q95 q95) (bvnand q95 q95)))))
(assert (forall ((q96 (_ BitVec 10)) (q97 (_ BitVec 10)) (q98 (_ BitVec 10)) (q99 (_ BitVec 10)) (q100 (_ BitVec 10)) (q101 (_ BitVec 10)) (q102 (_ BitVec 10)) (q103 (_ BitVec 10)) (q104 (_ BitVec 10)) (q105 (_ BitVec 10)) (q106 (_ BitVec 10)) (q107 (_ BitVec 10)) (q108 (_ BitVec 8))) (=> (= q104 q106) (= (bvor q108 q108) (bvor q108 q108)))))
(assert (forall ((q109 (_ BitVec 10)) (q110 (_ BitVec 10)) (q111 (_ BitVec 10)) (q112 (_ BitVec 10)) (q113 (_ BitVec 10)) (q114 (_ BitVec 10)) (q115 (_ BitVec 10)) (q116 (_ BitVec 10)) (q117 (_ BitVec 10)) (q118 (_ BitVec 10)) (q119 (_ BitVec 10)) (q120 (_ BitVec 10)) (q121 (_ BitVec 10)) (q122 (_ BitVec 10)) (q123 (_ BitVec 10)) (q124 (_ BitVec 10)) (q125 (_ BitVec 8))) (=> (bvult (bvnot q125) (bvnot q125)) (distinct q121 q114))))
(assert (forall ((q126 (_ BitVec 10)) (q127 (_ BitVec 10)) (q128 (_ BitVec 10)) (q129 (_ BitVec 10)) (q130 (_ BitVec 10)) (q131 (_ BitVec 10)) (q132 (_ BitVec 10)) (q133 (_ BitVec 10)) (q134 (_ BitVec 10)) (q135 (_ BitVec 10)) (q136 (_ BitVec 10)) (q137 (_ BitVec 10)) (q138 (_ BitVec 10)) (q139 (_ BitVec 4))) (=> (distinct q139 q139) (= q137 q131))))
(declare-const bv_4-1 (_ BitVec 4))
(assert (forall ((q140 (_ BitVec 10)) (q141 (_ BitVec 10)) (q142 (_ BitVec 10)) (q143 (_ BitVec 10)) (q144 (_ BitVec 10)) (q145 (_ BitVec 10)) (q146 (_ BitVec 10)) (q147 (_ BitVec 10)) (q148 (_ BitVec 10)) (q149 (_ BitVec 10)) (q150 (_ BitVec 10)) (q151 (_ BitVec 10)) (q152 (_ BitVec 10)) (q153 (_ BitVec 10)) (q154 (_ BitVec 10)) (q155 (_ BitVec 9))) (=> (distinct q155 q155) (= q151 (bvadd q140 q148)))))
(assert (forall ((q156 (_ BitVec 10)) (q157 (_ BitVec 10)) (q158 (_ BitVec 12))) (=> (= q158 ((_ sign_extend 0) q158)) (distinct q157 q157))))
(assert (forall ((q159 (_ BitVec 10)) (q160 (_ BitVec 10)) (q161 (_ BitVec 10)) (q162 (_ BitVec 10)) (q163 (_ BitVec 10)) (q164 (_ BitVec 10)) (q165 (_ BitVec 10)) (q166 (_ BitVec 10)) (q167 (_ BitVec 10)) (q168 (_ BitVec 10)) (q169 (_ BitVec 10)) (q170 (_ BitVec 10)) (q171 (_ BitVec 10)) (q172 (_ BitVec 10)) (q173 (_ BitVec 10)) (q174 (_ BitVec 10)) (q175 (_ BitVec 10)) (q176 (_ BitVec 10)) (q177 (_ BitVec 8))) (=> (= q164 q161) (bvsgt q177 (bvnor q177 q177)))))
(assert (forall ((q199 (_ BitVec 10)) (q200 (_ BitVec 10)) (q201 (_ BitVec 10)) (q202 (_ BitVec 10)) (q203 (_ BitVec 10)) (q204 (_ BitVec 10)) (q205 (_ BitVec 10)) (q206 (_ BitVec 10)) (q207 (_ BitVec 10)) (q208 (_ BitVec 10)) (q209 (_ BitVec 10)) (q210 (_ BitVec 10)) (q211 (_ BitVec 10)) (q212 (_ BitVec 10)) (q213 (_ BitVec 10)) (q214 (_ BitVec 10)) (q215 (_ BitVec 10)) (q216 (_ BitVec 10)) (q217 (_ BitVec 12))) (=> (distinct (bvsdiv q217 q217) (bvsmod q217 (bvsdiv q217 q217))) (= q209 q199))))
(assert (forall ((q225 (_ BitVec 10)) (q226 (_ BitVec 10)) (q227 (_ BitVec 10)) (q228 (_ BitVec 10)) (q229 (_ BitVec 10)) (q230 (_ BitVec 10)) (q231 (_ BitVec 10)) (q232 (_ BitVec 10)) (q233 (_ BitVec 10)) (q234 (_ BitVec 10)) (q235 (_ BitVec 10)) (q236 (_ BitVec 10)) (q237 (_ BitVec 16))) (=> (distinct q237 q237) (bvult q233 q231))))
(declare-const bv_4-2 (_ BitVec 4))
(assert (forall ((q238 (_ BitVec 10)) (q239 (_ BitVec 10)) (q240 (_ BitVec 10)) (q241 (_ BitVec 10)) (q242 (_ BitVec 10)) (q243 (_ BitVec 10)) (q244 (_ BitVec 10)) (q245 (_ BitVec 10)) (q246 (_ BitVec 10)) (q247 (_ BitVec 10)) (q248 (_ BitVec 10)) (q249 (_ BitVec 10)) (q250 (_ BitVec 10)) (q251 (_ BitVec 10)) (q252 (_ BitVec 10)) (q253 (_ BitVec 10)) (q254 (_ BitVec 10)) (q255 (_ BitVec 29))) (=> (bvslt (bvsmod q255 q255) q255) (= q249 q248))))
(assert (forall ((q256 (_ BitVec 10)) (q257 (_ BitVec 10)) (q258 (_ BitVec 10)) (q259 (_ BitVec 10)) (q260 (_ BitVec 10)) (q261 (_ BitVec 10)) (q262 (_ BitVec 4))) (=> (bvugt q257 q259) (= (bvashr q262 q262) q262))))
(assert (forall ((q263 (_ BitVec 10)) (q264 (_ BitVec 10)) (q265 (_ BitVec 10)) (q266 (_ BitVec 10)) (q267 (_ BitVec 10)) (q268 (_ BitVec 10)) (q269 (_ BitVec 9))) (=> (bvsgt (bvadd q269 q269) (bvadd q269 q269)) (= q268 q268))))
(assert (forall ((q270 (_ BitVec 10)) (q271 (_ BitVec 10)) (q272 (_ BitVec 10)) (q273 (_ BitVec 10)) (q274 (_ BitVec 10)) (q275 (_ BitVec 10)) (q276 (_ BitVec 10)) (q277 (_ BitVec 10)) (q278 (_ BitVec 10)) (q279 (_ BitVec 10)) (q280 (_ BitVec 4))) (=> (distinct q279 q276) (= (bvor q280 q280) q280))))
(assert (forall ((q287 (_ BitVec 10)) (q288 (_ BitVec 10)) (q289 (_ BitVec 10)) (q290 (_ BitVec 10)) (q291 (_ BitVec 10)) (q292 (_ BitVec 10)) (q293 (_ BitVec 10)) (q294 (_ BitVec 10)) (q295 (_ BitVec 10)) (q296 (_ BitVec 10)) (q297 (_ BitVec 10)) (q298 (_ BitVec 10)) (q299 (_ BitVec 10)) (q300 (_ BitVec 10)) (q301 (_ BitVec 10)) (q302 (_ BitVec 10)) (q303 (_ BitVec 10)) (q304 (_ BitVec 10)) (q305 (_ BitVec 10)) (q306 (_ BitVec 10)) (q307 (_ BitVec 9))) (=> (= (bvnot q307) q307) (distinct q304 q304))))
(assert (forall ((q308 (_ BitVec 10)) (q309 (_ BitVec 10)) (q310 (_ BitVec 10)) (q311 (_ BitVec 10)) (q312 (_ BitVec 10)) (q313 (_ BitVec 10)) (q314 (_ BitVec 17))) (=> (bvslt q312 q312) (distinct (bvneg q314) (bvnot q314)))))
(assert (forall ((q315 (_ BitVec 10)) (q316 (_ BitVec 10)) (q317 (_ BitVec 10)) (q318 (_ BitVec 10)) (q319 (_ BitVec 10)) (q320 (_ BitVec 10)) (q321 (_ BitVec 10)) (q322 (_ BitVec 10)) (q323 (_ BitVec 10)) (q324 (_ BitVec 10)) (q325 (_ BitVec 10)) (q326 (_ BitVec 10)) (q327 (_ BitVec 10)) (q328 (_ BitVec 29))) (=> (distinct (bvmul q328 q328) (bvmul q328 q328)) (distinct (bvsmod q318 q326) q315))))
(assert (forall ((q329 (_ BitVec 10)) (q330 (_ BitVec 10)) (q331 (_ BitVec 10)) (q332 (_ BitVec 10)) (q333 (_ BitVec 10)) (q334 (_ BitVec 10)) (q335 (_ BitVec 10)) (q336 (_ BitVec 10)) (q337 (_ BitVec 10)) (q338 (_ BitVec 10)) (q339 (_ BitVec 10)) (q340 (_ BitVec 10)) (q341 (_ BitVec 9))) (=> (bvult (bvurem q341 q341) (bvsmod q341 q341)) (bvsgt q333 q334))))
(declare-const bv_9-1 (_ BitVec 9))
(assert (forall ((q342 (_ BitVec 10)) (q343 (_ BitVec 10)) (q344 (_ BitVec 10)) (q345 (_ BitVec 10)) (q346 (_ BitVec 10)) (q347 (_ BitVec 10)) (q348 (_ BitVec 10)) (q349 (_ BitVec 10)) (q350 (_ BitVec 10)) (q351 (_ BitVec 10)) (q352 (_ BitVec 10)) (q353 (_ BitVec 10)) (q354 (_ BitVec 10)) (q355 (_ BitVec 10)) (q356 (_ BitVec 10)) (q357 (_ BitVec 10)) (q358 (_ BitVec 10)) (q359 (_ BitVec 16))) (=> (distinct q345 q354) (= (bvsub q359 q359) (bvsub q359 q359)))))
(assert (forall ((q360 (_ BitVec 10)) (q361 (_ BitVec 10)) (q362 (_ BitVec 10)) (q363 (_ BitVec 10)) (q364 (_ BitVec 10)) (q365 (_ BitVec 10)) (q366 (_ BitVec 16))) (=> (= q366 q366) (= q360 q365))))
(declare-const bv_2-0 (_ BitVec 2))
(assert (forall ((q367 (_ BitVec 10)) (q368 (_ BitVec 10)) (q369 (_ BitVec 10)) (q370 (_ BitVec 10)) (q371 (_ BitVec 10)) (q372 (_ BitVec 10)) (q373 (_ BitVec 10)) (q374 (_ BitVec 10)) (q375 (_ BitVec 10)) (q376 (_ BitVec 10)) (q377 (_ BitVec 10)) (q378 (_ BitVec 3))) (=> (bvsge q376 q376) (distinct (bvand q378 q378) (bvand (bvand q378 q378) q378)))))
(assert (forall ((q379 (_ BitVec 10)) (q380 (_ BitVec 10)) (q381 (_ BitVec 10)) (q382 (_ BitVec 10)) (q383 (_ BitVec 10)) (q384 (_ BitVec 10)) (q385 (_ BitVec 10)) (q386 (_ BitVec 10)) (q387 (_ BitVec 10)) (q388 (_ BitVec 10)) (q389 (_ BitVec 10)) (q390 (_ BitVec 10)) (q391 (_ BitVec 10)) (q392 (_ BitVec 10)) (q393 (_ BitVec 9))) (=> (distinct (bvsub q382 q387) q383) (distinct (bvsub q393 q393) (bvadd q393 (bvsub q393 q393))))))
(assert (forall ((q394 (_ BitVec 10)) (q395 (_ BitVec 2))) (=> (= q395 q395) (= q394 q394))))
(declare-const bv_13-0 (_ BitVec 13))
(declare-const bv_8-4 (_ BitVec 8))
(assert (forall ((q398 (_ BitVec 10)) (q399 (_ BitVec 10)) (q400 (_ BitVec 10)) (q401 (_ BitVec 10)) (q402 (_ BitVec 10)) (q403 (_ BitVec 13))) (=> (distinct q402 q400) (= (bvnot (bvlshr q403 q403)) (bvashr (bvnand q403 q403) (bvnand q403 q403))))))
(assert (forall ((q404 (_ BitVec 10)) (q405 (_ BitVec 9))) (=> (bvsge q405 q405) (= q404 (bvudiv q404 q404)))))
(assert (forall ((q406 (_ BitVec 10)) (q407 (_ BitVec 10)) (q408 (_ BitVec 10)) (q409 (_ BitVec 4))) (=> (= q409 q409) (distinct q408 (bvand q406 q407)))))
(assert (forall ((q410 (_ BitVec 10)) (q411 (_ BitVec 10)) (q412 (_ BitVec 10)) (q413 (_ BitVec 10)) (q414 (_ BitVec 10)) (q415 (_ BitVec 10)) (q416 (_ BitVec 10)) (q417 (_ BitVec 10)) (q418 (_ BitVec 10)) (q419 (_ BitVec 10)) (q420 (_ BitVec 10)) (q421 (_ BitVec 10)) (q422 (_ BitVec 10)) (q423 (_ BitVec 10)) (q424 (_ BitVec 10)) (q425 (_ BitVec 10)) (q426 (_ BitVec 10)) (q427 (_ BitVec 10)) (q428 (_ BitVec 29))) (=> (distinct q415 q427) (= (bvurem q428 q428) q428))))
(assert (forall ((q429 (_ BitVec 10)) (q430 (_ BitVec 10)) (q431 (_ BitVec 10)) (q432 (_ BitVec 10)) (q433 (_ BitVec 10)) (q434 (_ BitVec 10)) (q435 (_ BitVec 10)) (q436 (_ BitVec 10)) (q437 (_ BitVec 10)) (q438 (_ BitVec 10)) (q439 (_ BitVec 10)) (q440 (_ BitVec 10)) (q441 (_ BitVec 10)) (q442 Bool)) (=> (= q437 q434) (or q442 q442 q442 q442 q442))))
(assert (forall ((q443 (_ BitVec 10)) (q444 (_ BitVec 10)) (q445 (_ BitVec 10)) (q446 (_ BitVec 10)) (q447 (_ BitVec 10)) (q448 (_ BitVec 10)) (q449 (_ BitVec 10)) (q450 (_ BitVec 10)) (q451 (_ BitVec 10)) (q452 (_ BitVec 10)) (q453 (_ BitVec 10)) (q454 (_ BitVec 10)) (q455 (_ BitVec 10)) (q456 (_ BitVec 10)) (q457 (_ BitVec 10)) (q458 (_ BitVec 10)) (q459 (_ BitVec 10)) (q460 (_ BitVec 10)) (q461 (_ BitVec 10)) (q462 (_ BitVec 10)) (q463 (_ BitVec 10)) (q464 (_ BitVec 13))) (=> (= q443 q450) (= q464 q464))))
(assert (forall ((q465 (_ BitVec 10)) (q466 (_ BitVec 10)) (q467 (_ BitVec 10)) (q468 (_ BitVec 10)) (q469 (_ BitVec 10)) (q470 (_ BitVec 10)) (q471 (_ BitVec 10)) (q472 (_ BitVec 10)) (q473 (_ BitVec 10)) (q474 (_ BitVec 10)) (q475 (_ BitVec 10)) (q476 (_ BitVec 10)) (q477 (_ BitVec 10)) (q478 (_ BitVec 10)) (q479 Bool)) (=> (and q479 q479 q479 q479 q479 q479 q479) (distinct (bvmul q477 q467) q478))))
(assert (forall ((q480 (_ BitVec 10)) (q481 (_ BitVec 10)) (q482 (_ BitVec 10)) (q483 (_ BitVec 10)) (q484 (_ BitVec 10)) (q485 (_ BitVec 10)) (q486 (_ BitVec 10)) (q487 (_ BitVec 10)) (q488 (_ BitVec 10)) (q489 (_ BitVec 10)) (q490 (_ BitVec 10)) (q491 (_ BitVec 10)) (q492 (_ BitVec 10)) (q493 (_ BitVec 10)) (q494 (_ BitVec 10)) (q495 (_ BitVec 10)) (q496 (_ BitVec 29))) (=> (bvuge (bvand (bvsrem q496 q496) q496) (bvand (bvsrem q496 q496) q496)) (= q493 q483))))
(declare-const bv_2-1 (_ BitVec 2))
(assert (forall ((q518 (_ BitVec 10)) (q519 (_ BitVec 10)) (q520 (_ BitVec 10)) (q521 (_ BitVec 10)) (q522 (_ BitVec 10)) (q523 (_ BitVec 10)) (q524 (_ BitVec 10)) (q525 (_ BitVec 10)) (q526 (_ BitVec 10)) (q527 (_ BitVec 10)) (q528 (_ BitVec 10)) (q529 (_ BitVec 10)) (q530 (_ BitVec 10)) (q531 (_ BitVec 10)) (q532 (_ BitVec 10)) (q533 (_ BitVec 10)) (q534 (_ BitVec 10)) (q535 (_ BitVec 10)) (q536 (_ BitVec 10)) (q537 (_ BitVec 13))) (=> (bvule q521 (bvsmod q535 q524)) (distinct (bvsmod (bvshl q537 q537) (bvsrem q537 q537)) q537))))
(assert (forall ((q538 (_ BitVec 10)) (q539 (_ BitVec 10)) (q540 (_ BitVec 16))) (=> (distinct (bvor q538 q539) (bvor q538 q539)) (bvult (bvsmod q540 q540) q540))))
(assert (forall ((q541 (_ BitVec 10)) (q542 (_ BitVec 10)) (q543 (_ BitVec 10)) (q544 (_ BitVec 10)) (q545 (_ BitVec 10)) (q546 (_ BitVec 10)) (q547 (_ BitVec 10)) (q548 (_ BitVec 10)) (q549 (_ BitVec 10)) (q550 (_ BitVec 10)) (q551 (_ BitVec 10)) (q552 (_ BitVec 10)) (q553 (_ BitVec 10)) (q554 (_ BitVec 10)) (q555 (_ BitVec 10)) (q556 (_ BitVec 8))) (=> (bvslt q556 q556) (distinct q544 q552))))
(assert (forall ((q557 (_ BitVec 10)) (q558 (_ BitVec 10)) (q559 (_ BitVec 10)) (q560 (_ BitVec 10)) (q561 (_ BitVec 10)) (q562 (_ BitVec 10)) (q563 (_ BitVec 10)) (q564 (_ BitVec 10)) (q565 (_ BitVec 10)) (q566 (_ BitVec 10)) (q567 (_ BitVec 10)) (q568 (_ BitVec 10)) (q569 (_ BitVec 16))) (=> (= q564 q557) (= (bvshl q569 q569) (bvadd (bvshl q569 q569) (bvmul q569 (bvshl q569 q569)))))))
(assert (forall ((q570 (_ BitVec 10)) (q571 (_ BitVec 10)) (q572 (_ BitVec 10)) (q573 (_ BitVec 10)) (q574 (_ BitVec 10)) (q575 (_ BitVec 10)) (q576 (_ BitVec 10)) (q577 (_ BitVec 10)) (q578 (_ BitVec 10)) (q579 (_ BitVec 10)) (q580 (_ BitVec 10)) (q581 Bool)) (=> (bvsle q571 q580) (= q581 q581))))
(assert (forall ((q582 (_ BitVec 10)) (q583 (_ BitVec 10)) (q584 (_ BitVec 10)) (q585 (_ BitVec 10)) (q586 (_ BitVec 10)) (q587 (_ BitVec 9))) (=> (distinct (bvlshr q587 (bvlshr q587 q587)) (bvlshr q587 (bvlshr q587 q587))) (distinct q583 q586))))
(assert (forall ((q588 (_ BitVec 10)) (q589 (_ BitVec 10)) (q590 (_ BitVec 10)) (q591 (_ BitVec 10)) (q592 (_ BitVec 10)) (q593 (_ BitVec 10)) (q594 (_ BitVec 10)) (q595 (_ BitVec 10)) (q596 (_ BitVec 10)) (q597 (_ BitVec 10)) (q598 (_ BitVec 10)) (q599 (_ BitVec 10)) (q600 (_ BitVec 10)) (q601 (_ BitVec 10)) (q602 (_ BitVec 29))) (=> (distinct q602 q602) (distinct q600 q597))))
(assert (forall ((q603 (_ BitVec 10)) (q604 (_ BitVec 10)) (q605 (_ BitVec 10)) (q606 (_ BitVec 10)) (q607 (_ BitVec 10)) (q608 (_ BitVec 10)) (q609 (_ BitVec 10)) (q610 (_ BitVec 10)) (q611 (_ BitVec 10)) (q612 (_ BitVec 10)) (q613 (_ BitVec 10)) (q614 (_ BitVec 10)) (q615 (_ BitVec 10)) (q616 (_ BitVec 29))) (=> (= q616 q616) (distinct (bvand q612 q607) q612))))
(declare-const bv_18-0 (_ BitVec 18))
(assert (forall ((q617 (_ BitVec 10)) (q618 (_ BitVec 10)) (q619 (_ BitVec 10)) (q620 (_ BitVec 11))) (=> (distinct q620 q620) (bvugt (bvudiv q619 q617) (bvudiv q619 q617)))))
(assert (forall ((q644 (_ BitVec 10)) (q645 (_ BitVec 10)) (q646 (_ BitVec 10)) (q647 (_ BitVec 10)) (q648 (_ BitVec 10)) (q649 (_ BitVec 10)) (q650 (_ BitVec 10)) (q651 (_ BitVec 10)) (q652 (_ BitVec 10)) (q653 (_ BitVec 10)) (q654 (_ BitVec 10)) (q655 (_ BitVec 10)) (q656 (_ BitVec 10)) (q657 (_ BitVec 10)) (q658 (_ BitVec 10)) (q659 (_ BitVec 10)) (q660 (_ BitVec 10)) (q661 (_ BitVec 11))) (=> (distinct q651 q660) (bvult (bvshl q661 q661) (bvsrem q661 (bvshl q661 q661))))))
(assert (forall ((q662 (_ BitVec 10)) (q663 (_ BitVec 10)) (q664 (_ BitVec 10)) (q665 (_ BitVec 8))) (=> (distinct q662 q663) (= (bvshl q665 (bvadd q665 q665)) q665))))
(declare-const bv_15-0 (_ BitVec 15))
(assert (forall ((q666 (_ BitVec 10)) (q667 (_ BitVec 10)) (q668 (_ BitVec 10)) (q669 (_ BitVec 10)) (q670 (_ BitVec 10)) (q671 (_ BitVec 10)) (q672 (_ BitVec 10)) (q673 (_ BitVec 16))) (=> (bvult q668 q672) (= q673 (bvsdiv q673 (bvsub q673 q673))))))
(assert (forall ((q674 (_ BitVec 10)) (q675 (_ BitVec 10)) (q676 (_ BitVec 10)) (q677 (_ BitVec 10)) (q678 (_ BitVec 29))) (=> (bvult q678 (bvneg q678)) (bvule q676 q674))))
(check-sat)

Eldarica nightly (http://philipp.ruemmer.org/eldarica-bin-nightly.zip) throws an assertion error

 Theories: GroebnerMultiplication, ModuloArithmetic
 Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.util.Debug$.assertTrue(Debug.scala:111)
        at ap.util.Debug$.assertInt(Debug.scala:144)
        at ap.theories.bitvectors.LShiftCastSplitter$$anonfun$shiftCastActions$3.apply(ShiftCastSplitter.scala:152)
        at ap.theories.bitvectors.LShiftCastSplitter$$anonfun$shiftCastActions$3.apply(ShiftCastSplitter.scala:75)
        at scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
        at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
        at ap.theories.bitvectors.LShiftCastSplitter$.shiftCastActions(ShiftCastSplitter.scala:75)
        at ap.theories.bitvectors.ModPlugin$.modShiftCast(ModPlugin.scala:209)
        at ap.theories.bitvectors.ModPlugin$.handleGoal(ModPlugin.scala:166)
        at ap.proof.theoryPlugins.PluginSequence.handleGoal(Plugin.scala:238)                                                                                                                    
        at ap.proof.theoryPlugins.PluginTask.apply(Plugin.scala:392)
        at ap.proof.goal.Goal.step(Goal.scala:395)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:470)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1079)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1069)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidity(ModelSearchProver.scala:1057)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply$mcZ$sp(HornPredAbs.scala:703)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply(HornPredAbs.scala:694)
。。

'-assert', '-abstract:term',

rainoftime commented 4 years ago

Besides, https://github.com/uuverifiers/eldarica/issues/19 seems not fixed in the latest nightly build above.

pruemmer commented 4 years ago

I have not updated the snapshot on philipp.ruemmer.org; but the problem should be fixed in the release version?

När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

pruemmer commented 4 years ago

I have not updated the snapshot on philipp.ruemmer.org; but the problem should be fixed in the release version?

rainoftime commented 4 years ago

At commit 31d9075b7, this issue remains.

pruemmer commented 4 years ago

Yes, sorry for the confusion, I meant that #19 is fixed! This issue I have not yet looked into ...

pruemmer commented 4 years ago

In version f817bc3 this should be fixed!