scripts/cpa.sh -heap 50000M -noout -disable-java-assertions -predicateAnalysis-PredAbsRefiner-ABEl -timelimit 900s -stats -spec test/programs/benchmarks/bitvector/ALL.prp test/programs/benchmarks/bitvector/soft_float_2_true-unreach-call.c.cil.c -------------------------------------------------------------------------------- Running CPAchecker with Java heap of size 50000M. 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) 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) Starting analysis ... (CPAchecker.runAlgorithm, 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) 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) 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) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, 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) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, 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) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, 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) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, 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) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, 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) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, 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) Error path found, but identified as infeasible by counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO) Stopping analysis ... (CPAchecker.runAlgorithm, INFO) Analysis incomplete: no errors found, but not everything could be checked. (CPAchecker.analyzeResult, WARNING) PredicateCPA statistics ----------------------- Number of abstractions: 345 (3% of all post computations) Times abstraction was reused: 0 Because of function entry/exit: 0 (0%) Because of loop head: 345 (100%) Because of join nodes: 0 (0%) Because of threshold: 0 (0%) Times precision was empty: 320 (93%) Times precision was {false}: 7 (2%) Times result was cached: 0 (0%) Times cartesian abs was used: 0 (0%) Times boolean abs was used: 18 (5%) Times result was 'false': 7 (2%) Number of strengthen sat checks: 21 Times result was 'false': 4 (19%) Number of coverage checks: 4289 BDD entailment checks: 169 Number of SMT sat checks: 21 trivial: 0 cached: 1 Max ABE block size: 30 Number of predicates discovered: 6 Number of abstraction locations: 3 Max number of predicates per location: 5 Avg number of predicates per location: 4 Total predicates per abstraction: 79 Max number of predicates per abstraction: 4 Avg number of predicates per abstraction: 3.16 Number of irrelevant predicates: 7 (9%) Number of preds handled by boolean abs: 72 (91%) Total number of models for allsat: 18 Max number of models for allsat: 1 Avg number of models for allsat: 1.00 Number of path formula cache hits: 11641 (75%) Time for post operator: 0.804s Time for path formula creation: 0.710s Actual computation: 0.687s Time for strengthen operator: 0.545s Time for satisfiability checks: 0.526s Time for prec operator: 0.249s Time for abstraction: 0.232s (Max: 0.006s, Count: 345) Boolean abstraction: 0.029s Solving time: 0.006s (Max: 0.001s) Model enumeration time: 0.005s Time for BDD construction: 0.001s (Max: 0.001s) Time for merge operator: 0.104s Time for coverage check: 0.003s Time for BDD entailment checks: 0.001s Total time for SMT solver (w/o itp): 0.537s Number of BDD nodes: 208 Size of BDD node table: 10007 Size of BDD node cleanup queue: 36 (count: 620, min: 0, max: 36, avg: 0,06) 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.163s Automaton transfers with branching: 0 Automaton transfer successors: 25659 (count: 25659, min: 1, max: 1, avg: 1,00) [1 x 25659] CPA algorithm statistics ------------------------ Number of iterations: 9817 Max size of waitlist: 324 Average size of waitlist: 96 Number of computed successors: 12375 Max successors for one state: 2 Number of times merged: 2060 Number of times stopped: 2229 Number of times breaked: 17 Total time for CPA algorithm: 2.888s (Max: 1.809s) Time for choose from waitlist: 0.047s Time for precision adjustment: 0.363s Time for transfer relation: 1.871s Time for merge operator: 0.231s Time for stop operator: 0.077s Time for adding to reached set: 0.104s Predicate-Abstraction Refiner statistics ---------------------------------------- Avg. length of target path (in blocks): 62 (count: 17, min: 2, max: 5, avg: 3,65) Time for refinement: 0.891s Counterexample analysis: 0.457s (Max: 0.103s, Calls: 17) Refinement sat check: 0.262s Interpolant computation: 0.075s Error path post-processing: 0.308s Path-formulas extraction: 0.000s Building the counterexample trace: 0.458s Extracting precise counterexample: 0.308s Predicate creation: 0.001s Precision update: 0.006s ARG update: 0.042s Length of refined path (in blocks): 10 (count: 8, min: 1, max: 3, avg: 1,25) Number of affected states: 2 (count: 8, min: 0, max: 2, avg: 0,25) Length (states) of path with itp 'true': 0 (count: 8, min: 0, max: 0, avg: 0,00) Length (states) of path with itp non-trivial itp: 2 (count: 8, min: 0, max: 2, avg: 0,25) Length (states) of path with itp 'false': 7 (count: 8, min: 0, max: 1, avg: 0,88) Different non-trivial interpolants along paths: 0 (count: 8, min: 0, max: 0, avg: 0,00) Equal non-trivial interpolants along paths: 1 (count: 8, min: 0, max: 1, avg: 0,13) 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: 17 Number of successful refinements: 9 Number of failed refinements: 0 Max. size of reached set before ref.: 4738 Max. size of reached set after ref.: 3158 Avg. size of reached set before ref.: 1459.53 Avg. size of reached set after ref.: 1030.56 Total time for CEGAR algorithm: 3.795s Time for refinements: 0.906s Average time for refinement: 0.053s Max time for refinement: 0.186s Counterexample-Check Algorithm statistics ----------------------------------------- Number of counterexample checks: 8 Number of infeasible paths: 8 (100%) Time for counterexample checks: 0.671s CPAchecker general statistics ----------------------------- Number of program locations: 114 Number of functions: 5 Number of loops: 2 Size of reached set: 698 Number of reached locations: 91 (80%) Avg states per location: 7 Max states per location: 17 (at node N8) Number of reached functions: 4 (80%) Number of partitions: 698 Avg size of partitions: 1 Max size of partitions: 1 Number of target states: 0 Time for analysis setup: 1.499s Time for loading CPAs: 0.550s Time for loading parser: 0.333s Time for CFA construction: 0.526s Time for parsing file(s): 0.205s Time for AST to CFA: 0.198s Time for CFA sanity check: 0.000s Time for post-processing: 0.093s Time for var class.: 0.000s Time for Analysis: 4.466s CPU time for analysis: 10.650s Total time for CPAchecker: 5.967s Total CPU time for CPAchecker: 12.820s Time for Garbage Collector: 0.040s (in 1 runs) Garbage Collector(s) used: PS MarkSweep, PS Scavenge Used heap memory: 519MB ( 495 MiB) max; 227MB ( 216 MiB) avg; 571MB ( 544 MiB) peak Used non-heap memory: 24MB ( 23 MiB) max; 20MB ( 19 MiB) avg; 25MB ( 23 MiB) peak Used in PS Old Gen pool: 0MB ( 0 MiB) max; 0MB ( 0 MiB) avg; 0MB ( 0 MiB) peak Allocated heap memory: 2024MB ( 1930 MiB) max; 2024MB ( 1930 MiB) avg Allocated non-heap memory: 25MB ( 24 MiB) max; 24MB ( 23 MiB) avg Total process virtual memory: 57123MB ( 54476 MiB) max; 57074MB ( 54430 MiB) avg Verification result: UNKNOWN, incomplete analysis. More details about the verification run can be found in the directory "./output".