Open
Description
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 -kInduction -setprop solver.solver=PRINCESS -setprop cpa.predicate.encodeBitvectorAs=INTEGER -timelimit 60s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/loop-acceleration/array_2-1.i
--------------------------------------------------------------------------------
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 / kInduction (OpenJDK 64-Bit Server VM 17.0.7) started (CPAchecker.run, INFO)
Parsing CFA from file(s) "../sv-benchmarks/c/loop-acceleration/array_2-1.i" (CPAchecker.parse, INFO)
Using the following resource limits: CPU-time limit of 60s (Parallel analysis 1:ResourceLimitChecker.fromConfiguration, INFO)
Using unsound approximation of ints with unbounded integers and floats with unbounded integers for encoding program semantics. (Parallel analysis 1:PredicateCPA:FormulaManagerView.<init>, WARNING)
Using predicate analysis with Princess 2022-11-03. (Parallel analysis 1:PredicateCPA:PredicateCPA.<init>, INFO)
Using unsound approximation of ints with unbounded integers and floats with unbounded integers for encoding program semantics. (Parallel analysis 1:AssumptionStorageCPA:FormulaManagerView.<init>, WARNING)
Using unsound approximation of ints with unbounded integers and floats with unbounded integers for encoding program semantics. (Parallel analysis 1:InductionStepCase:PredicateCPA:FormulaManagerView.<init>, WARNING)
Using predicate analysis with Princess 2022-11-03. (Parallel analysis 1:InductionStepCase:PredicateCPA:PredicateCPA.<init>, INFO)
Using unsound approximation of ints with unbounded integers and floats with unbounded integers for encoding program semantics. (Parallel analysis 1:InductionStepCase:AssumptionStorageCPA:FormulaManagerView.<init>, WARNING)
Using the following resource limits: CPU-time limit of 60s (Parallel analysis 2:ResourceLimitChecker.fromConfiguration, INFO)
Starting analysis ... (CPAchecker.runAlgorithm, INFO)
Creating formula for program (Parallel analysis 1:AbstractBMCAlgorithm.run, INFO)
Adjusting interestingVariableLimit to 1 (Parallel analysis 2:InvariantsCPA:InvariantsCPA$InterestingVariableLimitAdjuster.adjustConditions, INFO)
Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@5917a039 (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Updating reached set provided to other analyses (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Adjusting interestingVariableLimit to 2 (Parallel analysis 2:InvariantsCPA:InvariantsCPA$InterestingVariableLimitAdjuster.adjustConditions, INFO)
Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@5917a039 (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Updating reached set provided to other analyses (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Adjusting interestingVariableLimit to 3 (Parallel analysis 2:InvariantsCPA:InvariantsCPA$InterestingVariableLimitAdjuster.adjustConditions, INFO)
Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@5917a039 (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Updating reached set provided to other analyses (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Adjusting interestingVariableLimit to 5 (Parallel analysis 2:InvariantsCPA:InvariantsCPA$InterestingVariableLimitAdjuster.adjustConditions, INFO)
Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@5917a039 (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Updating reached set provided to other analyses (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Starting satisfiability check... (Parallel analysis 1:AbstractBMCAlgorithm.boundedModelCheck, INFO)
Adjusting maximum formula depth to 3 (Parallel analysis 2:InvariantsCPA:InvariantsCPA$FormulaDepthAdjuster.adjustConditions, INFO)
Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@5917a039 (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Updating reached set provided to other analyses (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Adjusting abstraction strategy to NEVER (Parallel analysis 2:InvariantsCPA:InvariantsCPA$AbstractionStrategyAdjuster.adjustConditions, INFO)
Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@5917a039 (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Updating reached set provided to other analyses (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Starting assertions check... (Parallel analysis 1:AbstractBMCAlgorithm.checkBoundingAssertions, INFO)
Running algorithm to create induction hypothesis (Parallel analysis 1:KInductionProver.check, INFO)
Starting induction check... (Parallel analysis 1:KInductionProver.check, INFO)
Adjusting maxLoopIterations to 2 (Parallel analysis 1:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState, INFO)
Creating formula for program (Parallel analysis 1:AbstractBMCAlgorithm.run, INFO)
Starting satisfiability check... (Parallel analysis 1:AbstractBMCAlgorithm.boundedModelCheck, INFO)
Starting assertions check... (Parallel analysis 1:AbstractBMCAlgorithm.checkBoundingAssertions, INFO)
Running algorithm to create induction hypothesis (Parallel analysis 1:KInductionProver.check, INFO)
Starting induction check... (Parallel analysis 1:KInductionProver.check, INFO)
Adjusting maxLoopIterations to 3 (Parallel analysis 1:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState, INFO)
Creating formula for program (Parallel analysis 1:AbstractBMCAlgorithm.run, INFO)
Starting satisfiability check... (Parallel analysis 1:AbstractBMCAlgorithm.boundedModelCheck, INFO)
Starting assertions check... (Parallel analysis 1:AbstractBMCAlgorithm.checkBoundingAssertions, INFO)
Running algorithm to create induction hypothesis (Parallel analysis 1:KInductionProver.check, INFO)
Starting induction check... (Parallel analysis 1:KInductionProver.check, INFO)
Adjusting maxLoopIterations to 4 (Parallel analysis 1:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState, INFO)
Creating formula for program (Parallel analysis 1:AbstractBMCAlgorithm.run, INFO)
Starting satisfiability check... (Parallel analysis 1:AbstractBMCAlgorithm.boundedModelCheck, INFO)
Starting assertions check... (Parallel analysis 1:AbstractBMCAlgorithm.checkBoundingAssertions, INFO)
Running algorithm to create induction hypothesis (Parallel analysis 1:KInductionProver.check, INFO)
Starting induction check... (Parallel analysis 1:KInductionProver.check, INFO)
Adjusting maxLoopIterations to 5 (Parallel analysis 1:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState, INFO)
Creating formula for program (Parallel analysis 1:AbstractBMCAlgorithm.run, INFO)
Starting satisfiability check... (Parallel analysis 1:AbstractBMCAlgorithm.boundedModelCheck, INFO)
Starting assertions check... (Parallel analysis 1:AbstractBMCAlgorithm.checkBoundingAssertions, INFO)
Running algorithm to create induction hypothesis (Parallel analysis 1:KInductionProver.check, INFO)
Starting induction check... (Parallel analysis 1:KInductionProver.check, INFO)
Adjusting maxLoopIterations to 6 (Parallel analysis 1:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState, INFO)
Creating formula for program (Parallel analysis 1:AbstractBMCAlgorithm.run, INFO)
Starting satisfiability check... (Parallel analysis 1:AbstractBMCAlgorithm.boundedModelCheck, INFO)
Starting assertions check... (Parallel analysis 1:AbstractBMCAlgorithm.checkBoundingAssertions, INFO)
Running algorithm to create induction hypothesis (Parallel analysis 1:KInductionProver.check, INFO)
Starting induction check... (Parallel analysis 1:KInductionProver.check, INFO)
Analysis was terminated (Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis, INFO)
Exception in thread "main" java.lang.IllegalArgumentException: unhandled model value store(store(store(store(store(store(store(store(store(const(12291), 8191, 12289), 8195, 12289), 12263, 8190), 12267, 8190), 12271, 8190), 12275, 8189), 12279, 8189), 12283, 8189), 12287, 8189) of type class ap.parser.IFunApp
at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.convertValue(PrincessFormulaCreator.java:147)
at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.convertValue(PrincessFormulaCreator.java:72)
at org.sosy_lab.java_smt.solvers.princess.PrincessModel.getAssignments(PrincessModel.java:167)
at org.sosy_lab.java_smt.solvers.princess.PrincessModel.asList(PrincessModel.java:74)
at org.sosy_lab.java_smt.basicimpl.CachingModel.asList(CachingModel.java:38)
at org.sosy_lab.java_smt.api.BasicProverEnvironment.getModelAssignments(BasicProverEnvironment.java:112)
at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper.getModelAssignments(BasicProverWithAssumptionsWrapper.java:89)
at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.getModelAssignments(BasicProverEnvironmentView.java:71)
at org.sosy_lab.cpachecker.core.algorithm.bmc.ProverEnvironmentWithFallback.getModelAssignments(ProverEnvironmentWithFallback.java:213)
at org.sosy_lab.cpachecker.core.algorithm.bmc.KInductionProver.check(KInductionProver.java:487)
at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.checkStepCase(AbstractBMCAlgorithm.java:563)
at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.run(AbstractBMCAlgorithm.java:496)
at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.run(BMCAlgorithm.java:130)
at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.runParallelAnalysis(ParallelAlgorithm.java:397)
at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.lambda$createParallelAnalysis$3(ParallelAlgorithm.java:342)
at com.google.common.util.concurrent.TrustedListenableFutureTask$TrustedFutureInterruptibleTask.runInterruptibly(TrustedListenableFutureTask.java:131)
at com.google.common.util.concurrent.InterruptibleTask.run(InterruptibleTask.java:75)
at com.google.common.util.concurrent.TrustedListenableFutureTask.run(TrustedListenableFutureTask.java:82)
at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
at java.base/java.lang.Thread.run(Thread.java:833)