scripts/cpa.sh -sv-comp15 -disable-java-assertions -heap 10000m -timelimit 900s -stats -spec ../benchmarks/c/loop-lit/ALL.prp ../benchmarks/c/loop-lit/cggmp2005_true-unreach-call.c.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_69830804_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)
Stopping analysis ... (CPAchecker.runAlgorithm, INFO)
Restart Algorithm statistics
----------------------------
Number of algorithms provided: 6
Number of algorithms used: 1
Total time for algorithm 1: 0.155s
ValueAnalysisCPA statistics
---------------------------
Number of variables: 34 (count: 18, min: 0, max: 3, avg: 1.89)
Number of global variables: 0 (count: 18, 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: 40 (count: 40, min: 1, max: 1, avg: 1.00) [1 x 40]
CPA algorithm statistics
------------------------
Number of iterations: 18
Max size of waitlist: 1
Average size of waitlist: 1
Number of computed successors: 17
Max successors for one state: 1
Number of times merged: 0
Number of times stopped: 0
Number of times breaked: 0
Total time for CPA algorithm: 0.014s (Max: 0.014s)
Time for choose from waitlist: 0.000s
Time for precision adjustment: 0.000s
Time for transfer relation: 0.011s
Time for stop operator: 0.001s
Time for adding to reached set: 0.001s
Counterexample-Check Algorithm statistics
-----------------------------------------
Number of counterexample checks: 0
CPAchecker general statistics
-----------------------------
Number of program locations: 14
Number of functions: 2
Number of loops: 1
Size of reached set: 18
Number of reached locations: 11 (79%)
Avg states per location: 1
Max states per location: 5 (at node N15)
Number of reached functions: 2 (100%)
Number of partitions: 11
Avg size of partitions: 1
Max size of partitions: 5 (with key [N15 (before lines 63-67), Function main called from node N9, stack depth 1 [7f42e1a7], stack [main], Init])
Number of target states: 0
Time for analysis setup: 0.402s
Time for loading CPAs: 0.003s
Time for loading parser: 0.186s
Time for CFA construction: 0.193s
Time for parsing file(s): 0.104s
Time for AST to CFA: 0.055s
Time for CFA sanity check: 0.000s
Time for post-processing: 0.021s
Time for Analysis: 0.156s
CPU time for analysis: 0.240s
Total time for CPAchecker: 0.559s
Total CPU time for CPAchecker: 1.110s
Verification result: TRUE. No property violation found by chosen configuration.
More details about the verification run can be found in the directory "./output".