search

uuverifiers / eldarica

The Eldarica model checker
Other
80 stars 22 forks source link

AssertionError at Predef.scala:156 (IdealInt.scala:654) #16

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following instance, 654.txt

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

 Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.basetypes.IdealInt.$up(IdealInt.scala:654)
        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.ReduceWithConjunction.ap$terfor$conjunctions$ReduceWithConjunction$$reduceWithPlugin(ReduceWithConjunction.scala:621)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:91)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:165)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:174)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:173)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.Iterator$class.foreach(Iterator.scala:891)
        at scala.collection.AbstractIterator.foreach(Iterator.scala:1334)
        at scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
        at ap.terfor.conjunctions.NegatedConjunctions.foreach(NegatedConjunctions.scala:72)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
        at ap.terfor.conjunctions.NegatedConjunctions.map(NegatedConjunctions.scala:72)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceNegatedConjs(ReduceWithConjunction.scala:173)
...

Option

'-assert', '-noSlicing', '-abstract:term'
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