scripts/cpa.sh -sv-comp15 -disable-java-assertions -heap 10000m -timelimit 900s -stats -spec ../benchmarks/c/loop-invgen/ALL.prp ../benchmarks/c/loop-invgen/nested6_true-unreach-call.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_1861049096_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)
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.483s
ValueAnalysisCPA statistics
---------------------------
Number of variables: 97633 (count: 48818, min: 0, max: 4, avg: 2.00)
Number of global variables: 0 (count: 48818, min: 0, max: 0, avg: 0.00)
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.070s
Automaton transfers with branching: 0
Automaton transfer successors: 83690 (count: 83690, min: 1, max: 1, avg: 1.00) [1 x 83690]
CPA algorithm statistics
------------------------
Number of iterations: 41843
Max size of waitlist: 6974
Average size of waitlist: 3487
Number of computed successors: 55789
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 6972
Number of times breaked: 0
Total time for CPA algorithm: 58.347s (Max: 58.347s)
Time for choose from waitlist: 0.032s
Time for precision adjustment: 0.063s
Time for transfer relation: 0.676s
Time for stop operator: 57.304s
Time for adding to reached set: 0.118s
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)
Warning: Analysis 2 stopped (The CPU-time limit of 60s has elapsed.) (ShutdownNotifier.shutdownIfNecessary, WARNING)
Statistics for algorithm 2 of 6
===============================
Total time for algorithm 2: 57.595s
ValueAnalysisCPA statistics
---------------------------
Number of variables: 87869 (count: 43947, min: 0, max: 2, avg: 2.00)
Number of global variables: 0 (count: 43947, min: 0, max: 0, avg: 0.00)
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.028s
Automaton transfers with branching: 0
Automaton transfer successors: 80603 (count: 80603, min: 1, max: 1, avg: 1.00) [1 x 80603]
ComponentAwarePrecisionAdjustment Statistics statistics
-------------------------------------------------------
Total time for precision adjustment: 0.170s
Total time for composite: 0.019s
Total time for abstraction computation: 0.108s
Total time for path threshold: 0.001s
Number of abstraction computations: 51291
CPA algorithm statistics
------------------------
Number of iterations: 36640
Max size of waitlist: 7325
Average size of waitlist: 3660
Number of computed successors: 51291
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 7325
Number of times breaked: 1
Total time for CPA algorithm: 57.535s (Max: 57.530s)
Time for choose from waitlist: 0.015s
Time for precision adjustment: 0.188s
Time for transfer relation: 0.340s
Time for stop operator: 56.821s
Time for adding to reached set: 0.092s
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: 21 (count: 20, min: 0, max: 4, avg: 1.05)
Size of interpolant: 18 (count: 20, min: 0, max: 2, avg: 0.90)
Time for interpolation: 0.007s
CEGAR algorithm statistics
--------------------------
Number of refinements: 1
Number of successful refinements: 1
Number of failed refinements: 0
Max. size of reached set before ref.: 31
Max. size of reached set after ref.: 11
Avg. size of reached set before ref.: 31.00
Avg. size of reached set after ref.: 11.00
Total time for CEGAR algorithm: 57.554s
Time for refinements: 0.019s
Average time for refinement: 0.019s
Max time for refinement: 0.019s
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 (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)
Could not use induction for proving program safety, program has too many loops (Analysis3:BMCAlgorithm$KInductionProver., WARNING)
Starting satisfiability check... (Analysis3:BMCAlgorithm.checkTargetStates, INFO)
Starting assertions check... (Analysis3:BMCAlgorithm.checkBoundingAssertions, INFO)
Adjusting maxLoopIterations to 2 (Analysis3:LoopstackCPA:LoopstackCPA.adjustPrecision, INFO)
Starting satisfiability check... (Analysis3:BMCAlgorithm.checkTargetStates, INFO)
Starting assertions check... (Analysis3:BMCAlgorithm.checkBoundingAssertions, INFO)
Adjusting maxLoopIterations to 3 (Analysis3:LoopstackCPA:LoopstackCPA.adjustPrecision, INFO)
Starting satisfiability check... (Analysis3:BMCAlgorithm.checkTargetStates, INFO)
Error found, creating error path (Analysis3:BMCAlgorithm.addCounterexampleTo, INFO)
ARG branching without AssumeEdge at ARG node 107544. (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, 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.789s
PredicateCPA statistics
-----------------------
Number of abstractions: 0 (0% of all post computations)
Number of strengthen sat checks: 0
Number of coverage checks: 778
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.144s
Time for path formula creation: 0.142s
Time for strengthen operator: 0.004s
Time for prec operator: 0.000s
Time for merge operator: 0.018s
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:3
Maximum loop iteration reached:4
ValueAnalysisCPA statistics
---------------------------
Number of variables: 2769 (count: 711, min: 0, max: 5, avg: 3.89)
Number of global variables: 0 (count: 711, min: 0, max: 0, avg: 0.00)
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.020s
Automaton transfers with branching: 0
Automaton transfer successors: 1398 (count: 1438, min: 0, max: 1, avg: 0.97) [0 x 40, 1 x 1398]
CPA algorithm statistics
------------------------
Number of iterations: 1063
Max size of waitlist: 13
Average size of waitlist: 6
Number of computed successors: 1119
Max successors for one state: 2
Number of times merged: 389
Number of times stopped: 389
Number of times breaked: 0
Total time for CPA algorithm: 0.330s (Max: 0.227s)
Time for choose from waitlist: 0.001s
Time for precision adjustment: 0.003s
Time for transfer relation: 0.255s
Time for merge operator: 0.044s
Time for stop operator: 0.018s
Time for adding to reached set: 0.002s
BMC algorithm statistics
------------------------
Time for final sat check: 0.020s
Time for error path creation: 0.005s
Time for bounding assertions check: 0.008s
Counterexample-Check Algorithm statistics
-----------------------------------------
Number of counterexample checks: 1
Number of infeasible paths: 1 (100%)
Time for counterexample checks: 0.202s
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.297s
PredicateCPA statistics
-----------------------
Number of abstractions: 81 (12% of all post computations)
Times abstraction was reused: 0
Because of function entry/exit: 0 (0%)
Because of loop head: 81 (100%)
Because of join nodes: 0 (0%)
Because of threshold: 0 (0%)
Times precision was empty: 9 (11%)
Times precision was {false}: 0 (0%)
Times result was cached: 2 (2%)
Times cartesian abs was used: 0 (0%)
Times boolean abs was used: 70 (86%)
Times result was 'false': 9 (11%)
Number of strengthen sat checks: 45
Times result was 'false': 36 (80%)
Number of coverage checks: 95
BDD entailment checks: 95
Number of SMT sat checks: 45
trivial: 0
cached: 3
Max ABE block size: 9
Number of predicates discovered: 15
Number of abstraction locations: 4
Max number of predicates per location: 9
Avg number of predicates per location: 5
Total predicates per abstraction: 330
Max number of predicates per abstraction: 9
Avg number of predicates per abstraction: 4.71
Number of irrelevant predicates: 39 (12%)
Number of preds handled by boolean abs: 291 (88%)
Total number of models for allsat: 149
Max number of models for allsat: 12
Avg number of models for allsat: 2.13
Number of path formula cache hits: 488 (63%)
Time for post operator: 0.022s
Time for path formula creation: 0.020s
Actual computation: 0.018s
Time for strengthen operator: 0.024s
Time for satisfiability checks: 0.022s
Time for prec operator: 0.110s
Time for abstraction: 0.110s (Max: 0.004s, Count: 81)
Boolean abstraction: 0.044s
Solving time: 0.023s (Max: 0.001s)
Model enumeration time: 0.001s
Time for BDD construction: 0.003s (Max: 0.001s)
Time for merge operator: 0.000s
Time for coverage check: 0.004s
Time for BDD entailment checks: 0.004s
Total time for SMT solver (w/o itp): 0.046s
Number of BDD nodes: 737
Size of BDD node table: 10007
Size of BDD node cleanup queue: 0 (count: 618, 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.002s
Automaton transfers with branching: 0
Automaton transfer successors: 840 (count: 840, min: 1, max: 1, avg: 1.00) [1 x 840]
CPA algorithm statistics
------------------------
Number of iterations: 559
Max size of waitlist: 9
Average size of waitlist: 3
Number of computed successors: 618
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 26
Number of times breaked: 9
Total time for CPA algorithm: 0.179s (Max: 0.060s)
Time for choose from waitlist: 0.001s
Time for precision adjustment: 0.111s
Time for transfer relation: 0.053s
Time for merge operator: 0.001s
Time for stop operator: 0.005s
Time for adding to reached set: 0.002s
Predicate-Abstraction Refiner statistics
----------------------------------------
Avg. length of target path (in blocks): 50 (count: 9, min: 3, max: 8, avg: 5.56)
Time for refinement: 0.038s
Counterexample analysis: 0.019s (Max: 0.005s, Calls: 9)
Refinement sat check: 0.009s
Interpolant computation: 0.004s
Error path post-processing: 0.000s
Path-formulas extraction: 0.000s
Building the counterexample trace: 0.019s
Extracting precise counterexample: 0.014s
Predicate creation: 0.001s
Precision update: 0.002s
ARG update: 0.001s
Length of refined path (in blocks): 36 (count: 7, min: 3, max: 8, avg: 5.14)
Number of affected states: 22 (count: 7, min: 1, max: 6, avg: 3.14)
Length (states) of path with itp 'true': 7 (count: 7, min: 0, max: 2, avg: 1.00)
Length (states) of path with itp non-trivial itp: 22 (count: 7, min: 1, max: 6, avg: 3.14)
Length (states) of path with itp 'false': 2 (count: 7, min: 0, max: 1, avg: 0.29)
Different non-trivial interpolants along paths: 8 (count: 7, min: 0, max: 3, avg: 1.14)
Equal non-trivial interpolants along paths: 7 (count: 7, min: 0, max: 3, avg: 1.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: 9
Number of successful refinements: 8
Number of failed refinements: 0
Max. size of reached set before ref.: 175
Max. size of reached set after ref.: 38
Avg. size of reached set before ref.: 82.22
Avg. size of reached set after ref.: 18.38
Total time for CEGAR algorithm: 0.219s
Time for refinements: 0.040s
Average time for refinement: 0.004s
Max time for refinement: 0.019s
Counterexample-Check Algorithm statistics
-----------------------------------------
Number of counterexample checks: 1
Number of infeasible paths: 1 (100%)
Time for counterexample checks: 0.047s
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)
Shutdown requested (The CPU-time limit of 900s has elapsed.), waiting for termination. (ForceTerminationOnShutdown$1.shutdownRequested, WARNING)
Warning: Analysis stopped (The CPU-time limit of 900s has elapsed.) (ShutdownNotifier.shutdownIfNecessary, WARNING)
Restart Algorithm statistics
----------------------------
Number of algorithms provided: 6
Number of algorithms used: 5
Total time for algorithm 5: 754.621s
PredicateCPA statistics
-----------------------
Number of abstractions: 14392 (9% of all post computations)
Times abstraction was reused: 0
Because of function entry/exit: 0 (0%)
Because of loop head: 14392 (100%)
Because of join nodes: 0 (0%)
Because of threshold: 0 (0%)
Times precision was empty: 8 (0%)
Times precision was {false}: 0 (0%)
Times result was cached: 502 (3%)
Times cartesian abs was used: 0 (0%)
Times boolean abs was used: 13882 (96%)
Times result was 'false': 163 (1%)
Number of strengthen sat checks: 13876
Times result was 'false': 13708 (99%)
Number of coverage checks: 762435
BDD entailment checks: 762435
Number of SMT sat checks: 13876
trivial: 0
cached: 4
Max ABE block size: 6
Number of predicates discovered: 172
Number of abstraction locations: 4
Max number of predicates per location: 166
Avg number of predicates per location: 44
Total predicates per abstraction: 1538631
Max number of predicates per abstraction: 166
Avg number of predicates per abstraction: 110.84
Number of irrelevant predicates: 2 (0%)
Number of preds handled by boolean abs: 1538629 (100%)
Total number of models for allsat: 13889
Max number of models for allsat: 2
Avg number of models for allsat: 1.00
Number of path formula cache hits: 180572 (99%)
Time for post operator: 0.328s
Time for path formula creation: 0.272s
Actual computation: 0.144s
Time for strengthen operator: 12.500s
Time for satisfiability checks: 12.390s
Time for prec operator: 159.623s
Time for abstraction: 159.486s (Max: 0.643s, Count: 14392)
Boolean abstraction: 86.236s
Solving time: 40.934s (Max: 0.010s)
Model enumeration time: 0.472s
Time for BDD construction: 7.542s (Max: 0.052s)
Time for merge operator: 0.000s
Time for coverage check: 3.276s
Time for BDD entailment checks: 3.231s
Total time for SMT solver (w/o itp): 53.724s
Number of BDD nodes: 800584
Size of BDD node table: 879881
Size of BDD node cleanup queue: 3907781 (count: 2384296, min: 0, max: 89176, avg: 1.64)
Time for BDD node cleanup: 0.788s
Time for BDD garbage collection: 0.200s (in 25 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.544s
Time for transition matches: 0.100s
Time for transition assertions: 0.017s
Time for transition actions: 0.056s
Automaton transfers with branching: 0
Automaton transfer successors: 197424 (count: 197424, min: 1, max: 1, avg: 1.00) [1 x 197424]
CPA algorithm statistics
------------------------
Number of iterations: 140513
Max size of waitlist: 170
Average size of waitlist: 58
Number of computed successors: 154744
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 5
Number of times breaked: 168
Total time for CPA algorithm: 178.173s (Max: 3.747s)
Time for choose from waitlist: 0.050s
Time for precision adjustment: 159.747s
Time for transfer relation: 14.124s
Time for merge operator: 0.210s
Time for stop operator: 3.624s
Time for adding to reached set: 0.192s
Predicate-Abstraction Refiner statistics
----------------------------------------
Avg. length of target path (in blocks): 14371 (count: 168, min: 4, max: 169, avg: 85.54)
Time for refinement: 576.806s
Counterexample analysis: 576.027s (Max: 14.294s, Calls: 168)
Refinement sat check: 6.342s
Interpolant computation: 568.110s
Error path post-processing: 0.000s
Path-formulas extraction: 0.005s
Building the counterexample trace: 576.470s
Extracting precise counterexample: 0.000s
Predicate creation: 0.085s
Precision update: 0.054s
ARG update: 0.150s
Length of refined path (in blocks): 14193 (count: 166, min: 3, max: 168, avg: 85.50)
Number of affected states: 14027 (count: 166, min: 2, max: 167, avg: 84.50)
Length (states) of path with itp 'true': 0 (count: 166, min: 0, max: 0, avg: 0.00)
Length (states) of path with itp non-trivial itp: 14027 (count: 166, min: 2, max: 167, avg: 84.50)
Length (states) of path with itp 'false': 1 (count: 166, min: 0, max: 1, avg: 0.01)
Different non-trivial interpolants along paths: 13861 (count: 166, min: 1, max: 166, avg: 83.50)
Equal non-trivial interpolants along paths: 0 (count: 166, 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: 168
Number of successful refinements: 167
Number of failed refinements: 0
Max. size of reached set before ref.: 1849
Max. size of reached set after ref.: 11
Avg. size of reached set before ref.: 931.95
Avg. size of reached set after ref.: 10.94
Total time for CEGAR algorithm: 754.599s
Time for refinements: 576.425s
Average time for refinement: 3.431s
Max time for refinement: 14.297s
Counterexample-Check Algorithm statistics
-----------------------------------------
Number of counterexample checks: 0
CPAchecker general statistics
-----------------------------
Number of program locations: 35
Number of functions: 2
Number of loops: 3
Size of reached set: 1849
Number of reached locations: 33 (94%)
Avg states per location: 56
Max states per location: 166 (at node N1)
Number of reached functions: 2 (100%)
Number of partitions: 1684
Avg size of partitions: 1
Max size of partitions: 166 (with key [N38 (before lines 129-137), Function main called from node N9, stack depth 1 [259f2bf7], stack [main], Init])
Number of target states: 1
Size of final wait list 170
Time for analysis setup: 0.415s
Time for loading CPAs: 0.003s
Time for loading parser: 0.196s
Time for CFA construction: 0.196s
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.024s
Time for Analysis: 872.912s
CPU time for analysis: 899.110s
Total time for CPAchecker: 873.328s
Total CPU time for CPAchecker: 900.020s
Verification result: UNKNOWN, incomplete analysis.
More details about the verification run can be found in the directory "./output".