Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
kfriedberger opened this issue Jun 4, 2023 · 1 comment

Comments

@kfriedberger
Copy link
Member

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)
@daniel-raffler
Copy link
Contributor

I've seen this issue somewhat frequently and now reported it here

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Development

No branches or pull requests

2 participants