uuverifiers/eldarica

AssertionError at Predef.scala:156 (HornWrapper.scala:73)

Closed this issue · 2 comments

rainoftime commented

Hi, for the following instance,

(set-logic HORN)
(assert (forall ((q0 (_ BitVec 9)) (q1 (_ BitVec 12))) (=> (distinct q0 q0) (bvslt (bvsmod q1 q1) q1))))
(assert (forall ((q3 (_ BitVec 9)) (q4 (_ BitVec 9)) (q5 (_ BitVec 8))) (=> (bvule q4 (bvnor q3 q3)) (distinct (bvlshr (bvsdiv q5 q5) (bvsdiv q5 q5)) (bvsdiv q5 q5)))))
(check-sat)

eldarica 31d9075

Theories: GroebnerMultiplication, ModuloArithmetic
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at lazabs.horn.bottomup.HornWrapper$.verifySolution(HornWrapper.scala:73)
        at lazabs.horn.bottomup.InnerHornWrapper.<init>(HornWrapper.scala:433)
        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)
rainoftime commented

Related: #22

pruemmer commented