AssertionError at Predef.scala:156 (ConjunctEliminator.scala:558)
Closed this issue · 2 comments
rainoftime commented
Hi, for the following instance,
(set-logic HORN)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const bv_15-0 (_ BitVec 15))
(assert (forall ((q1 (_ BitVec 9)) (q2 (_ BitVec 9)) (q3 (_ BitVec 9)) (q4 (_ BitVec 10))) (=> (= q4 q4) (= (bvnor q2 (bvsrem q1 q2)) (bvnor q2 (bvsrem q1 q2))))))
(assert (forall ((q5 (_ BitVec 9)) (q6 (_ BitVec 9)) (q7 (_ BitVec 9)) (q8 (_ BitVec 9)) (q9 (_ BitVec 15))) (=> (= q9 q9) (distinct (bvneg q7) (bvneg q7)))))
(check-sat)
(exit)
Eldarica nightly (http://philipp.ruemmer.org/eldarica-bin-nightly.zip)
throws an assertion error
Theories: GroebnerMultiplication, ModuloArithmetic [59/1922]
Exception in thread "main" java.lang.AssertionError: assertion failed
at scala.Predef$.assert(Predef.scala:156)
at ap.terfor.conjunctions.ConjunctEliminator.ap$terfor$conjunctions$ConjunctEliminator$$eliminableDivInEqs(ConjunctEliminator.scala:558)
at ap.terfor.conjunctions.ConjunctEliminator$$anonfun$eliminate$1.apply(ConjunctEliminator.scala:720)
at ap.terfor.conjunctions.ConjunctEliminator$$anonfun$eliminate$1.apply(ConjunctEliminator.scala:694)
at scala.collection.Iterator$class.foreach(Iterator.scala:891)
at ap.util.FilterIt.foreach(FilterIt.scala:35)
at ap.terfor.conjunctions.ConjunctEliminator.eliminate(ConjunctEliminator.scala:694)
at ap.proof.goal.EliminateFactsTask$.apply(EliminateFactsTask.scala:45)
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:589)
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.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
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.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
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)
...
Options
-assert -noSlicing -abstract:relIneqs
rainoftime commented
Another instance with option -abstract:relIneqs
(set-logic HORN)
(declare-fun inv-int1 (Int Int) Bool)
(declare-fun inv-int2 (Int Int Int) Bool)
(declare-fun inv-int3 (Int Int Int Int) Bool)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const i1 Int)
(declare-const i3 Int)
(assert (forall ((q9 Int) (q10 Int) (q11 Bool)) (=> (distinct (div 333 398) 97 q9) (distinct q11 q11 q11 q11 q11 q11))))
(assert (forall ((q12 Int) (q13 Int) (q14 Int) (q15 Bool)) (=> (=> q15 q15) (> 160 165 (+ q12 420 (- q14 q13 q12 420) q12 420) 376))))
(assert (forall ((q16 Int) (q17 Int) (q18 Int) (q19 Int) (q20 Bool)) (=> (=> q20 q20) (= 451 210 946))))
(assert (forall ((q21 Int) (q22 Int) (q23 Int) (q24 Int) (q25 Int) (q26 Int) (q27 Bool)) (=> (not q27) (>= (- q25) (- q24 160 q26)))))
(assert (forall ((q28 Int) (q29 Int) (q30 Int) (q31 Bool)) (=> (distinct q31 q31 q31 q31 q31 q31 q31) (>= 224 (- q28)))))
(assert (forall ((q32 Int) (q33 Int) (q34 Int) (q35 Int) (q36 Int) (q37 Int) (q38 Bool)) (=> (= q38 q38 q38 q38) (>= q36 q34 q35 q33))))
(assert (forall ((q39 Int) (q40 Int) (q41 Int) (q42 Int) (q43 Bool)) (=> (and q43 q43 q43 q43 q43 q43 q43 q43 q43) (distinct (mod q40 667) (div 355 927)))))
(assert (forall ((q44 Int) (q45 Bool)) (=> (or q45 q45 q45 q45 q45 q45 q45) (< q44 (+ 765 (div 153 153) 633 903 q44)))))
(assert (forall ((q46 Int) (q47 Int) (q48 Int) (q49 Int) (q50 Int) (q51 Int) (q52 Bool)) (=> (or q52 q52 q52 q52 q52 q52 q52 q52 q52) (<= (div 739 (mod 771 909)) (mod 548 21)))))
(assert (forall ((q53 Int) (q54 Bool)) (=> (and q54 q54 q54 q54 q54 q54 q54 q54) (>= 556 (+ 315 556 841 556 315)))))
(assert (forall ((q62 Int) (q63 Int) (q64 Int) (q65 Int) (q66 Int) (q67 Bool)) (=> (not q67) (< 692 (- 817 817) 799 692))))
(assert (forall ((q69 Int) (q70 Int) (q71 Bool)) (=> (< (- q70) 538 80 292) (not q71))))
(assert (forall ((q83 Int) (q84 Int) (q85 Bool)) (=> (= q85 q85 q85 q85 q85 q85 q85) (< 351 q84 444 679))))
(assert (forall ((q86 Int) (q87 Int) (q88 Int) (q89 Int) (q90 Int) (q91 Bool)) (=> (and q91 q91 q91 q91 q91 q91 q91 q91) (>= 5 737))))
(assert (forall ((q92 Int) (q93 Int) (q94 Int) (q95 Int) (q96 Int) (q97 Bool)) (=> (distinct (div q93 733) 296) (or q97 q97 q97 q97 q97))))
(assert (forall ((q98 Int) (q99 Int) (q100 Int) (q101 Int) (q102 Bool)) (=> (> q98 549) (= q102 q102 q102 q102 q102))))
(assert (forall ((q108 Int) (q109 Int) (q110 Bool)) (=> (= (- 399) 399) (and q110 q110 q110 q110))))
(assert (forall ((q116 Int) (q117 Int) (q118 Bool)) (=> (and q118 q118 q118 q118) (>= 803 (- 803)))))
(assert (forall ((q126 Int) (q127 Int) (q128 Int) (q129 Int) (q130 Int) (q131 Bool)) (=> (not q131) (>= 402 (div 292 802)))))
(assert (forall ((q138 Int) (q139 Int) (q140 Bool)) (=> (= q138 812 (- 812 (- q138 576) 576 q139)) (or q140 q140 q140 q140 q140 q140 q140 q140))))
(assert (forall ((q141 Int) (q142 Int) (q143 Int) (q144 Bool)) (=> (not q144) (= (* 825 (mod q142 654) (mod 180 (mod 654 654)) 105) 653 (- 180 q142 105)))))
(assert (forall ((q154 Int) (q155 Int) (q156 Int) (q157 Bool)) (=> (or q157 q157 q157 q157) (> (+ q155 q155 652 968) 903 204 (mod 411 862)))))
(assert (forall ((q161 Int) (q162 Int) (q163 Int) (q164 Int) (q165 Int) (q166 Bool)) (=> (>= 502 q164) (not q166))))
(assert (forall ((q167 Int) (q168 Int) (q169 Bool)) (=> (distinct 130 q167 q168 (mod 843 623)) (distinct q169 q169 q169 q169 q169 q169))))
(assert (forall ((q174 Int) (q175 Int) (q176 Int) (q177 Int) (q178 Int) (q179 Int) (q180 Bool)) (=> (and q180 q180 q180) (distinct q179 552))))
(assert (forall ((q181 Int) (q182 Int) (q183 Int) (q184 Int) (q185 Bool)) (=> (< q181 q184) (=> q185 q185))))
(assert (forall ((q200 Int) (q201 Int) (q202 Int) (q203 Bool)) (=> (>= (- 734 411) (+ 869 q200 q202) (+ 734 869 (- 734 411) (+ 869 q200 q202) 734) (+ q201 734 (+ 869 q200 q202) q202)) (= q203 q203))))
(assert (forall ((q208 Int) (q209 Int) (q210 Bool)) (=> (distinct 188 q208 q209) (distinct q210 q210))))
(assert (forall ((q227 Int) (q228 Bool)) (=> (or q228 q228 q228 q228 q228 q228) (<= (div 996 996) 994))))
(assert (forall ((q229 Int) (q230 Int) (q231 Int) (q232 Int) (q233 Int) (q234 Bool)) (=> (not q234) (<= q232 272))))
(assert (forall ((q244 Int) (q245 Int) (q246 Int) (q247 Int) (q248 Int) (q249 Int) (q250 Bool)) (=> (= q250 q250 q250 q250 q250) (< (div q245 310) 664))))
(assert (forall ((q251 Int) (q252 Bool)) (=> (< (abs 701) 145 q251) (or q252 q252 q252 q252 q252 q252))))
(assert (forall ((q257 Int) (q258 Int) (q259 Bool)) (=> (=> q259 q259) (<= 479 416))))
(declare-const i5 Int)
(assert (forall ((q271 Int) (q272 Int) (q273 Bool)) (=> (distinct (- q271 q272 (- 887) 934) (+ q272 (- 887) (- 887) q272)) (or q273 q273 q273 q273 q273 q273 q273 q273))))
(assert (forall ((q274 Int) (q275 Int) (q276 Int) (q277 Int) (q278 Bool)) (=> (<= q276 (- 668)) (not q278))))
(assert (forall ((q279 Int) (q280 Bool)) (=> (<= q279 669) (and q280 q280 q280 q280 q280 q280))))
(declare-const i6 Int)
(assert (forall ((q283 Int) (q284 Int) (q285 Int) (q286 Bool)) (=> (< (div q283 139) 562 (mod 139 562)) (and q286 q286 q286))))
(assert (forall ((q290 Int) (q291 Int) (q292 Int) (q293 Int) (q294 Bool)) (=> (= q294 q294 q294 q294 q294) (= q291 (div (- q292 905 905 905 q290) 881)))))
(assert (forall ((q295 Int) (q296 Int) (q297 Int) (q298 Int) (q299 Bool)) (=> (>= q297 (abs 410) q298) (and q299 q299 q299 q299 q299))))
(assert (forall ((q300 Int) (q301 Int) (q302 Int) (q303 Int) (q304 Int) (q305 Bool)) (=> (distinct q305 q305 q305 q305 q305) (< (- q301 (abs q300) q303) 340))))
(assert (forall ((q306 Int) (q307 Int) (q308 Int) (q309 Int) (q310 Bool)) (=> (< q306 643) (or q310 q310))))
(assert (forall ((q321 Int) (q322 Int) (q323 Int) (q324 Bool)) (=> (distinct (- 47 q323 228 q321 583) (- q321 (+ q321 583) (- 47 q323 228 q321 583) (- 47 q323 228 q321 583) 47)) (distinct q324 q324 q324 q324 q324 q324 q324))))
(assert (forall ((q325 Int) (q326 Int) (q327 Int) (q328 Int) (q329 Bool)) (=> (= (* q327 798) 377) (or q329 q329 q329))))
(assert (forall ((q336 Int) (q337 Int) (q338 Int) (q339 Int) (q340 Int) (q341 Int) (q342 Bool)) (=> (= q342 q342) (distinct (- (abs q341) q337) 361))))
(declare-const i7 Int)
(assert (forall ((q343 Int) (q344 Int) (q345 Int) (q346 Int) (q347 Int) (q348 Int) (q349 Bool)) (=> (and q349 q349 q349 q349 q349 q349 q349) (distinct (* 34 498 167 q344) (+ q348 q345)))))
(declare-const i8 Int)
(assert (forall ((q350 Int) (q351 Int) (q352 Int) (q353 Int) (q354 Bool)) (=> (= q354 q354 q354) (< (abs q350) 686))))
(assert (forall ((q359 Int) (q360 Int) (q361 Int) (q362 Int) (q363 Int) (q364 Int) (q365 Bool)) (=> (distinct 907 q360) (and q365 q365 q365 q365 q365))))
(assert (forall ((q370 Int) (q371 Int) (q372 Int) (q373 Int) (q374 Int) (q375 Int) (q376 Bool)) (=> (distinct q376 q376 q376 q376 q376 q376) (<= (abs q372) q372 582 (abs q372)))))
(assert (forall ((q385 Int) (q386 Int) (q387 Bool)) (=> (<= 981 35) (= q387 q387 q387 q387 q387 q387 q387 q387 q387))))
(assert (forall ((q388 Int) (q389 Int) (q390 Int) (q391 Int) (q392 Bool)) (=> (=> q392 q392) (>= (+ 362 689 412 811) (- (- 689 q391 517 689) 362 (- 689 q391 517 689)) 689))))
(assert (forall ((q393 Int) (q394 Int) (q395 Int) (q396 Int) (q397 Int) (q398 Bool)) (=> (= q396 q395 679 q397) (=> q398 q398))))
(assert (forall ((q399 Int) (q400 Int) (q401 Int) (q402 Int) (q403 Bool)) (=> (>= q400 q399 q400) (distinct q403 q403 q403 q403 q403 q403 q403 q403))))
(assert (forall ((q404 Int) (q405 Int) (q406 Int) (q407 Int) (q408 Bool)) (=> (and q408 q408 q408) (<= (div (- q404 (+ q405 702 (* 229 702 q406) 702 q407) (* 229 998 998 (* 229 702 q406)) (* 229 998 998 (* 229 702 q406)) 998) 998) q407))))
(assert (forall ((q421 Int) (q422 Int) (q423 Bool)) (=> (not q423) (< (mod q421 675) (mod (mod q421 675) 885)))))
(assert (forall ((q431 Int) (q432 Int) (q433 Int) (q434 Int) (q435 Bool)) (=> (= q435 q435 q435) (> q431 (* (div 36 824) 917) (* (div 36 824) (div 36 824)) (div q433 705)))))
(declare-const i9 Int)
(assert (forall ((q437 Int) (q438 Int) (q439 Bool)) (=> (> q438 323) (distinct q439 q439 q439 q439 q439 q439 q439))))
(assert (forall ((q440 Int) (q441 Int) (q442 Bool)) (=> (< (abs 328) q440) (=> q442 q442))))
(assert (forall ((q443 Int) (q444 Int) (q445 Int) (q446 Int) (q447 Bool)) (=> (>= (abs q445) q443 (abs q445)) (distinct q447 q447 q447 q447 q447 q447))))
(assert (forall ((q448 Int) (q449 Int) (q450 Int) (q451 Int) (q452 Int) (q453 Int) (q454 Bool)) (=> (and q454 q454 q454 q454 q454) (< 149 q449 (abs q451) (abs q451)))))
(assert (forall ((q465 Int) (q466 Bool)) (=> (= 909 654) (= q466 q466 q466 q466 q466))))
(assert (forall ((q473 Int) (q474 Int) (q475 Int) (q476 Int) (q477 Bool)) (=> (>= 866 q473 q475) (not q477))))
(assert (forall ((q481 Int) (q482 Bool)) (=> (= q482 q482 q482) (<= q481 (abs 202) 144 (* 877 50)))))
(declare-const i10 Int)
(assert (forall ((q499 Int) (q500 Int) (q501 Bool)) (=> (and q501 q501 q501 q501 q501 q501) (<= (- 643 (- (+ (- 53) 643 713 q500) 925 q499 (* 534 713 863) (- 53)) q499) 643))))
(assert (forall ((q510 Int) (q511 Int) (q512 Int) (q513 Int) (q514 Int) (q515 Bool)) (=> (= q513 (+ 19 (- q514 q512 778 q510 q510) (* 19 q511) q513) (+ q511 q510 q514 (* 19 q511))) (not q515))))
(declare-const i11 Int)
(check-sat)
(exit)
pruemmer commented
This should be fixed now, I have uploaded an updated version on http://philipp.ruemmer.org/eldarica-bin-nightly.zip