scripts/cpa.sh -sv-comp15 -disable-java-assertions -heap 10000m -timelimit 900s -stats -spec ../benchmarks/c/loops/ALL.prp ../benchmarks/c/loops/for_infinite_loop_2_true-unreach-call_false-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_-1327334956_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)
lines 102-108: Dead code detected: __VERIFIER_assert
(
x
!=
0
)
; (CFACreationUtils.addEdgeToCFA, 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)
Warning: Analysis 1 stopped (The CPU-time limit of 60s has elapsed.) (ShutdownNotifier.shutdownIfNecessary, WARNING)
Statistics for algorithm 1 of 6
===============================
Total time for algorithm 1: 58.103s
ValueAnalysisCPA statistics
---------------------------
Number of variables: 258788 (count: 72463, min: 0, max: 4, avg: 3.57)
Number of global variables: 0 (count: 72463, min: 0, max: 0, avg: 0.00)
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.097s
Automaton transfers with branching: 0
Automaton transfer successors: 93174 (count: 93174, min: 1, max: 1, avg: 1.00) [1 x 93174]
CPA algorithm statistics
------------------------
Number of iterations: 72462
Max size of waitlist: 2
Average size of waitlist: 1
Number of computed successors: 72462
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 0
Number of times breaked: 0
Total time for CPA algorithm: 57.971s (Max: 57.971s)
Time for choose from waitlist: 0.021s
Time for precision adjustment: 0.043s
Time for transfer relation: 0.926s
Time for stop operator: 56.709s
Time for adding to reached set: 0.136s
Counterexample-Check Algorithm statistics
-----------------------------------------
Number of counterexample checks: 0
RestartAlgorithm switches to the next configuration... (RestartAlgorithm.run, INFO)
Using the following resource limits: CPU-time limit of 60s (Analysis2:ResourceLimitChecker.fromConfiguration, INFO)
Stopping analysis ... (CPAchecker.runAlgorithm, INFO)
Restart Algorithm statistics
----------------------------
Number of algorithms provided: 6
Number of algorithms used: 2
Total time for algorithm 2: 0.054s
ValueAnalysisCPA statistics
---------------------------
Number of variables: 14 (count: 13, min: 0, max: 2, avg: 1.08)
Number of global variables: 0 (count: 13, min: 0, max: 0, avg: 0.00)
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.002s
Automaton transfers with branching: 0
Automaton transfer successors: 51 (count: 51, min: 1, max: 1, avg: 1.00) [1 x 51]
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: 25
CPA algorithm statistics
------------------------
Number of iterations: 23
Max size of waitlist: 3
Average size of waitlist: 1
Number of computed successors: 25
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 1
Number of times breaked: 1
Total time for CPA algorithm: 0.005s (Max: 0.003s)
Time for choose from waitlist: 0.000s
Time for precision adjustment: 0.001s
Time for transfer relation: 0.004s
Time for stop operator: 0.000s
Time for adding to reached set: 0.000s
ValueAnalysisDelegatingRefiner statistics
-----------------------------------------
number of value analysis refinements: 1
number of successful valueAnalysis refinements: 1
number of predicate refinements: 0
ValueAnalysisInterpolationBasedRefiner statistics
-------------------------------------------------
Number of interpolations: 1
Number of interpolation queries: 11 (count: 11, min: 0, max: 5, avg: 1.00)
Size of interpolant: 7 (count: 11, min: 0, max: 1, avg: 0.64)
Time for interpolation: 0.005s
CEGAR algorithm statistics
--------------------------
Number of refinements: 1
Number of successful refinements: 1
Number of failed refinements: 0
Max. size of reached set before ref.: 14
Max. size of reached set after ref.: 2
Avg. size of reached set before ref.: 14.00
Avg. size of reached set after ref.: 2.00
Total time for CEGAR algorithm: 0.016s
Time for refinements: 0.011s
Average time for refinement: 0.011s
Max time for refinement: 0.011s
Counterexample-Check Algorithm statistics
-----------------------------------------
Number of counterexample checks: 0
CPAchecker general statistics
-----------------------------
Number of program locations: 16
Number of functions: 2
Number of loops: 1
Size of reached set: 13
Number of reached locations: 13 (81%)
Avg states per location: 1
Max states per location: 1 (at node N0)
Number of reached functions: 2 (100%)
Number of partitions: 13
Avg size of partitions: 1
Max size of partitions: 1
Number of target states: 0
Time for analysis setup: 0.406s
Time for loading CPAs: 0.004s
Time for loading parser: 0.200s
Time for CFA construction: 0.183s
Time for parsing file(s): 0.096s
Time for AST to CFA: 0.052s
Time for CFA sanity check: 0.000s
Time for post-processing: 0.022s
Time for Analysis: 58.216s
CPU time for analysis: 60.280s
Total time for CPAchecker: 58.623s
Total CPU time for CPAchecker: 61.170s
Verification result: TRUE. No property violation found by chosen configuration.
More details about the verification run can be found in the directory "./output".