scripts/cpa.sh -heap 3000M -noout -disable-java-assertions -predicateAnalysis-PredAbsRefiner-ABEl -setprop cpa.predicate.handlePointerAliasing=false -64 -timelimit 900s -stats -spec test/programs/benchmarks/ldv-linux-3.4-simple/ALL.prp test/programs/benchmarks/ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mousedev.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c -------------------------------------------------------------------------------- Running CPAchecker with Java heap of size 3000M. Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO) CPAchecker 1.4-svn (OpenJDK 64-Bit Server VM 1.7.0_65) started (CPAchecker.run, INFO) line 3878: Dead code detected: Goto: case_1 (CFACreationUtils.addEdgeToCFA, INFO) line 3883: Dead code detected: Goto: case_2 (CFACreationUtils.addEdgeToCFA, INFO) line 3888: Dead code detected: Goto: case_4 (CFACreationUtils.addEdgeToCFA, INFO) line 3897: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label case_2 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_1 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_4 is not reachable. (CFAFunctionBuilder.leave, INFO) line 4034: Dead code detected: Goto: case_1 (CFACreationUtils.addEdgeToCFA, INFO) line 4039: Dead code detected: Goto: case_2 (CFACreationUtils.addEdgeToCFA, INFO) line 4044: Dead code detected: Goto: case_4 (CFACreationUtils.addEdgeToCFA, INFO) line 4053: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label case_2 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_1 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_4 is not reachable. (CFAFunctionBuilder.leave, INFO) line 9833: Dead code detected: Goto: case_2 (CFACreationUtils.addEdgeToCFA, INFO) line 9838: Dead code detected: Goto: case_4 (CFACreationUtils.addEdgeToCFA, INFO) line 9843: Dead code detected: Goto: case_8 (CFACreationUtils.addEdgeToCFA, INFO) line 9847: Dead code detected: Goto: switch_default (CFACreationUtils.addEdgeToCFA, INFO) Dead code detected: Label case_2 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label switch_default is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_4 is not reachable. (CFAFunctionBuilder.leave, INFO) Dead code detected: Label case_8 is not reachable. (CFAFunctionBuilder.leave, INFO) Inline assembler ignored, analysis is probably unsound! (CFABuilder.createCFA, WARNING) line 4888: Function pointer *__cil_tmp4 with type void (*)(struct file *, wait_queue_head_t *, struct poll_table_struct *) is called, but no possible target functions were found. (CFunctionPointerResolver.replaceFunctionPointerCall, WARNING) Handling of pointer aliasing is disabled, analysis is unsound if aliased pointers exist. (PredicateCPA:PathFormulaManagerImpl., WARNING) Using predicate analysis with SMTInterpol 2.1-174-ga199d47-comp and JFactory 1.21. (PredicateCPA:PredicateCPA., INFO) Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (PredicateCPA:PredicateCPARefiner., INFO) The following configuration options were specified but are not used: cpa.predicate.memoryAllocationsAlwaysSucceed cpa.predicate.maxPreFilledAllocationSize (CPAchecker.printConfigurationWarnings, WARNING) Starting analysis ... (CPAchecker.runAlgorithm, INFO) Program contains array, or pointer (multiple level of indirection), or field (enable handleFieldAccess and handleFieldAliasing) access; analysis is imprecise in case of aliasing. (PredicateCPA:CtoFormulaConverter.makeVariableUnsafe, WARNING) Assuming external function ldv_initialize to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __raw_spin_lock_init to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __mutex_init to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __init_waitqueue_head to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function dev_set_name to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function device_initialize to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function input_register_handle to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function device_add to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function _raw_spin_lock to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function _raw_spin_unlock to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __wake_up to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function kill_fasync to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function input_close_device to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function input_unregister_handle to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function put_device to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function input_register_handler to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function device_del to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function misc_register to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function memset to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function msecs_to_jiffies to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __list_del_entry to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@58b02770: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(handler) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7df75478: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(lock) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@457d6677: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4b313e1d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(lock) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6b30f750: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@19f636e6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6a65dbc6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@42e407bb: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@28459341: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6097cabc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(handler) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5d8bbd6f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@62e8dbb0: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(handler) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5cdabd4d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@68e6de81: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6e6736dc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1ca04be: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7e6cea21: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@74a4c43a: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(lock) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@9c19db1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@11b39c01: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@62484ff7: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@17ace898: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(lock) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@e8e70f0: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5cd7221: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3d2b9f90: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@65f910c: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(lock) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@4e0e6423: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6527c8f6: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1dc5bb3d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Infeasible counterexample found, but could not remove it from the ARG. Therefore, we cannot prove safety. (CounterexampleCheckAlgorithm.checkCounterexample, WARNING) Assuming external function input_open_device to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function get_device to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Assuming external function __list_add to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Using the following resource limits: CPU-time limit of 900s (CounterexampleCheck:ResourceLimitChecker.fromConfiguration, INFO) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1dfe2677: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(handler) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@5a1dda02: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1728bea1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@63eb3fdd: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@7a71edaa: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6feda7c8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@65e55bd1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@52436bf1: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@6fca908d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(handler) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@453a7cca: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(handler) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@452c22f3: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@14640ce4: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1b27d947: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(lock) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@702ffbcc: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@3289233f: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@2e5524e: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@242f4f5d: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(lock) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@31a9c151: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@515b96e5: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(lock) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@30b94e61: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(mousedev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@f1c6dba: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Dereferencing of a non-pointer in expression *(dev) (org.eclipse.cdt.internal.core.dom.parser.ProblemType@1fc6a0b8: Type depends on an unresolved name) (CounterexampleCheck:ASTConverter.convert, WARNING) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Assuming external function ldv_check_return_value to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) line 4888: Ignoring call via function pointer poll_wait::__cil_tmp4 for which no suitable target was found in line: (*__cil_tmp4)(filp, wait_address, p); (FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING) line 4888: Ignoring function call through function pointer *__cil_tmp4: (*__cil_tmp4)(filp, wait_address, p); (PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING) Assuming external function synchronize_sched to be a constant function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO) Recursion detected, aborting. To ignore recursion, add -skipRecursion to the command line. (CallstackCPA:CallstackTransferRelation.getAbstractSuccessorsForEdge, INFO) Error: line 8362: Unsupported C feature (recursion): mousedev_close_device(mousedev); (CallstackTransferRelation.getAbstractSuccessorsForEdge, SEVERE) PredicateCPA statistics ----------------------- Number of abstractions: 70 (1% of all post computations) Times abstraction was reused: 0 Because of function entry/exit: 0 (0%) Because of loop head: 70 (100%) Because of join nodes: 0 (0%) Because of threshold: 0 (0%) Times precision was empty: 2 (3%) Times precision was {false}: 0 (0%) Times result was cached: 25 (36%) Times cartesian abs was used: 0 (0%) Times boolean abs was used: 43 (61%) Times result was 'false': 6 (9%) Number of strengthen sat checks: 52 Times result was 'false': 46 (88%) Number of coverage checks: 1264 BDD entailment checks: 34 Number of SMT sat checks: 52 trivial: 0 cached: 8 Max ABE block size: 135 Number of predicates discovered: 6 Number of abstraction locations: 3 Max number of predicates per location: 4 Avg number of predicates per location: 3 Total predicates per abstraction: 110 Max number of predicates per abstraction: 4 Avg number of predicates per abstraction: 2.56 Number of irrelevant predicates: 16 (15%) Number of preds handled by boolean abs: 94 (85%) Total number of models for allsat: 37 Max number of models for allsat: 1 Avg number of models for allsat: 0.86 Number of path formula cache hits: 2774 (26%) Time for post operator: 1.091s Time for path formula creation: 0.953s Actual computation: 1.021s Time for strengthen operator: 0.440s Time for satisfiability checks: 0.410s Time for prec operator: 2.348s Time for abstraction: 2.346s (Max: 0.303s, Count: 70) Boolean abstraction: 1.016s Solving time: 0.873s (Max: 0.207s) Model enumeration time: 0.115s Time for BDD construction: 0.003s (Max: 0.001s) Time for merge operator: 0.582s Time for coverage check: 0.003s Time for BDD entailment checks: 0.002s Total time for SMT solver (w/o itp): 1.398s Number of BDD nodes: 212 Size of BDD node table: 10007 Size of BDD node cleanup queue: 84 (count: 244, min: 0, max: 65, avg: 0,34) 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.142s Automaton transfers with branching: 0 Automaton transfer successors: 25642 (count: 25642, min: 1, max: 1, avg: 1,00) [1 x 25642] CPA algorithm statistics ------------------------ Number of iterations: 6265 Max size of waitlist: 38 Average size of waitlist: 20 Number of computed successors: 6982 Max successors for one state: 2 Number of times merged: 615 Number of times stopped: 649 Number of times breaked: 6 Total time for CPA algorithm: 5.686s (Max: 2.856s) Time for choose from waitlist: 0.059s Time for precision adjustment: 2.467s Time for transfer relation: 2.093s Time for merge operator: 0.711s Time for stop operator: 0.056s Time for adding to reached set: 0.087s Predicate-Abstraction Refiner statistics ---------------------------------------- Avg. length of target path (in blocks): 21 (count: 6, min: 2, max: 5, avg: 3,50) Time for refinement: 2.311s Counterexample analysis: 0.781s (Max: 0.307s, Calls: 6) Refinement sat check: 0.589s Interpolant computation: 0.023s Error path post-processing: 1.439s Path-formulas extraction: 0.000s Building the counterexample trace: 0.781s Extracting precise counterexample: 1.439s Predicate creation: 0.000s Precision update: 0.001s ARG update: 0.065s Length of refined path (in blocks): 8 (count: 3, min: 2, max: 3, avg: 2,67) Number of affected states: 3 (count: 3, min: 1, max: 1, avg: 1,00) Length (states) of path with itp 'true': 2 (count: 3, min: 0, max: 1, avg: 0,67) Length (states) of path with itp non-trivial itp: 3 (count: 3, min: 1, max: 1, avg: 1,00) Length (states) of path with itp 'false': 2 (count: 3, min: 0, max: 1, avg: 0,67) Different non-trivial interpolants along paths: 0 (count: 3, min: 0, max: 0, avg: 0,00) Equal non-trivial interpolants along paths: 0 (count: 3, 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: 6 Number of successful refinements: 4 Number of failed refinements: 0 Max. size of reached set before ref.: 2192 Max. size of reached set after ref.: 528 Avg. size of reached set before ref.: 1572.17 Avg. size of reached set after ref.: 363.00 Total time for CEGAR algorithm: 8.010s Time for refinements: 2.324s Average time for refinement: 0.387s Max time for refinement: 1.029s Counterexample-Check Algorithm statistics ----------------------------------------- Number of counterexample checks: 2 Number of infeasible paths: 2 (100%) Time for counterexample checks: 1.934s CPAchecker general statistics ----------------------------- Number of program locations: 1428 Number of functions: 90 Number of loops: 8 Size of reached set: 2630 Number of reached locations: 956 (67%) Avg states per location: 2 Max states per location: 39 (at node N4949) Number of reached functions: 61 (68%) Number of partitions: 2630 Avg size of partitions: 1 Max size of partitions: 1 Number of target states: 0 Size of final wait list 24 Time for analysis setup: 3.384s Time for loading CPAs: 0.501s Time for loading parser: 0.435s Time for CFA construction: 2.399s Time for parsing file(s): 0.949s Time for AST to CFA: 0.795s Time for CFA sanity check: 0.001s Time for post-processing: 0.471s Time for var class.: 0.000s Time for Analysis: 9.944s CPU time for analysis: 9.940s Total time for CPAchecker: 13.328s Total CPU time for CPAchecker: 13.310s Time for Garbage Collector: 0.275s (in 4 runs) Garbage Collector(s) used: PS MarkSweep, PS Scavenge Used heap memory: 290MB ( 276 MiB) max; 118MB ( 112 MiB) avg; 316MB ( 301 MiB) peak Used non-heap memory: 27MB ( 26 MiB) max; 22MB ( 21 MiB) avg; 27MB ( 26 MiB) peak Used in PS Old Gen pool: 29MB ( 28 MiB) max; 6MB ( 6 MiB) avg; 29MB ( 28 MiB) peak Allocated heap memory: 902MB ( 860 MiB) max; 614MB ( 586 MiB) avg Allocated non-heap memory: 28MB ( 26 MiB) max; 25MB ( 24 MiB) avg Total process virtual memory: 4969MB ( 4739 MiB) max; 4916MB ( 4688 MiB) avg Verification result: UNKNOWN, incomplete analysis. More details about the verification run can be found in the directory "./output".