scripts/cpa.sh -sv-comp15 -disable-java-assertions -heap 10000m -timelimit 900s -stats -spec ../benchmarks/c/loop-acceleration/ALL.prp ../benchmarks/c/loop-acceleration/underapprox_true-unreach-call2.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_577459129_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_79) 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.148s
ValueAnalysisCPA statistics
---------------------------
Number of variables: 59 (count: 22, min: 0, max: 4, avg: 2.68)
Number of global variables: 0 (count: 22, 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: 58 (count: 58, min: 1, max: 1, avg: 1.00) [1 x 58]
CPA algorithm statistics
------------------------
Number of iterations: 22
Max size of waitlist: 1
Average size of waitlist: 1
Number of computed successors: 21
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.016s (Max: 0.016s)
Time for choose from waitlist: 0.002s
Time for precision adjustment: 0.001s
Time for transfer relation: 0.011s
Time for stop operator: 0.001s
Time for adding to reached set: 0.000s
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: 22
Number of reached locations: 11 (79%)
Avg states per location: 2
Max states per location: 7 (at node N13)
Number of reached functions: 2 (100%)
Number of partitions: 11
Avg size of partitions: 2
Max size of partitions: 7 (with key [N13 (before lines 56-60), Function main called from node N9, stack depth 1 [3d986b90], stack [main], Init])
Number of target states: 0
Time for analysis setup: 0.406s
Time for loading CPAs: 0.003s
Time for loading parser: 0.194s
Time for CFA construction: 0.188s
Time for parsing file(s): 0.102s
Time for AST to CFA: 0.053s
Time for CFA sanity check: 0.000s
Time for post-processing: 0.021s
Time for Analysis: 0.149s
CPU time for analysis: 0.200s
Total time for CPAchecker: 0.556s
Total CPU time for CPAchecker: 1.100s
Verification result: TRUE. No property violation found by chosen configuration.
More details about the verification run can be found in the directory "./output".