search

uuverifiers / eldarica

The Eldarica model checker
Other
80 stars 23 forks source link

AssertionError at Predef.scala:156 (IdealInt.scala:664) #17

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following instance, 664.txt

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

 Exception in thread "main" java.lang.AssertionError: assertion failed                                                                                                                            [121/1865]
        at scala.Predef$.assert(Predef.scala:156)
        at ap.basetypes.IdealInt.getHighestSetBit(IdealInt.scala:664)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1$$anonfun$2.apply(ModReducer.scala:320)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1$$anonfun$2.apply(ModReducer.scala:316)
        at ap.util.LRUCache.apply(LRUCache.scala:37)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1.apply(ModReducer.scala:315)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1.apply(ModReducer.scala:185)
        at ap.terfor.conjunctions.ReducerPlugin$.rewritePreds(ReducerPlugin.scala:89)
        at ap.theories.bitvectors.ModReducer$Reducer.reduce(ModReducer.scala:185)
        at ap.terfor.conjunctions.SeqReducerPlugin.reduce(ReducerPlugin.scala:371)
        at ap.terfor.conjunctions.ReduceWithConjunction.ap$terfor$conjunctions$ReduceWithConjunction$$reduceWithPlugin(ReduceWithConjunction.scala:621)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:91)
...

Options

'-assert', '-noSlicing', '-abstract:relIneqs'
pruemmer commented 4 years ago

After the most recent changes, this exception does not occur any more. I have uploaded an updated version on http://philipp.ruemmer.org/eldarica-bin-nightly.zip