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.

Sign up for GitHub

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

Jump to bottom

Princess: missing arithmetic atom in interpolation (found in CPAchecker benchmark) #306

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

Princess: missing arithmetic atom in interpolation (found in CPAchecker benchmark) #306

kfriedberger opened this issue Jun 4, 2023 · 1 comment
Labels
bug Princess

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 -predicateAnalysis -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/loop-acceleration/diamond_2-2.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 / predicateAnalysis (OpenJDK 64-Bit Server VM 17.0.7) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "../sv-benchmarks/c/loop-acceleration/diamond_2-2.c" (CPAchecker.parse, INFO)

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

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

Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (PredicateCPA:PredicateCPARefiner.<init>, INFO)

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

Exception in thread "main" java.lang.Error: The arithmetic atom (main::x@5 >= 0) was not found
	at ap.interpolants.InterpolationContext.getPartialInterpolant(InterpolationContext.scala:200)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:598)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:940)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:1015)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:940)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:1015)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:940)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:1015)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:940)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:1015)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:898)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:940)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:1015)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:940)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:1015)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:940)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:1015)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:588)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.$anonfun$applyHelp$3(Interpolator.scala:384)
	at ap.interpolants.Interpolator$.$anonfun$applyHelp$3$adapted(Interpolator.scala:378)
	at scala.collection.Iterator$$anon$9.next(Iterator.scala:584)
	at scala.collection.Iterator$ConcatIterator.next(Iterator.scala:1194)
	at scala.collection.IterableOnceOps.foldLeft(IterableOnce.scala:675)
	at scala.collection.IterableOnceOps.foldLeft$(IterableOnce.scala:669)
	at scala.collection.AbstractIterator.foldLeft(Iterator.scala:1300)
	at scala.collection.IterableOnceOps.$div$colon(IterableOnce.scala:697)
	at scala.collection.IterableOnceOps.$div$colon$(IterableOnce.scala:697)
	at scala.collection.AbstractIterator.$div$colon(Iterator.scala:1300)
	at ap.terfor.conjunctions.LazyConjunction$.conj(LazyConjunction.scala:56)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:397)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:656)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:646)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:670)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:646)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:588)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:588)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:776)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:588)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:241)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:646)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:646)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:646)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:646)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:646)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:588)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:776)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:588)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:776)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:588)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.apply(Interpolator.scala:76)
	at ap.api.SimpleAPI.$anonfun$getInterpolants$20(SimpleAPI.scala:2447)
	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:59)
	at ap.util.Timeout$.withChecker(Timeout.scala:56)
	at ap.util.Timeout$.$anonfun$withTimeoutMillis$2(Timeout.scala:71)
	at ap.util.Timeout$.catchTimeout(Timeout.scala:100)
	at ap.util.Timeout$.withTimeoutMillis(Timeout.scala:73)
	at ap.api.SimpleAPI.$anonfun$getInterpolants$13(SimpleAPI.scala:2449)
	at ap.api.SimpleAPI.$anonfun$getInterpolants$13$adapted(SimpleAPI.scala:2435)
	at scala.collection.immutable.Range.map(Range.scala:59)
	at ap.api.SimpleAPI.$anonfun$getInterpolants$12(SimpleAPI.scala:2435)
	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:59)
	at ap.util.Debug$.withDisabledAssertions(Debug.scala:159)
	at ap.api.SimpleAPI.getInterpolants(SimpleAPI.scala:2435)
	at org.sosy_lab.java_smt.solvers.princess.PrincessInterpolatingProver.getSeqInterpolants(PrincessInterpolatingProver.java:122)
	at org.sosy_lab.java_smt.solvers.princess.PrincessInterpolatingProver.getInterpolant(PrincessInterpolatingProver.java:100)
	at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper.getInterpolant(InterpolatingProverWithAssumptionsWrapper.java:46)
	at org.sosy_lab.cpachecker.util.predicates.smt.InterpolatingProverEnvironmentView.getInterpolant(InterpolatingProverEnvironmentView.java:32)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.strategy.ITPStrategy.getInterpolantFromSublist(ITPStrategy.java:166)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.strategy.SequentialInterpolation.getFwdInterpolants(SequentialInterpolation.java:157)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.strategy.SequentialInterpolation.getInterpolants(SequentialInterpolation.java:110)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.getInterpolants(InterpolationManager.java:763)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager$Interpolator.buildCounterexampleTrace(InterpolationManager.java:976)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTrace0(InterpolationManager.java:429)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.lambda$buildCounterexampleTrace$0(InterpolationManager.java:328)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.callWithTimelimit(InterpolationManager.java:337)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTrace(InterpolationManager.java:327)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performInterpolatingRefinement(PredicateCPARefiner.java:400)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.checkCounterexample(PredicateCPARefiner.java:390)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performRefinementForPath(PredicateCPARefiner.java:281)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateStaticRefiner.performRefinementForPath(PredicateStaticRefiner.java:183)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinementForPath(AbstractARGBasedRefiner.java:158)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinement(AbstractARGBasedRefiner.java:104)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.refine(CEGARAlgorithm.java:310)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:256)
	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)
@kfriedberger kfriedberger changed the title Princess: missing aithmetic atom in interpolation (found in CPAchecker benchmark) Princess: missing arithmetic atom in interpolation (found in CPAchecker benchmark) Jun 4, 2023
@kfriedberger
Copy link
Member Author

Same here:
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 -predicateAnalysis -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/loop-crafted/simple_array_index_value_4.i.v+lhb-reducer.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 / predicateAnalysis (OpenJDK 64-Bit Server VM 17.0.7) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "../sv-benchmarks/c/loop-crafted/simple_array_index_value_4.i.v+lhb-reducer.c" (CPAchecker.parse, INFO)

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

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

Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (PredicateCPA:PredicateCPARefiner.<init>, INFO)

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

Exception in thread "main" java.lang.Error: The arithmetic atom (__VERIFIER_nondet_uint!2@ >= 0) was not found
	at ap.interpolants.InterpolationContext.getPartialInterpolant(InterpolationContext.scala:200)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:599)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:656)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:646)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:697)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:646)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:646)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:588)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:776)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:588)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:588)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:776)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:227)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:940)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:1015)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:898)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:646)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:251)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:571)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:940)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:1015)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:977)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:625)
	at ap.interpolants.Interpolator$.applyHelp(Interpolator.scala:502)
	at ap.interpolants.Interpolator$.apply(Interpolator.scala:76)
	at ap.api.SimpleAPI.$anonfun$getInterpolants$20(SimpleAPI.scala:2447)
	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:59)
	at ap.util.Timeout$.withChecker(Timeout.scala:56)
	at ap.util.Timeout$.$anonfun$withTimeoutMillis$2(Timeout.scala:71)
	at ap.util.Timeout$.catchTimeout(Timeout.scala:100)
	at ap.util.Timeout$.withTimeoutMillis(Timeout.scala:73)
	at ap.api.SimpleAPI.$anonfun$getInterpolants$13(SimpleAPI.scala:2449)
	at ap.api.SimpleAPI.$anonfun$getInterpolants$13$adapted(SimpleAPI.scala:2435)
	at scala.collection.immutable.Range.map(Range.scala:59)
	at ap.api.SimpleAPI.$anonfun$getInterpolants$12(SimpleAPI.scala:2435)
	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:59)
	at ap.util.Debug$.withDisabledAssertions(Debug.scala:159)
	at ap.api.SimpleAPI.getInterpolants(SimpleAPI.scala:2435)
	at org.sosy_lab.java_smt.solvers.princess.PrincessInterpolatingProver.getSeqInterpolants(PrincessInterpolatingProver.java:122)
	at org.sosy_lab.java_smt.solvers.princess.PrincessInterpolatingProver.getInterpolant(PrincessInterpolatingProver.java:100)
	at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper.getInterpolant(InterpolatingProverWithAssumptionsWrapper.java:46)
	at org.sosy_lab.cpachecker.util.predicates.smt.InterpolatingProverEnvironmentView.getInterpolant(InterpolatingProverEnvironmentView.java:32)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.strategy.ITPStrategy.getInterpolantFromSublist(ITPStrategy.java:166)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.strategy.SequentialInterpolation.getFwdInterpolants(SequentialInterpolation.java:157)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.strategy.SequentialInterpolation.getInterpolants(SequentialInterpolation.java:110)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.getInterpolants(InterpolationManager.java:763)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager$Interpolator.buildCounterexampleTrace(InterpolationManager.java:976)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTrace0(InterpolationManager.java:429)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.lambda$buildCounterexampleTrace$0(InterpolationManager.java:328)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.callWithTimelimit(InterpolationManager.java:337)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTrace(InterpolationManager.java:327)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performInterpolatingRefinement(PredicateCPARefiner.java:400)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.checkCounterexample(PredicateCPARefiner.java:390)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performRefinementForPath(PredicateCPARefiner.java:281)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateStaticRefiner.performRefinementForPath(PredicateStaticRefiner.java:183)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinementForPath(AbstractARGBasedRefiner.java:158)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinement(AbstractARGBasedRefiner.java:104)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.refine(CEGARAlgorithm.java:310)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:256)
	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)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Princess
Milestone
No milestone
Development

No branches or pull requests
1 participant
@kfriedberger