kfriedberger
commented
1 year ago 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)
LOG: