search

uuverifiers / eldarica

The Eldarica model checker
Other
80 stars 23 forks source link

NoSuchElementException: key not found: sc_2_0_0 #5

Closed cocreature closed 8 years ago

cocreature commented 8 years ago

When I run eldarica without any special options (using commit dcb9b058b85b2c3c5da63d411ff6de736aebaeee) on this example, I get the following exception

Warning: ignoring get-model
Theories: SimpleArray(1)

Initially:                11 clauses
After inlining:           11 clauses
After shortening clauses: 12 clauses

Constant and interval propagation ++++++++++++++++
Unique satisfiable clauses: 12
Starting CEGAR
.
Found counterexample #1, refining ... (2and/0or)  80 -> 79 ... adding predicates:
INV_MAIN_0: !(INV_MAIN_0_13_0 = INV_MAIN_0_4_0) | INV_MAIN_0_14_0 = INV_MAIN_0_5_0

Found counterexample #2, refining ... (2and/0or)  35 -> 34 ... adding predicates:
INV_MAIN_0: !(INV_MAIN_0_13_0 + -1*INV_MAIN_0_11_0 - 4*INV_MAIN_0_10_0 = 0) | !(4*INV_MAIN_0_12_0 + INV_MAIN_0_11_0 - INV_MAIN_0_4_0 = 0) | INV_MAIN_0_14_0 = INV_MAIN_0_5_0

Found counterexample #3, refining ... (2and/0or)  36 -> 35 ... adding predicates:
INV_MAIN_0: !(INV_MAIN_0_11_0 + 4*INV_MAIN_0_10_0 - INV_MAIN_0_4_0 = 0) | INV_MAIN_0_6_0 = INV_MAIN_0_5_0
.
Found counterexample #4, refining ... (2and/0or)  52 -> 51 ... adding predicates:
INV_MAIN_0: !(4*INV_MAIN_0_12_0 + INV_MAIN_0_3_0 - 4*INV_MAIN_0_10_0 - INV_MAIN_0_11_0 = 0), INV_MAIN_0_13_0 + -4*INV_MAIN_0_12_0 - INV_MAIN_0_3_0 = 0

Found counterexample #5, refining ... (3and/0or)  66 -> 65 ... adding predicates:
INV_MAIN_0: INV_MAIN_0_14_0 = INV_MAIN_0_6_0 & INV_MAIN_0_13_0 + -4*INV_MAIN_0_12_0 - INV_MAIN_0_3_0 = 0 & INV_MAIN_0_11_0 = INV_MAIN_0_3_0, !(INV_MAIN_0_13_0 + -4*INV_MAIN_0_10_0 - INV_MAIN_0_3_0 = 0) | !(4*INV_MAIN_0_12_0 + INV_MAIN_0_3_0 - INV_MAIN_0_4_0 = 0) | INV_MAIN_0_6_0 = INV_MAIN_0_5_0
..
Found counterexample #6, refining ... (2and/0or)  60 -> 59 ... adding predicates:
INV_MAIN_0: !(INV_MAIN_0_13_0 = INV_MAIN_0_4_0) | (INV_MAIN_0_11_0 + 4*INV_MAIN_0_10_0 - INV_MAIN_0_4_0 = 0 & INV_MAIN_0_6_0 = INV_MAIN_0_5_0)
..
Found counterexample #7, refining ... (4and/0or)  267 -> 160 ... adding predicates:
INV_MAIN_0_INV_MAIN_0_INV_MAIN_0: !(INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_13_0 = INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_4_0) | INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_14_0 = INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_5_0
.
Found counterexample #8, refining ... (4and/0or) . 420 -> 319 ... adding predicates:
INV_MAIN_0: INV_MAIN_0_11_0 + 4*INV_MAIN_0_7_0 + -1*INV_MAIN_0_3_0 - 4*INV_MAIN_0_0_0 = 0 & INV_MAIN_0_9_0 = INV_MAIN_0_2_0, !(INV_MAIN_0_13_0 = INV_MAIN_0_4_0)
INV_MAIN_0_INV_MAIN_0_INV_MAIN_0: INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_11_0 + 4*INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_7_0 + -1*INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_3_0 - 4*INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_0_0 = 0 & INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_9_0 = INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_2_0, !(INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_43_0 = INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_34_0) | INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_44_0 = INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_35_0
..
Found counterexample #9, refining ... (4and/0or)  205 -> 155java.util.NoSuchElementException: key not found: sc_2_0_0
    at scala.collection.MapLike$class.default(MapLike.scala:228)
    at scala.collection.AbstractMap.default(Map.scala:59)
    at scala.collection.MapLike$class.apply(MapLike.scala:141)
    at scala.collection.AbstractMap.apply(Map.scala:59)
    at ap.util.FastImmutableMap.apply(FastImmutableMap.scala:51)
    at ap.terfor.TermOrder.compareTerms(TermOrder.scala:254)
    at ap.terfor.TermOrder.compare(TermOrder.scala:239)
    at ap.terfor.linearcombination.LinearCombination1.$minus(LinearCombination.scala:1362)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:658)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:546)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:478)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:478)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:478)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:546)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:478)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:515)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:515)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:515)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:515)
    at ap.interpolants.Interpolator$.ap$interpolants$Interpolator$$applyHelp(Interpolator.scala:394)
    at ap.interpolants.Interpolator$.apply(Interpolator.scala:62)
    at lazabs.horn.bottomup.TreeInterpolator$.lazabs$horn$bottomup$TreeInterpolator$$computeInts$1(TreeInterpolator.scala:146)
    at lazabs.horn.bottomup.TreeInterpolator$$anonfun$lazabs$horn$bottomup$TreeInterpolator$$computeInts$1$3.apply(TreeInterpolator.scala:157)
    at lazabs.horn.bottomup.TreeInterpolator$$anonfun$lazabs$horn$bottomup$TreeInterpolator$$computeInts$1$3.apply(TreeInterpolator.scala:156)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:683)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:682)
    at lazabs.horn.bottomup.TreeInterpolator$.lazabs$horn$bottomup$TreeInterpolator$$computeInts$1(TreeInterpolator.scala:156)
    at lazabs.horn.bottomup.TreeInterpolator$.treeInterpolate(TreeInterpolator.scala:178)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.apply(DisjInterpolator.scala:607)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.apply(DisjInterpolator.scala:194)
    at ap.SimpleAPI$.withProver(SimpleAPI.scala:142)
    at lazabs.horn.bottomup.DisjInterpolator$.lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp(DisjInterpolator.scala:194)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$predicateGenerator$1.apply$mcV$sp(DisjInterpolator.scala:138)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$predicateGenerator$1.apply(DisjInterpolator.scala:138)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$predicateGenerator$1.apply(DisjInterpolator.scala:138)
    at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
    at ap.util.Timeout$.withChecker(Timeout.scala:44)
    at ap.util.Timeout$$anonfun$withTimeoutMillis$1.apply(Timeout.scala:58)
    at ap.util.Timeout$.catchTimeout(Timeout.scala:88)
    at ap.util.Timeout$.withTimeoutMillis(Timeout.scala:61)
    at lazabs.horn.bottomup.DisjInterpolator$.predicateGenerator(DisjInterpolator.scala:155)
    at lazabs.horn.bottomup.DagInterpolator$.interpolatingPredicateGenCEXAndOr(DagInterpolator.scala:156)
    at lazabs.horn.bottomup.HornWrapper$$anonfun$10$$anonfun$apply$5.apply(HornWrapper.scala:166)
    at lazabs.horn.bottomup.HornWrapper$$anonfun$10$$anonfun$apply$5.apply(HornWrapper.scala:166)
    at lazabs.horn.bottomup.HornPredAbs.liftedTree1$1(HornPredAbs.scala:932)
    at lazabs.horn.bottomup.HornPredAbs.<init>(HornPredAbs.scala:909)
    at lazabs.horn.bottomup.HornWrapper$$anonfun$12.apply(HornWrapper.scala:218)
    at lazabs.horn.bottomup.HornWrapper$$anonfun$12.apply(HornWrapper.scala:218)
    at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
    at scala.Console$.withOut(Console.scala:65)
    at lazabs.horn.bottomup.HornWrapper.<init>(HornWrapper.scala:217)
    at lazabs.horn.Solve$.apply(Solve.scala:81)
    at lazabs.Main$$anonfun$doMain$3.apply$mcV$sp(Main.scala:421)
    at lazabs.Main$$anonfun$doMain$3.apply(Main.scala:421)
    at lazabs.Main$$anonfun$doMain$3.apply(Main.scala:421)
    at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
    at scala.Console$.withErr(Console.scala:80)
    at lazabs.Main$.doMain(Main.scala:420)
    at lazabs.Main$.main(Main.scala:143)
    at lazabs.Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
    at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
    at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
    at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
    at scala.tools.nsc.ObjectRunner$.run(ObjectRunner.scala:39)
    at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
    at scala.tools.nsc.ObjectRunner$.runAndCatch(ObjectRunner.scala:39)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:65)
    at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

The example is minified so I don’t actually know what the correct answer would be but throwing an exception is probably not it :)

I wasn’t able to minify it further, in particular the conditions in IN_INV seem to be important.

pruemmer commented 8 years ago

Thanks for the bug report. I can reproduce the problem on my machine, but am not sure yet what causes the problem ... will look into that next week. Philipp

pruemmer commented 8 years ago

This was indeed a bug in the interpolation code in Princess; should be fixed now! Philipp

cocreature commented 8 years ago

Thanks!