search

uuverifiers / eldarica

The Eldarica model checker
Other
80 stars 23 forks source link

AssertionError at Predef.scala:156 (HornWrapper.scala:102) #26

Open rainoftime opened 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_3-0 (_ BitVec 3))
(assert (forall ((q0 (_ BitVec 7)) (q1 (_ BitVec 7)) (q2 (_ BitVec 7)) (q3 (_ BitVec 7)) (q4 (_ BitVec 7)) (q5 (_ BitVec 10))) (=> (distinct q2 q2) (bvslt (bvor q5 q5) (bvor q5 q5)))))
(assert (forall ((q6 (_ BitVec 7)) (q7 (_ BitVec 7)) (q8 (_ BitVec 7)) (q9 (_ BitVec 7)) (q10 (_ BitVec 10))) (=> (bvslt (bvsmod q10 (bvlshr q10 q10)) (bvlshr q10 q10)) (distinct (bvnot q8) (bvnot q8)))))
(assert (forall ((q11 (_ BitVec 7)) (q12 (_ BitVec 7)) (q13 (_ BitVec 7)) (q14 (_ BitVec 7)) (q15 (_ BitVec 7)) (q16 (_ BitVec 7)) (q17 (_ BitVec 7)) (q18 (_ BitVec 7)) (q19 (_ BitVec 7)) (q20 (_ BitVec 7
)) (q21 (_ BitVec 7)) (q22 (_ BitVec 7)) (q23 (_ BitVec 7)) (q24 (_ BitVec 10))) (=> (= q22 (bvnot (bvadd q22 q20))) (= (bvlshr q24 q24) (bvlshr q24 q24)))))
(declare-const bv_8-0 (_ BitVec 8))
(assert (forall ((q25 (_ BitVec 7)) (q26 (_ BitVec 7)) (q27 (_ BitVec 7)) (q28 (_ BitVec 7)) (q29 (_ BitVec 7)) (q30 (_ BitVec 7)) (q31 (_ BitVec 7)) (q32 (_ BitVec 9))) (=> (distinct q26 q29) (bvsge (bvo
r q32 q32) (bvor q32 q32)))))
(assert (forall ((q33 (_ BitVec 7)) (q34 (_ BitVec 7)) (q35 (_ BitVec 7)) (q36 (_ BitVec 7)) (q37 (_ BitVec 7)) (q38 (_ BitVec 7)) (q39 (_ BitVec 7)) (q40 (_ BitVec 7)) (q41 (_ BitVec 7)) (q42 (_ BitVec 7
)) (q43 (_ BitVec 7)) (q44 (_ BitVec 7)) (q45 (_ BitVec 9))) (=> (= q36 q39) (bvugt (bvudiv q45 q45) q45))))
(assert (forall ((q46 (_ BitVec 7)) (q47 (_ BitVec 7)) (q48 (_ BitVec 8))) (=> (= q48 q48) (distinct (bvashr q47 (bvudiv q47 q46)) q46))))
(assert (forall ((q49 (_ BitVec 7)) (q50 (_ BitVec 7)) (q51 (_ BitVec 7)) (q52 (_ BitVec 7)) (q53 (_ BitVec 7)) (q54 (_ BitVec 7)) (q55 (_ BitVec 7)) (q56 (_ BitVec 7)) (q57 (_ BitVec 7)) (q58 (_ BitVec 7
)) (q59 (_ BitVec 7)) (q60 (_ BitVec 8))) (=> (bvuge q60 q60) (distinct q54 q56))))
(assert (forall ((q61 (_ BitVec 7)) (q62 (_ BitVec 7)) (q63 (_ BitVec 7)) (q64 (_ BitVec 7)) (q65 (_ BitVec 7)) (q66 (_ BitVec 7)) (q67 (_ BitVec 7)) (q68 (_ BitVec 7)) (q69 (_ BitVec 7)) (q70 (_ BitVec 7
)) (q71 (_ BitVec 7)) (q72 (_ BitVec 9))) (=> (= q71 q66) (= q72 (bvashr q72 q72)))))
(assert (forall ((q73 (_ BitVec 7)) (q74 (_ BitVec 7)) (q75 (_ BitVec 12))) (=> (bvule (bvsrem q75 q75) q75) (= (bvor (bvadd q73 q73) (bvnot q74)) q74))))
(declare-const bv_20-0 (_ BitVec 20))
(assert (forall ((q76 (_ BitVec 7)) (q77 (_ BitVec 7)) (q78 (_ BitVec 8))) (=> (bvsgt q76 (bvsub q76 (bvurem q76 q77))) (distinct (bvand q78 q78) q78))))
(assert (forall ((q79 (_ BitVec 7)) (q80 (_ BitVec 7)) (q81 (_ BitVec 7)) (q82 (_ BitVec 7)) (q83 (_ BitVec 7)) (q84 (_ BitVec 7)) (q85 (_ BitVec 9))) (=> (bvule q81 q80) (distinct (bvnor (bvurem q85 q85)
 q85) (bvnor (bvurem q85 q85) q85)))))
(assert (forall ((q86 (_ BitVec 7)) (q87 (_ BitVec 7)) (q88 (_ BitVec 7)) (q89 (_ BitVec 7)) (q90 (_ BitVec 7)) (q91 (_ BitVec 7)) (q92 (_ BitVec 7)) (q93 (_ BitVec 7)) (q94 (_ BitVec 7)) (q95 (_ BitVec 2
0))) (=> (distinct q88 q86) (bvsge (bvsub q95 q95) q95))))
(assert (forall ((q96 (_ BitVec 7)) (q97 (_ BitVec 7)) (q98 (_ BitVec 7)) (q99 (_ BitVec 7)) (q100 (_ BitVec 7)) (q101 (_ BitVec 7)) (q102 (_ BitVec 7)) (q103 (_ BitVec 7)) (q104 (_ BitVec 7)) (q105 (_ Bi
tVec 7)) (q106 (_ BitVec 3))) (=> (distinct q100 q96) (distinct q106 q106))))
(assert (forall ((q107 (_ BitVec 7)) (q108 (_ BitVec 7)) (q109 (_ BitVec 7)) (q110 (_ BitVec 7)) (q111 (_ BitVec 7)) (q112 (_ BitVec 7)) (q113 (_ BitVec 7)) (q114 (_ BitVec 7)) (q115 (_ BitVec 7)) (q116 (
_ BitVec 7)) (q117 (_ BitVec 12))) (=> (bvugt q115 q111) (bvsle (bvashr q117 q117) (bvashr q117 q117)))))
(assert (forall ((q118 (_ BitVec 7)) (q119 (_ BitVec 7)) (q120 (_ BitVec 7)) (q121 (_ BitVec 7)) (q122 (_ BitVec 7)) (q123 (_ BitVec 7)) (q124 (_ BitVec 7)) (q125 (_ BitVec 7)) (q126 (_ BitVec 7)) (q127 (
_ BitVec 7)) (q128 (_ BitVec 7)) (q129 (_ BitVec 7)) (q130 (_ BitVec 7)) (q131 (_ BitVec 9))) (=> (bvsle q122 q127) (= (bvnot (bvsmod q131 q131)) (bvsmod q131 q131)))))
(assert (forall ((q133 (_ BitVec 7)) (q134 (_ BitVec 8))) (=> (bvsle q133 (bvashr q133 q133)) (bvsgt q134 q134))))
(assert (forall ((q135 (_ BitVec 7)) (q136 (_ BitVec 7)) (q137 (_ BitVec 7)) (q138 (_ BitVec 7)) (q139 (_ BitVec 9))) (=> (= (bvand q137 q135) q136) (= q139 q139))))
(assert (forall ((q140 (_ BitVec 7)) (q141 (_ BitVec 7)) (q142 (_ BitVec 7)) (q143 (_ BitVec 7)) (q144 (_ BitVec 7)) (q145 (_ BitVec 7)) (q146 (_ BitVec 7)) (q147 (_ BitVec 7)) (q148 (_ BitVec 7)) (q149 (
_ BitVec 9))) (=> (bvule q146 q142) (distinct q149 (bvsrem q149 q149)))))
(assert (forall ((q150 (_ BitVec 7)) (q151 (_ BitVec 7)) (q152 (_ BitVec 7)) (q153 (_ BitVec 7)) (q154 Bool)) (=> (= q151 (bvadd q151 q153)) (or q154 q154 q154 q154 q154 q154))))
(assert (forall ((q155 (_ BitVec 7)) (q156 (_ BitVec 7)) (q157 (_ BitVec 7)) (q158 (_ BitVec 7)) (q159 (_ BitVec 7)) (q160 (_ BitVec 7)) (q161 (_ BitVec 7)) (q162 (_ BitVec 7)) (q163 (_ BitVec 7)) (q164 (
_ BitVec 7)) (q165 (_ BitVec 7)) (q166 (_ BitVec 7)) (q167 (_ BitVec 8))) (=> (= q167 (bvsdiv q167 q167)) (bvsge q164 q162))))
(assert (forall ((q168 (_ BitVec 7)) (q169 (_ BitVec 7)) (q170 (_ BitVec 7)) (q171 (_ BitVec 7)) (q172 (_ BitVec 7)) (q173 (_ BitVec 7)) (q174 (_ BitVec 7)) (q175 (_ BitVec 7)) (q176 (_ BitVec 7)) (q177 (
_ BitVec 7)) (q178 (_ BitVec 7)) (q179 (_ BitVec 7)) (q180 (_ BitVec 7)) (q181 (_ BitVec 7)) (q182 (_ BitVec 3))) (=> (= (bvsmod q182 q182) (bvsmod q182 q182)) (= q171 q176))))
(assert (forall ((q183 (_ BitVec 7)) (q184 (_ BitVec 7)) (q185 (_ BitVec 7)) (q186 (_ BitVec 7)) (q187 (_ BitVec 7)) (q188 (_ BitVec 7)) (q189 (_ BitVec 8))) (=> (bvugt q184 (bvashr q188 q186)) (= (bvashr
 q189 q189) q189))))
(assert (forall ((q190 (_ BitVec 7)) (q191 (_ BitVec 7)) (q192 (_ BitVec 7)) (q193 (_ BitVec 7)) (q194 (_ BitVec 7)) (q195 (_ BitVec 7)) (q196 (_ BitVec 7)) (q197 (_ BitVec 7)) (q198 (_ BitVec 7)) (q199 (
_ BitVec 7)) (q200 (_ BitVec 7)) (q201 (_ BitVec 7)) (q202 (_ BitVec 7)) (q203 (_ BitVec 7)) (q204 (_ BitVec 9))) (=> (bvugt (bvshl q204 q204) (bvshl q204 q204)) (distinct q203 q190))))
(assert (forall ((q205 (_ BitVec 7)) (q206 (_ BitVec 7)) (q207 (_ BitVec 7)) (q208 (_ BitVec 7)) (q209 (_ BitVec 7)) (q210 (_ BitVec 7)) (q211 (_ BitVec 7)) (q212 (_ BitVec 7)) (q213 (_ BitVec 7)) (q214 (
_ BitVec 7)) (q215 (_ BitVec 8))) (=> (distinct q210 q207) (= (bvnand q215 q215) q215))))
(assert (forall ((q216 (_ BitVec 7)) (q217 (_ BitVec 7)) (q218 (_ BitVec 7)) (q219 (_ BitVec 7)) (q220 (_ BitVec 3))) (=> (distinct q220 (bvlshr q220 q220)) (distinct q218 (bvsrem q219 q217)))))
(assert (forall ((q221 (_ BitVec 7)) (q222 (_ BitVec 7)) (q223 Bool)) (=> (distinct q221 (bvadd q221 q221)) (distinct q223 q223))))
(assert (forall ((q224 (_ BitVec 7)) (q225 (_ BitVec 7)) (q226 (_ BitVec 7)) (q227 (_ BitVec 7)) (q228 (_ BitVec 7)) (q229 Bool)) (=> (not q229) (= (bvshl (bvneg q228) q228) q227))))
(declare-const bv_25-0 (_ BitVec 25))
(assert (forall ((q238 (_ BitVec 7)) (q239 (_ BitVec 7)) (q240 (_ BitVec 7)) (q241 (_ BitVec 7)) (q242 (_ BitVec 7)) (q243 (_ BitVec 7)) (q244 (_ BitVec 7)) (q245 (_ BitVec 7)) (q246 (_ BitVec 7)) (q247 (
_ BitVec 7)) (q248 (_ BitVec 3))) (=> (= (bvor q248 q248) (bvashr (bvor q248 q248) (bvor q248 q248))) (= q242 q247))))
(assert (forall ((q249 (_ BitVec 7)) (q250 (_ BitVec 7)) (q251 (_ BitVec 7)) (q252 (_ BitVec 7)) (q253 (_ BitVec 7)) (q254 (_ BitVec 7)) (q255 (_ BitVec 7)) (q256 (_ BitVec 7)) (q257 (_ BitVec 7)) (q258 (
_ BitVec 7)) (q259 (_ BitVec 3))) (=> (distinct (bvmul q259 q259) q259) (bvslt q249 q250))))
(assert (forall ((q260 (_ BitVec 7)) (q261 (_ BitVec 7)) (q262 (_ BitVec 7)) (q263 (_ BitVec 7)) (q264 (_ BitVec 7)) (q265 (_ BitVec 7)) (q266 (_ BitVec 7)) (q267 (_ BitVec 7)) (q268 (_ BitVec 7)) (q269 (
_ BitVec 7)) (q270 (_ BitVec 7)) (q271 (_ BitVec 7)) (q272 (_ BitVec 7)) (q273 (_ BitVec 7)) (q274 (_ BitVec 10))) (=> (distinct q272 (bvsub q262 q266)) (distinct (bvmul (bvnot q274) (bvnot q274)) (bvnot 
q274)))))
(assert (forall ((q275 (_ BitVec 7)) (q276 (_ BitVec 7)) (q277 (_ BitVec 7)) (q278 (_ BitVec 7)) (q279 (_ BitVec 7)) (q280 (_ BitVec 7)) (q281 (_ BitVec 7)) (q282 (_ BitVec 7)) (q283 (_ BitVec 4))) (=> (b
vsgt q279 q278) (bvugt (bvurem q283 q283) (bvurem q283 q283)))))
(assert (forall ((q284 (_ BitVec 7)) (q285 (_ BitVec 25))) (=> (distinct q284 q284) (= q285 (bvashr q285 q285)))))
(assert (forall ((q286 (_ BitVec 7)) (q287 (_ BitVec 7)) (q288 (_ BitVec 7)) (q289 (_ BitVec 7)) (q290 (_ BitVec 7)) (q291 (_ BitVec 7)) (q292 (_ BitVec 7)) (q293 (_ BitVec 7)) (q294 (_ BitVec 7)) (q295 (
_ BitVec 7)) (q296 (_ BitVec 7)) (q297 (_ BitVec 7)) (q298 (_ BitVec 7)) (q299 (_ BitVec 7)) (q300 (_ BitVec 4))) (=> (= q300 (bvnand q300 q300)) (= (bvsmod q290 q297) q295))))
(assert (forall ((q301 (_ BitVec 7)) (q302 (_ BitVec 7)) (q303 (_ BitVec 7)) (q304 (_ BitVec 7)) (q305 (_ BitVec 7)) (q306 (_ BitVec 7)) (q307 (_ BitVec 10))) (=> (bvsle q307 q307) (bvsgt q305 q301))))
(assert (forall ((q314 (_ BitVec 7)) (q315 (_ BitVec 7)) (q316 (_ BitVec 7)) (q317 (_ BitVec 7)) (q318 (_ BitVec 7)) (q319 (_ BitVec 7)) (q320 (_ BitVec 7)) (q321 (_ BitVec 7)) (q322 (_ BitVec 7)) (q323 (
_ BitVec 7)) (q324 (_ BitVec 7)) (q325 (_ BitVec 7)) (q326 (_ BitVec 7)) (q327 (_ BitVec 7)) (q328 (_ BitVec 3))) (=> (bvsle (bvnand q328 q328) q328) (bvuge q324 q321))))
(assert (forall ((q329 (_ BitVec 7)) (q330 (_ BitVec 7)) (q331 (_ BitVec 7)) (q332 (_ BitVec 7)) (q333 (_ BitVec 7)) (q334 (_ BitVec 7)) (q335 (_ BitVec 7)) (q336 (_ BitVec 7)) (q337 (_ BitVec 20))) (=> (
bvuge q329 q336) (distinct q337 (bvshl q337 q337)))))
(assert (forall ((q338 (_ BitVec 7)) (q339 (_ BitVec 7)) (q340 (_ BitVec 7)) (q341 (_ BitVec 7)) (q342 (_ BitVec 7)) (q343 (_ BitVec 7)) (q344 (_ BitVec 7)) (q345 (_ BitVec 7)) (q346 (_ BitVec 7)) (q347 (
_ BitVec 7)) (q348 (_ BitVec 7)) (q349 (_ BitVec 7)) (q350 (_ BitVec 7)) (q351 (_ BitVec 7)) (q352 (_ BitVec 7)) (q353 (_ BitVec 3))) (=> (= q353 q353) (bvugt q341 q342))))
(declare-const bv_31-0 (_ BitVec 31))
(assert (forall ((q354 (_ BitVec 7)) (q355 (_ BitVec 7)) (q356 (_ BitVec 7)) (q357 (_ BitVec 7)) (q358 (_ BitVec 7)) (q359 (_ BitVec 7)) (q360 (_ BitVec 7)) (q361 (_ BitVec 7)) (q362 (_ BitVec 10))) (=> (
= q357 (bvnor q361 q358)) (bvult (bvadd (bvlshr q362 q362) q362) (bvadd (bvlshr q362 q362) q362)))))
(assert (forall ((q363 (_ BitVec 7)) (q364 (_ BitVec 7)) (q365 (_ BitVec 7)) (q366 (_ BitVec 7)) (q367 (_ BitVec 20))) (=> (bvsle (bvurem q367 q367) (bvurem q367 q367)) (distinct q366 q363))))
(assert (forall ((q368 (_ BitVec 7)) (q369 (_ BitVec 3))) (=> (distinct q369 q369) (bvuge (bvadd q368 q368) (bvadd q368 q368)))))
(assert (forall ((q370 (_ BitVec 7)) (q371 (_ BitVec 7)) (q372 (_ BitVec 7)) (q373 (_ BitVec 7)) (q374 (_ BitVec 7)) (q375 (_ BitVec 7)) (q376 (_ BitVec 7)) (q377 (_ BitVec 3))) (=> (distinct q375 q372) (
= (bvshl (bvsmod q377 q377) (bvsmod q377 q377)) (bvsmod q377 q377)))))
(declare-const bv_24-0 (_ BitVec 24))
(assert (forall ((q395 (_ BitVec 7)) (q396 (_ BitVec 7)) (q397 (_ BitVec 7)) (q398 (_ BitVec 7)) (q399 (_ BitVec 7)) (q400 (_ BitVec 7)) (q401 (_ BitVec 7)) (q402 (_ BitVec 20))) (=> (bvult q401 q397) (= 
q402 (bvsrem q402 q402)))))
(assert (forall ((q403 (_ BitVec 7)) (q404 (_ BitVec 7)) (q405 (_ BitVec 7)) (q406 (_ BitVec 7)) (q407 (_ BitVec 7)) (q408 (_ BitVec 7)) (q409 (_ BitVec 7)) (q410 (_ BitVec 7)) (q411 (_ BitVec 7)) (q412 (
_ BitVec 7)) (q413 (_ BitVec 7)) (q414 (_ BitVec 8))) (=> (= q409 q408) (distinct (bvadd q414 (bvsdiv q414 q414)) (bvsdiv q414 q414)))))
(assert (forall ((q415 (_ BitVec 7)) (q416 (_ BitVec 7)) (q417 (_ BitVec 7)) (q418 (_ BitVec 7)) (q419 (_ BitVec 7)) (q420 (_ BitVec 7)) (q421 (_ BitVec 7)) (q422 (_ BitVec 7)) (q423 (_ BitVec 7)) (q424 (
_ BitVec 7)) (q425 (_ BitVec 31))) (=> (= q422 q419) (distinct (bvshl q425 q425) (bvshl q425 q425)))))
(assert (forall ((q426 (_ BitVec 7)) (q427 (_ BitVec 7)) (q428 (_ BitVec 7)) (q429 (_ BitVec 7)) (q430 (_ BitVec 7)) (q431 (_ BitVec 7)) (q432 (_ BitVec 7)) (q433 (_ BitVec 7)) (q434 (_ BitVec 7)) (q435 (
_ BitVec 7)) (q436 (_ BitVec 4))) (=> (bvule (bvashr q436 q436) (bvashr q436 q436)) (= q428 (bvsrem q433 q432)))))
(assert (forall ((q437 (_ BitVec 7)) (q438 (_ BitVec 7)) (q439 (_ BitVec 7)) (q440 (_ BitVec 7)) (q441 (_ BitVec 7)) (q442 (_ BitVec 7)) (q443 (_ BitVec 7)) (q444 (_ BitVec 7)) (q445 (_ BitVec 7)) (q446 (
_ BitVec 7)) (q447 (_ BitVec 7)) (q448 (_ BitVec 7)) (q449 (_ BitVec 7)) (q450 (_ BitVec 20))) (=> (= q450 (bvshl q450 q450)) (= q438 q443))))
(assert (forall ((q451 (_ BitVec 7)) (q452 (_ BitVec 7)) (q453 (_ BitVec 7)) (q454 (_ BitVec 7)) (q455 (_ BitVec 7)) (q456 (_ BitVec 7)) (q457 (_ BitVec 7)) (q458 (_ BitVec 7)) (q459 (_ BitVec 7)) (q460 (
_ BitVec 7)) (q461 (_ BitVec 7)) (q462 (_ BitVec 7)) (q463 (_ BitVec 7)) (q464 (_ BitVec 7)) (q465 (_ BitVec 7)) (q466 (_ BitVec 12))) (=> (bvugt q452 q457) (bvsgt q466 q466))))
(assert (forall ((q467 (_ BitVec 7)) (q468 (_ BitVec 7)) (q469 (_ BitVec 7)) (q470 (_ BitVec 7)) (q471 (_ BitVec 7)) (q472 (_ BitVec 7)) (q473 (_ BitVec 7)) (q474 (_ BitVec 10))) (=> (= (bvnor q474 q474) 
(bvnor q474 q474)) (= (bvmul q473 (bvshl q470 q473)) q469))))
(assert (forall ((q475 (_ BitVec 7)) (q476 (_ BitVec 7)) (q477 (_ BitVec 7)) (q478 (_ BitVec 7)) (q479 (_ BitVec 7)) (q480 (_ BitVec 7)) (q481 (_ BitVec 7)) (q482 (_ BitVec 7)) (q483 (_ BitVec 7)) (q484 (
_ BitVec 7)) (q485 Bool)) (=> (and q485 q485 q485 q485 q485 q485) (bvsge (bvnot q484) (bvnot q484)))))
(check-sat)

eldarica 31d9075

'-assert', '-noSlicing', '-abstract:oct'
Theories: GroebnerMultiplication, ModuloArithmetic
 Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at lazabs.horn.bottomup.HornWrapper$.verifyCEX(HornWrapper.scala:102)
        at lazabs.horn.bottomup.InnerHornWrapper.<init>(HornWrapper.scala:443)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:254)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:256)
        at lazabs.ParallelComputation$.apply(ParallelComputation.scala:46)
        at lazabs.horn.bottomup.HornWrapper.<init>(HornWrapper.scala:253)
        at lazabs.horn.Solve$.apply(Solve.scala:81)
        at lazabs.Main$.doMain(Main.scala:601)
        at lazabs.Main$.main(Main.scala:271)
        at lazabs.Main.main(Main.scala)