scripts/cpa.sh -sv-comp15 -disable-java-assertions -heap 10000m -timelimit 900s -stats -spec ../benchmarks/c/loops/ALL.prp ../benchmarks/c/loops/for_bounded_loop1_false-unreach-call_true-termination.i
--------------------------------------------------------------------------------
Running CPAchecker with Java heap of size 10000m.
Running CPAchecker with the following extra VM options: -Djava.io.tmpdir=/tmp/vcloud-vcloud-master/worker/tmp_-1258651731_tempdir
Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO)
CPAchecker 1.3.10-svcomp15 (OpenJDK 64-Bit Server VM 1.7.0_85) started (CPAchecker.run, INFO)
Using Restarting Algorithm (CoreComponentsFactory.createAlgorithm, INFO)
The following configuration options were specified but are not used:
cpa.predicate.useFloatingPointArithmetic
cpa.callstack.skipVoidRecursion
cpa.arg.errorPath.file
cpa.callstack.skipFunctionPointerRecursion
cpa.arg.errorPath.graphml
(CPAchecker.printConfigurationWarnings, WARNING)
Starting analysis ... (CPAchecker.runAlgorithm, INFO)
Using the following resource limits: CPU-time limit of 60s (Analysis1:ResourceLimitChecker.fromConfiguration, INFO)
Error path found, starting counterexample check with CPACHECKER. (Analysis1:CounterexampleCheckAlgorithm.checkCounterexample, INFO)
Using the following resource limits: CPU-time limit of 900s (Analysis1:CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO)
Using predicate analysis with MathSAT5 version 5.2.12 (6de13e7f4050) (Jun 5 2014 09:12:40, gmp 5.0.5, gcc 4.6.3, 64-bit) and JFactory 1.21. (Analysis1:CounterexampleCheck:PredicateCPA:PredicateCPA., INFO)
Error path found, but identified as infeasible by counterexample check with CPACHECKER. (Analysis1:CounterexampleCheckAlgorithm.checkCounterexample, INFO)
Warning: Analysis not completed (Refinement failed: External tool verified counterexample as infeasible) (CounterexampleCheckAlgorithm.checkCounterexample, WARNING)
Statistics for algorithm 1 of 6
===============================
Total time for algorithm 1: 0.268s
ValueAnalysisCPA statistics
---------------------------
Number of variables: 80 (count: 31, min: 0, max: 4, avg: 2.58)
Number of global variables: 0 (count: 31, min: 0, max: 0, avg: 0.00)
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.003s
Automaton transfers with branching: 0
Automaton transfer successors: 42 (count: 42, min: 1, max: 1, avg: 1.00) [1 x 42]
CPA algorithm statistics
------------------------
Number of iterations: 27
Max size of waitlist: 4
Average size of waitlist: 2
Number of computed successors: 30
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 0
Number of times breaked: 1
Total time for CPA algorithm: 0.017s (Max: 0.017s)
Time for choose from waitlist: 0.000s
Time for precision adjustment: 0.001s
Time for transfer relation: 0.013s
Time for stop operator: 0.001s
Time for adding to reached set: 0.001s
Counterexample-Check Algorithm statistics
-----------------------------------------
Number of counterexample checks: 1
Number of infeasible paths: 1 (100%)
Time for counterexample checks: 0.118s
RestartAlgorithm switches to the next configuration... (RestartAlgorithm.run, INFO)
Using the following resource limits: CPU-time limit of 60s (Analysis2:ResourceLimitChecker.fromConfiguration, INFO)
Error path found, starting counterexample check with CPACHECKER. (Analysis2:CounterexampleCheckAlgorithm.checkCounterexample, INFO)
Using the following resource limits: CPU-time limit of 900s (Analysis2:CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO)
Using predicate analysis with MathSAT5 version 5.2.12 (6de13e7f4050) (Jun 5 2014 09:12:40, gmp 5.0.5, gcc 4.6.3, 64-bit) and JFactory 1.21. (Analysis2:CounterexampleCheck:PredicateCPA:PredicateCPA., INFO)
Error path found, but identified as infeasible by counterexample check with CPACHECKER. (Analysis2:CounterexampleCheckAlgorithm.checkCounterexample, INFO)
Warning: Analysis not completed (Refinement failed: External tool verified counterexample as infeasible) (CounterexampleCheckAlgorithm.checkCounterexample, WARNING)
Statistics for algorithm 2 of 6
===============================
Total time for algorithm 2: 0.139s
ValueAnalysisCPA statistics
---------------------------
Number of variables: 49 (count: 31, min: 0, max: 3, avg: 1.58)
Number of global variables: 0 (count: 31, min: 0, max: 0, avg: 0.00)
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.000s
Automaton transfers with branching: 0
Automaton transfer successors: 99 (count: 99, min: 1, max: 1, avg: 1.00) [1 x 99]
ComponentAwarePrecisionAdjustment Statistics statistics
-------------------------------------------------------
Total time for precision adjustment: 0.001s
Total time for composite: 0.000s
Total time for abstraction computation: 0.000s
Total time for path threshold: 0.000s
Number of abstraction computations: 63
CPA algorithm statistics
------------------------
Number of iterations: 55
Max size of waitlist: 4
Average size of waitlist: 2
Number of computed successors: 63
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 0
Number of times breaked: 3
Total time for CPA algorithm: 0.013s (Max: 0.006s)
Time for choose from waitlist: 0.000s
Time for precision adjustment: 0.001s
Time for transfer relation: 0.008s
Time for stop operator: 0.001s
Time for adding to reached set: 0.003s
ValueAnalysisDelegatingRefiner statistics
-----------------------------------------
number of value analysis refinements: 2
number of successful valueAnalysis refinements: 2
number of predicate refinements: 0
ValueAnalysisInterpolationBasedRefiner statistics
-------------------------------------------------
Number of interpolations: 2
Number of interpolation queries: 24 (count: 23, min: 0, max: 5, avg: 1.04)
Size of interpolant: 21 (count: 23, min: 0, max: 2, avg: 0.91)
Time for interpolation: 0.009s
CEGAR algorithm statistics
--------------------------
Number of refinements: 3
Number of successful refinements: 2
Number of failed refinements: 0
Max. size of reached set before ref.: 31
Max. size of reached set after ref.: 2
Avg. size of reached set before ref.: 22.67
Avg. size of reached set after ref.: 2.00
Total time for CEGAR algorithm: 0.045s
Time for refinements: 0.032s
Average time for refinement: 0.010s
Max time for refinement: 0.013s
Counterexample-Check Algorithm statistics
-----------------------------------------
Number of counterexample checks: 1
Number of infeasible paths: 1 (100%)
Time for counterexample checks: 0.046s
RestartAlgorithm switches to the next configuration... (RestartAlgorithm.run, INFO)
Using the following resource limits: CPU-time limit of 60s (Analysis3:ResourceLimitChecker.fromConfiguration, INFO)
Using predicate analysis with MathSAT5 version 5.2.12 (6de13e7f4050) (Jun 5 2014 09:12:40, gmp 5.0.5, gcc 4.6.3, 64-bit) and JFactory 1.21. (Analysis3:PredicateCPA:PredicateCPA., INFO)
Creating formula for program (Analysis3:BMCAlgorithm.run, INFO)
Finding invariants (Analysis3:CPAInvariantGenerator$InvariantGenerationTask.call, INFO)
Starting satisfiability check... (Analysis3:BMCAlgorithm.checkTargetStates, INFO)
Starting assertions check... (Analysis3:BMCAlgorithm.checkBoundingAssertions, INFO)
Running algorithm to create induction hypothesis (Analysis3:BMCAlgorithm$KInductionProver.check, INFO)
Starting induction check... (Analysis3:BMCAlgorithm$KInductionProver.check, INFO)
Adjusting maxLoopIterations to 2 (Analysis3:LoopstackCPA:LoopstackCPA.adjustPrecision, INFO)
Starting satisfiability check... (Analysis3:BMCAlgorithm.checkTargetStates, INFO)
Error found, creating error path (Analysis3:BMCAlgorithm.addCounterexampleTo, INFO)
Adjusting interestingVariableLimit to 1 (Analysis3:InvariantsCPA:InvariantsCPA$InterestingVariableLimitAdjuster.adjustConditions, INFO)
ARG branching without AssumeEdge at ARG node 210. (Analysis3:PredicateCPA:PathFormulaManagerImpl.buildBranchingFormula, WARNING)
Could not create error path because of missing branching information! (Analysis3:BMCAlgorithm.addCounterexampleTo, WARNING)
Error path found, starting counterexample check with CPACHECKER. (Analysis3:CounterexampleCheckAlgorithm.checkCounterexample, INFO)
Using the following resource limits: CPU-time limit of 900s (Analysis3:CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO)
Using predicate analysis with MathSAT5 version 5.2.12 (6de13e7f4050) (Jun 5 2014 09:12:40, gmp 5.0.5, gcc 4.6.3, 64-bit) and JFactory 1.21. (Analysis3:CounterexampleCheck:PredicateCPA:PredicateCPA., INFO)
Error path found and confirmed by counterexample check with CPACHECKER. (Analysis3:CounterexampleCheckAlgorithm.checkCounterexample, INFO)
Error path found, starting counterexample check with CPACHECKER. (Analysis3:CounterexampleCheckAlgorithm.checkCounterexample, INFO)
Using the following resource limits: CPU-time limit of 900s (Analysis3:CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO)
Using predicate analysis with MathSAT5 version 5.2.12 (6de13e7f4050) (Jun 5 2014 09:12:40, gmp 5.0.5, gcc 4.6.3, 64-bit) and JFactory 1.21. (Analysis3:CounterexampleCheck:PredicateCPA:PredicateCPA., INFO)
Error path found, but identified as infeasible by counterexample check with CPACHECKER. (Analysis3:CounterexampleCheckAlgorithm.checkCounterexample, INFO)
Warning: Analysis not completed (Refinement failed: External tool verified counterexample as infeasible) (CounterexampleCheckAlgorithm.checkCounterexample, WARNING)
Statistics for algorithm 3 of 6
===============================
Total time for algorithm 3: 0.240s
PredicateCPA statistics
-----------------------
Number of abstractions: 0 (0% of all post computations)
Number of strengthen sat checks: 0
Number of coverage checks: 8
BDD entailment checks: 0
Number of SMT sat checks: 0
trivial: 0
cached: 0
Max ABE block size: 0
Number of predicates discovered: 0
Time for post operator: 0.019s
Time for path formula creation: 0.014s
Time for strengthen operator: 0.001s
Time for prec operator: 0.000s
Time for merge operator: 0.001s
Time for coverage check: 0.000s
Total time for SMT solver (w/o itp): 0.000s
Number of BDD nodes: 202
Size of BDD node table: 10007
Size of BDD node cleanup queue: 0 (count: 1, min: 0, max: 0, avg: 0.00)
Time for BDD node cleanup: 0.000s
Time for BDD garbage collection: 0.000s (in 0 runs)
PrecisionBootstrap statistics
-----------------------------
Init. function predicates: 0
Init. global predicates: 0
Init. location predicates: 0
Loopstack CPA statistics
------------------------
Bound k:2
Maximum loop iteration reached:3
ValueAnalysisCPA statistics
---------------------------
Number of variables: 108 (count: 62, min: 0, max: 4, avg: 1.74)
Number of global variables: 0 (count: 62, min: 0, max: 0, avg: 0.00)
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.001s
Automaton transfers with branching: 0
Automaton transfer successors: 120 (count: 127, min: 0, max: 1, avg: 0.94) [0 x 7, 1 x 120]
CPA algorithm statistics
------------------------
Number of iterations: 103
Max size of waitlist: 4
Average size of waitlist: 2
Number of computed successors: 100
Max successors for one state: 2
Number of times merged: 4
Number of times stopped: 4
Number of times breaked: 0
Total time for CPA algorithm: 0.041s (Max: 0.015s)
Time for choose from waitlist: 0.002s
Time for precision adjustment: 0.001s
Time for transfer relation: 0.035s
Time for merge operator: 0.001s
Time for stop operator: 0.000s
Time for adding to reached set: 0.000s
BMC algorithm statistics
------------------------
Time for final sat check: 0.001s
Time for error path creation: 0.001s
Time for bounding assertions check: 0.001s
Number of cut points for induction: 0
Time for induction formula creation: 0.013s
Time for invariant generation: 0.052s
Time for induction check: 0.001s
Counterexample-Check Algorithm statistics
-----------------------------------------
Number of counterexample checks: 1
Number of infeasible paths: 1 (100%)
Time for counterexample checks: 0.070s
RestartAlgorithm switches to the next configuration... (RestartAlgorithm.run, INFO)
Using predicate analysis with MathSAT5 version 5.2.12 (6de13e7f4050) (Jun 5 2014 09:12:40, gmp 5.0.5, gcc 4.6.3, 64-bit) and JFactory 1.21. (Analysis4:PredicateCPA:PredicateCPA., INFO)
Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (Analysis4:PredicateCPA:PredicateCPARefiner., INFO)
Error path found, starting counterexample check with CPACHECKER. (Analysis4:CounterexampleCheckAlgorithm.checkCounterexample, INFO)
Using the following resource limits: CPU-time limit of 900s (Analysis4:CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO)
Using predicate analysis with MathSAT5 version 5.2.12 (6de13e7f4050) (Jun 5 2014 09:12:40, gmp 5.0.5, gcc 4.6.3, 64-bit) and JFactory 1.21. (Analysis4:CounterexampleCheck:PredicateCPA:PredicateCPA., INFO)
Error path found, but identified as infeasible by counterexample check with CPACHECKER. (Analysis4:CounterexampleCheckAlgorithm.checkCounterexample, INFO)
Warning: Analysis not completed (Refinement failed: External tool verified counterexample as infeasible) (CounterexampleCheckAlgorithm.checkCounterexample, WARNING)
Statistics for algorithm 4 of 6
===============================
Total time for algorithm 4: 0.108s
PredicateCPA statistics
-----------------------
Number of abstractions: 5 (6% of all post computations)
Times abstraction was reused: 0
Because of function entry/exit: 0 (0%)
Because of loop head: 5 (100%)
Because of join nodes: 0 (0%)
Because of threshold: 0 (0%)
Times precision was empty: 2 (40%)
Times precision was {false}: 0 (0%)
Times result was cached: 0 (0%)
Times cartesian abs was used: 0 (0%)
Times boolean abs was used: 3 (60%)
Times result was 'false': 0 (0%)
Number of strengthen sat checks: 8
Times result was 'false': 4 (50%)
Number of coverage checks: 1
BDD entailment checks: 1
Number of SMT sat checks: 8
trivial: 0
cached: 1
Max ABE block size: 10
Number of predicates discovered: 5
Number of abstraction locations: 2
Max number of predicates per location: 3
Avg number of predicates per location: 2
Total predicates per abstraction: 7
Max number of predicates per abstraction: 3
Avg number of predicates per abstraction: 2.33
Number of irrelevant predicates: 0 (0%)
Number of preds handled by boolean abs: 7 (100%)
Total number of models for allsat: 3
Max number of models for allsat: 1
Avg number of models for allsat: 1.00
Number of path formula cache hits: 47 (36%)
Time for post operator: 0.006s
Time for path formula creation: 0.005s
Actual computation: 0.008s
Time for strengthen operator: 0.003s
Time for satisfiability checks: 0.003s
Time for prec operator: 0.007s
Time for abstraction: 0.007s (Max: 0.002s, Count: 5)
Boolean abstraction: 0.003s
Solving time: 0.000s (Max: 0.000s)
Model enumeration time: 0.000s
Time for BDD construction: 0.002s (Max: 0.001s)
Time for merge operator: 0.000s
Time for coverage check: 0.000s
Time for BDD entailment checks: 0.000s
Total time for SMT solver (w/o itp): 0.003s
Number of BDD nodes: 209
Size of BDD node table: 10007
Size of BDD node cleanup queue: 0 (count: 32, min: 0, max: 0, avg: 0.00)
Time for BDD node cleanup: 0.000s
Time for BDD garbage collection: 0.000s (in 0 runs)
PrecisionBootstrap statistics
-----------------------------
Init. function predicates: 0
Init. global predicates: 0
Init. location predicates: 0
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.003s
Automaton transfers with branching: 0
Automaton transfer successors: 119 (count: 119, min: 1, max: 1, avg: 1.00) [1 x 119]
CPA algorithm statistics
------------------------
Number of iterations: 77
Max size of waitlist: 4
Average size of waitlist: 2
Number of computed successors: 85
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 0
Number of times breaked: 4
Total time for CPA algorithm: 0.026s (Max: 0.012s)
Time for choose from waitlist: 0.000s
Time for precision adjustment: 0.007s
Time for transfer relation: 0.013s
Time for merge operator: 0.000s
Time for stop operator: 0.002s
Time for adding to reached set: 0.001s
Predicate-Abstraction Refiner statistics
----------------------------------------
Avg. length of target path (in blocks): 9 (count: 4, min: 2, max: 3, avg: 2.25)
Time for refinement: 0.021s
Counterexample analysis: 0.009s (Max: 0.004s, Calls: 4)
Refinement sat check: 0.002s
Interpolant computation: 0.001s
Error path post-processing: 0.000s
Path-formulas extraction: 0.001s
Building the counterexample trace: 0.009s
Extracting precise counterexample: 0.008s
Predicate creation: 0.001s
Precision update: 0.000s
ARG update: 0.000s
Length of refined path (in blocks): 4 (count: 2, min: 2, max: 2, avg: 2.00)
Number of affected states: 2 (count: 2, min: 1, max: 1, avg: 1.00)
Length (states) of path with itp 'true': 0 (count: 2, min: 0, max: 0, avg: 0.00)
Length (states) of path with itp non-trivial itp: 2 (count: 2, min: 1, max: 1, avg: 1.00)
Length (states) of path with itp 'false': 0 (count: 2, min: 0, max: 0, avg: 0.00)
Different non-trivial interpolants along paths: 0 (count: 2, min: 0, max: 0, avg: 0.00)
Equal non-trivial interpolants along paths: 0 (count: 2, min: 0, max: 0, avg: 0.00)
Different precisions along paths: 0 (count: 0, min: 0, max: 0, avg: 0.00)
Equal precisions along paths: 0 (count: 0, min: 0, max: 0, avg: 0.00)
Number of refs with location-based cutoff: 0
CEGAR algorithm statistics
--------------------------
Number of refinements: 4
Number of successful refinements: 3
Number of failed refinements: 0
Max. size of reached set before ref.: 45
Max. size of reached set after ref.: 6
Avg. size of reached set before ref.: 24.75
Avg. size of reached set after ref.: 4.33
Total time for CEGAR algorithm: 0.047s
Time for refinements: 0.021s
Average time for refinement: 0.005s
Max time for refinement: 0.014s
Counterexample-Check Algorithm statistics
-----------------------------------------
Number of counterexample checks: 1
Number of infeasible paths: 1 (100%)
Time for counterexample checks: 0.036s
RestartAlgorithm switches to the next configuration... (RestartAlgorithm.run, INFO)
Using the following resource limits: CPU-time limit of 900s (Analysis5:ResourceLimitChecker.fromConfiguration, INFO)
Using predicate analysis with MathSAT5 version 5.2.12 (6de13e7f4050) (Jun 5 2014 09:12:40, gmp 5.0.5, gcc 4.6.3, 64-bit) and JFactory 1.21. (Analysis5:PredicateCPA:PredicateCPA., INFO)
Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (Analysis5:PredicateCPA:PredicateCPARefiner., INFO)
Error path found, starting counterexample check with CBMC. (Analysis5:CounterexampleCheckAlgorithm.checkCounterexample, INFO)
Error path found and confirmed by counterexample check with CBMC. (Analysis5:CounterexampleCheckAlgorithm.checkCounterexample, INFO)
Stopping analysis ... (CPAchecker.runAlgorithm, INFO)
Restart Algorithm statistics
----------------------------
Number of algorithms provided: 6
Number of algorithms used: 5
Total time for algorithm 5: 0.132s
PredicateCPA statistics
-----------------------
Number of abstractions: 5 (6% of all post computations)
Times abstraction was reused: 0
Because of function entry/exit: 0 (0%)
Because of loop head: 5 (100%)
Because of join nodes: 0 (0%)
Because of threshold: 0 (0%)
Times precision was empty: 2 (40%)
Times precision was {false}: 0 (0%)
Times result was cached: 0 (0%)
Times cartesian abs was used: 0 (0%)
Times boolean abs was used: 3 (60%)
Times result was 'false': 0 (0%)
Number of strengthen sat checks: 8
Times result was 'false': 4 (50%)
Number of coverage checks: 1
BDD entailment checks: 1
Number of SMT sat checks: 8
trivial: 0
cached: 1
Max ABE block size: 10
Number of predicates discovered: 4
Number of abstraction locations: 2
Max number of predicates per location: 2
Avg number of predicates per location: 2
Total predicates per abstraction: 5
Max number of predicates per abstraction: 2
Avg number of predicates per abstraction: 1.67
Number of irrelevant predicates: 0 (0%)
Number of preds handled by boolean abs: 5 (100%)
Total number of models for allsat: 3
Max number of models for allsat: 1
Avg number of models for allsat: 1.00
Number of path formula cache hits: 47 (36%)
Time for post operator: 0.007s
Time for path formula creation: 0.006s
Actual computation: 0.010s
Time for strengthen operator: 0.007s
Time for satisfiability checks: 0.006s
Time for prec operator: 0.006s
Time for abstraction: 0.006s (Max: 0.002s, Count: 5)
Boolean abstraction: 0.005s
Solving time: 0.005s (Max: 0.002s)
Model enumeration time: 0.000s
Time for BDD construction: 0.000s (Max: 0.000s)
Time for merge operator: 0.000s
Time for coverage check: 0.000s
Time for BDD entailment checks: 0.000s
Total time for SMT solver (w/o itp): 0.011s
Number of BDD nodes: 205
Size of BDD node table: 10007
Size of BDD node cleanup queue: 0 (count: 31, min: 0, max: 0, avg: 0.00)
Time for BDD node cleanup: 0.000s
Time for BDD garbage collection: 0.000s (in 0 runs)
PrecisionBootstrap statistics
-----------------------------
Init. function predicates: 0
Init. global predicates: 0
Init. location predicates: 0
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.003s
Automaton transfers with branching: 0
Automaton transfer successors: 119 (count: 119, min: 1, max: 1, avg: 1.00) [1 x 119]
CPA algorithm statistics
------------------------
Number of iterations: 77
Max size of waitlist: 4
Average size of waitlist: 2
Number of computed successors: 85
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 0
Number of times breaked: 4
Total time for CPA algorithm: 0.026s (Max: 0.013s)
Time for choose from waitlist: 0.000s
Time for precision adjustment: 0.007s
Time for transfer relation: 0.018s
Time for merge operator: 0.000s
Time for stop operator: 0.001s
Time for adding to reached set: 0.000s
Predicate-Abstraction Refiner statistics
----------------------------------------
Avg. length of target path (in blocks): 9 (count: 4, min: 2, max: 3, avg: 2.25)
Time for refinement: 0.019s
Counterexample analysis: 0.010s (Max: 0.006s, Calls: 4)
Refinement sat check: 0.005s
Interpolant computation: 0.000s
Error path post-processing: 0.000s
Path-formulas extraction: 0.000s
Building the counterexample trace: 0.010s
Extracting precise counterexample: 0.006s
Predicate creation: 0.000s
Precision update: 0.000s
ARG update: 0.002s
Length of refined path (in blocks): 4 (count: 2, min: 2, max: 2, avg: 2.00)
Number of affected states: 2 (count: 2, min: 1, max: 1, avg: 1.00)
Length (states) of path with itp 'true': 0 (count: 2, min: 0, max: 0, avg: 0.00)
Length (states) of path with itp non-trivial itp: 2 (count: 2, min: 1, max: 1, avg: 1.00)
Length (states) of path with itp 'false': 0 (count: 2, min: 0, max: 0, avg: 0.00)
Different non-trivial interpolants along paths: 0 (count: 2, min: 0, max: 0, avg: 0.00)
Equal non-trivial interpolants along paths: 0 (count: 2, min: 0, max: 0, avg: 0.00)
Different precisions along paths: 0 (count: 0, min: 0, max: 0, avg: 0.00)
Equal precisions along paths: 0 (count: 0, min: 0, max: 0, avg: 0.00)
Number of refs with location-based cutoff: 0
CEGAR algorithm statistics
--------------------------
Number of refinements: 4
Number of successful refinements: 3
Number of failed refinements: 0
Max. size of reached set before ref.: 45
Max. size of reached set after ref.: 6
Avg. size of reached set before ref.: 24.75
Avg. size of reached set after ref.: 4.33
Total time for CEGAR algorithm: 0.045s
Time for refinements: 0.019s
Average time for refinement: 0.004s
Max time for refinement: 0.012s
Counterexample-Check Algorithm statistics
-----------------------------------------
Number of counterexample checks: 1
Number of infeasible paths: 0 (0%)
Time for counterexample checks: 0.067s
Time for running CBMC: 0.064s
CPAchecker general statistics
-----------------------------
Number of program locations: 25
Number of functions: 2
Number of loops: 1
Size of reached set: 45
Number of reached locations: 25 (100%)
Avg states per location: 1
Max states per location: 4 (at node N1)
Number of reached functions: 2 (100%)
Number of partitions: 44
Avg size of partitions: 1
Max size of partitions: 2 (with key [N18 (before lines 82-90), Function main called from node N9, stack depth 1 [23442dbd], stack [main], Init])
Number of target states: 1
Size of final wait list 3
Time for analysis setup: 0.405s
Time for loading CPAs: 0.003s
Time for loading parser: 0.199s
Time for CFA construction: 0.183s
Time for parsing file(s): 0.097s
Time for AST to CFA: 0.052s
Time for CFA sanity check: 0.000s
Time for post-processing: 0.022s
Time for Analysis: 1.162s
CPU time for analysis: 1.950s
Total time for CPAchecker: 1.568s
Total CPU time for CPAchecker: 2.830s
Verification result: FALSE. Property violation (__VERIFIER_error
(
)
; called in lines 37-40) found by chosen configuration.
More details about the verification run can be found in the directory "./output".