Princess: match error in model evaluation (found in CPAchecker benchmark)

[kfriedberger]

LOG:

scripts/cpa.sh -heap 13000M -noout -benchmark -stack 50M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop counterexample.export.allowImpreciseCounterexamples=true -setprop cpa.predicate.encodeFloatAs=INTEGER -bmc -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=INTEGER -setprop cpa.loopbound.maxLoopIterations=10 -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/nla-digbench-scaling/freire1_valuebound1.c


--------------------------------------------------------------------------------


Running CPAchecker with Java heap of size 13000M.
Running CPAchecker with Java stack of size 50M.
Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)

Using the following resource limits: CPU-time limit of 60s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 2.2.1-svn-43814M / bmc (OpenJDK 64-Bit Server VM 17.0.7) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "../sv-benchmarks/c/nla-digbench-scaling/freire1_valuebound1.c" (CPAchecker.parse, INFO)

Using unsound approximation of ints with unbounded integers and floats with unbounded integers for encoding program semantics. (PredicateCPA:FormulaManagerView.<init>, WARNING)

Using predicate analysis with Princess 2022-11-03. (PredicateCPA:PredicateCPA.<init>, INFO)

Using unsound approximation of ints with unbounded integers and floats with unbounded integers for encoding program semantics. (AssumptionStorageCPA:FormulaManagerView.<init>, WARNING)

Starting analysis ... (CPAchecker.runAlgorithm, INFO)

Creating formula for program (AbstractBMCAlgorithm.run, INFO)

Starting satisfiability check... (AbstractBMCAlgorithm.boundedModelCheck, INFO)

Error found, creating error path (AbstractBMCAlgorithm.analyzeCounterexample0, INFO)

Exception in thread "main" scala.MatchError: _0 (of class ap.parser.ISortedVariable)
	at ap.api.PartialModel$Evaluator$.postVisit(PartialModel.scala:134)
	at ap.api.PartialModel$Evaluator$.postVisit(PartialModel.scala:114)
	at ap.parser.CollectingVisitor.visit(InputAbsyVisitor.scala:169)
	at ap.api.PartialModel$Evaluator$.apply(PartialModel.scala:116)
	at ap.api.PartialModel.evalExpression(PartialModel.scala:59)
	at org.sosy_lab.java_smt.solvers.princess.PrincessModel.evaluate(PrincessModel.java:251)
	at org.sosy_lab.java_smt.solvers.princess.PrincessModel.evalImpl(PrincessModel.java:237)
	at org.sosy_lab.java_smt.solvers.princess.PrincessModel.evalImpl(PrincessModel.java:42)
	at org.sosy_lab.java_smt.basicimpl.AbstractEvaluator.evaluateImpl(AbstractEvaluator.java:119)
	at org.sosy_lab.java_smt.basicimpl.AbstractEvaluator.evaluate(AbstractEvaluator.java:101)
	at org.sosy_lab.java_smt.basicimpl.CachingModel.evaluate(CachingModel.java:55)
	at org.sosy_lab.cpachecker.util.predicates.smt.ModelView.evaluateImpl(ModelView.java:48)
	at org.sosy_lab.cpachecker.util.predicates.smt.ModelView.evaluate(ModelView.java:72)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.PathFormulaManagerImpl.lambda$getARGPathFromModel$0(PathFormulaManagerImpl.java:469)
	at org.sosy_lab.cpachecker.cpa.arg.ARGUtils.getPathFromBranchingInformation(ARGUtils.java:504)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.PathFormulaManagerImpl.getARGPathFromModel(PathFormulaManagerImpl.java:446)
	at org.sosy_lab.cpachecker.util.predicates.pathformula.PathFormulaManager.getARGPathFromModel(PathFormulaManager.java:143)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.analyzeCounterexample0(AbstractBMCAlgorithm.java:878)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.analyzeCounterexample(BMCAlgorithm.java:168)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.boundedModelCheck(AbstractBMCAlgorithm.java:720)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.boundedModelCheck(AbstractBMCAlgorithm.java:686)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.boundedModelCheck(BMCAlgorithm.java:158)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.run(AbstractBMCAlgorithm.java:454)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.run(BMCAlgorithm.java:130)
	at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:507)
	at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:369)
	at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:169)