scripts/cpa.sh -heap 50000M -noout -disable-java-assertions -predicateAnalysis-PredAbsRefiner-ABEl -timelimit 900s -stats -spec test/programs/benchmarks/bitvector-regression/ALL.prp test/programs/benchmarks/bitvector-regression/signextension2_true-unreach-call.i -------------------------------------------------------------------------------- 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) Stopping analysis ... (CPAchecker.runAlgorithm, INFO) Analysis incomplete: no errors found, but not everything could be checked. (CPAchecker.analyzeResult, WARNING) PredicateCPA statistics ----------------------- Number of abstractions: 0 (0% of all post computations) Number of strengthen sat checks: 1 Times result was 'false': 0 (0%) Number of coverage checks: 6 BDD entailment checks: 0 Number of SMT sat checks: 1 trivial: 0 cached: 0 Max ABE block size: 0 Number of predicates discovered: 0 Number of path formula cache hits: 1 (0%) Time for post operator: 0.040s Time for path formula creation: 0.040s Actual computation: 0.048s Time for strengthen operator: 0.034s Time for satisfiability checks: 0.034s Time for prec operator: 0.000s Time for merge operator: 0.001s Time for coverage check: 0.000s Total time for SMT solver (w/o itp): 0.034s Number of BDD nodes: 202 Size of BDD node table: 10007 Size of BDD node cleanup queue: 0 (count: 2, 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.004s Automaton transfers with branching: 0 Automaton transfer successors: 215 (count: 215, min: 1, max: 1, avg: 1,00) [1 x 215] CPA algorithm statistics ------------------------ Number of iterations: 13 Max size of waitlist: 2 Average size of waitlist: 1 Number of computed successors: 16 Max successors for one state: 2 Number of times merged: 3 Number of times stopped: 3 Number of times breaked: 1 Total time for CPA algorithm: 0.096s (Max: 0.096s) Time for choose from waitlist: 0.001s Time for precision adjustment: 0.004s Time for transfer relation: 0.087s Time for merge operator: 0.002s Time for stop operator: 0.000s Time for adding to reached set: 0.001s Predicate-Abstraction Refiner statistics ---------------------------------------- Avg. length of target path (in blocks): 1 (count: 1, min: 1, max: 1, avg: 1,00) Time for refinement: 0.095s Counterexample analysis: 0.033s (Max: 0.033s, Calls: 1) Refinement sat check: 0.009s Interpolant computation: 0.000s Error path post-processing: 0.059s Path-formulas extraction: 0.000s Building the counterexample trace: 0.033s Extracting precise counterexample: 0.059s Predicate creation: 0.000s Precision update: 0.000s ARG update: 0.000s Length of refined path (in blocks): 0 (count: 0, min: 0, max: 0, avg: 0,00) Number of affected states: 0 (count: 0, min: 0, max: 0, avg: 0,00) Length (states) of path with itp 'true': 0 (count: 0, min: 0, max: 0, avg: 0,00) Length (states) of path with itp non-trivial itp: 0 (count: 0, min: 0, max: 0, avg: 0,00) Length (states) of path with itp 'false': 0 (count: 0, min: 0, max: 0, avg: 0,00) Different non-trivial interpolants along paths: 0 (count: 0, min: 0, max: 0, avg: 0,00) Equal non-trivial interpolants along paths: 0 (count: 0, 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: 1 Number of successful refinements: 0 Number of failed refinements: 0 Max. size of reached set before ref.: 14 Max. size of reached set after ref.: 0 Avg. size of reached set before ref.: 14.00 Avg. size of reached set after ref.: NaN Total time for CEGAR algorithm: 0.198s Time for refinements: 0.102s Average time for refinement: 0.102s Max time for refinement: 0.102s Counterexample-Check Algorithm statistics ----------------------------------------- Number of counterexample checks: 1 Number of infeasible paths: 1 (100%) Time for counterexample checks: 0.165s CPAchecker general statistics ----------------------------- Number of program locations: 14 Number of functions: 1 Number of loops: 0 Size of reached set: 12 Number of reached locations: 12 (86%) Avg states per location: 1 Max states per location: 1 (at node N0) Number of reached functions: 1 (100%) Number of partitions: 12 Avg size of partitions: 1 Max size of partitions: 1 Number of target states: 0 Time for analysis setup: 1.557s Time for loading CPAs: 0.559s Time for loading parser: 0.333s Time for CFA construction: 0.576s Time for parsing file(s): 0.248s Time for AST to CFA: 0.207s Time for CFA sanity check: 0.000s Time for post-processing: 0.076s Time for var class.: 0.000s Time for Analysis: 0.364s CPU time for analysis: 0.420s Total time for CPAchecker: 1.923s Total CPU time for CPAchecker: 2.720s Time for Garbage Collector: 0.000s (in 0 runs) Garbage Collector(s) used: PS MarkSweep, PS Scavenge Used heap memory: 169MB ( 161 MiB) max; 113MB ( 107 MiB) avg; 169MB ( 161 MiB) peak Used non-heap memory: 21MB ( 20 MiB) max; 15MB ( 14 MiB) avg; 21MB ( 20 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: 24MB ( 23 MiB) max; 24MB ( 23 MiB) avg Total process virtual memory: 57123MB ( 54476 MiB) max; 57061MB ( 54418 MiB) avg Verification result: UNKNOWN, incomplete analysis. More details about the verification run can be found in the directory "./output".