search

uuverifiers / eldarica

The Eldarica model checker
Other
80 stars 22 forks source link

AssertionError at Predef.scala:156 (HornWrapper.scala:91) #19

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_14-0 (_ BitVec 14))
(assert (forall ((q0 (_ BitVec 12)) (q1 (_ BitVec 12)) (q2 (_ BitVec 12)) (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 12)) (q17 (_ BitVec 12)) (q18 (_ BitVec 12)) (q19 (_ BitVec 12)) (q20 (_ BitVec 12)) (q21 (_ BitVec 14))) (=> (distinct q16 q2) (bvsgt (bvsrem (bvudiv q21 q21) (bvashr q21 q21)) (bvashr q21 q21)))))
(assert (forall ((q22 (_ BitVec 12)) (q23 (_ BitVec 12)) (q24 (_ BitVec 12)) (q25 (_ BitVec 12)) (q26 (_ BitVec 12)) (q27 Bool)) (=> (distinct (bvsub q23 q24) q26) (=> q27 q27))))
(assert (forall ((q28 (_ BitVec 12)) (q29 (_ BitVec 12)) (q30 (_ BitVec 12)) (q31 (_ BitVec 12)) (q32 (_ BitVec 12)) (q33 (_ BitVec 12)) (q34 Bool)) (=> (xor q34 q34 q34 q34 q34 q34) (= q30 (bvashr q33 q29)))))
(assert (forall ((q35 (_ BitVec 12)) (q36 (_ BitVec 12)) (q37 (_ BitVec 12)) (q38 (_ BitVec 12)) (q39 (_ BitVec 12)) (q40 (_ BitVec 12)) (q41 (_ BitVec 12)) (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 9))) (=> (distinct (bvlshr q51 q44) q35) (= (bvsub (bvnot q53) (bvnot q53)) q53))))
(assert (forall ((q54 (_ BitVec 12)) (q55 (_ BitVec 12)) (q56 (_ BitVec 12)) (q57 (_ BitVec 12)) (q58 (_ BitVec 12)) (q59 (_ BitVec 9))) (=> (= q54 q54) (bvult (bvsub (bvshl q59 (bvnot q59)) (bvnot q59)) (bvsub (bvshl q59 (bvnot q59)) (bvnot q59))))))
(assert (forall ((q64 (_ BitVec 12)) (q65 (_ BitVec 12)) (q66 (_ BitVec 8))) (=> (distinct (bvashr q66 q66) q66) (= (bvneg q65) (bvashr q65 (bvneg q65))))))
(assert (forall ((q67 (_ BitVec 12)) (q68 (_ BitVec 12)) (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 (_ BitVec 12)) (q83 (_ BitVec 12)) (q84 (_ BitVec 12)) (q85 (_ BitVec 12)) (q86 (_ BitVec 12)) (q87 (_ BitVec 12)) (q88 (_ BitVec 14))) (=> (= (bvsmod q88 q88) (bvsmod q88 q88)) (distinct q73 q69))))
(assert (forall ((q107 (_ BitVec 12)) (q108 (_ BitVec 12)) (q109 (_ BitVec 12)) (q110 (_ BitVec 12)) (q111 (_ BitVec 12)) (q112 (_ BitVec 8))) (=> (= q112 (bvlshr q112 q112)) (= q108 q109))))
(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 12)) (q133 (_ BitVec 11))) (=> (distinct (bvnor q133 q133) (bvurem (bvnor q133 q133) q133)) (distinct q127 q125))))
(assert (forall ((q134 (_ BitVec 12)) (q135 (_ BitVec 12)) (q136 (_ BitVec 12)) (q137 (_ BitVec 8))) (=> (bvsle (bvnot q135) q136) (bvule (bvsdiv (bvnor q137 q137) q137) (bvashr (bvsdiv (bvnor q137 q137) q137) (bvsmod (bvnor q137 q137) q137))))))
(check-sat)

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

 Exception in thread "main" java.lang.AssertionError: assertion failed                                                                                                                              [6/1977]
        at scala.Predef$.assert(Predef.scala:156)
        at lazabs.horn.bottomup.HornWrapper$.verifyCEX(HornWrapper.scala:91)
        at lazabs.horn.bottomup.InnerHornWrapper.<init>(HornWrapper.scala:390)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$9.apply(HornWrapper.scala:228)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$9.apply(HornWrapper.scala:230)
        at lazabs.ParallelComputation$.apply(ParallelComputation.scala:46)
        at lazabs.horn.bottomup.HornWrapper.<init>(HornWrapper.scala:227)
        at lazabs.horn.Solve$.apply(Solve.scala:81)
        at lazabs.Main$.doMain(Main.scala:586)
        at lazabs.Main$.main(Main.scala:267)
        at lazabs.Main.main(Main.scala)
'-assert', '-abstract:relEqs'
pruemmer commented 4 years ago

This should be fixed in the latest version 2.0.4. Thanks for the bug reports, they are very useful!