/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../CPAchecker-2.2-unix/scripts/cpa.sh -heap 10000M -timelimit 900s -witness2invariant -skipRecursion -setprop invariantStore.witness=/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self/ourtool.2023-02-03_08-10-40.files/ourtool/nested3-1.yml/witness.graphml -stats -spec ../properties/unreach-call.prp -32 ../plain/nested3-1.c


--------------------------------------------------------------------------------


Running CPAchecker with Java heap of size 10000M.
Running CPAchecker with default stack size (1024k). Specify a larger value with -stack if needed.
Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)

Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 2.2 / witness2invariant (OpenJDK 64-Bit Server VM 11.0.17) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "../plain/nested3-1.c" (CPAchecker.parse, INFO)

Using predicate analysis with MathSAT5 version 5.6.8 (27814677e16f) (Jun 28 2022 17:03:19, gmp 6.1.2, gcc 6.3.0, 64-bit, reentrant) and JFactory 1.21. (PredicateCPA:PredicateCPA.<init>, INFO)

The following configuration options were specified but are not used:
 witness.noViolationValidation 
 (CPAchecker.printConfigurationWarnings, WARNING)

Starting analysis ... (CPAchecker.runAlgorithm, INFO)

Exporting invariant ./output/invariantWitnesses/d9f2b699-2032-4ed4-be09-1232170c4d76.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/d327033c-0a05-4710-bdff-69d76fcdddef.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/fce8fade-75c9-4551-ba37-4f1a87def8a7.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/4d521d1c-a07e-4d4f-a084-c2b66b2ba97e.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/23ca01f9-14a9-4f0d-8b76-6277abf1b425.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/5645a7b8-356b-4fca-b502-cfbad15c78b2.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/ac9cd32e-33f4-4549-81e9-1483d9f8463b.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/db564442-e4a9-403c-9ccc-9f8dde3f5ac9.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/13eb50b8-3db7-4cd2-9995-0fd765bd1d82.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/38556ee4-9cdc-48af-88e4-3b47c889836f.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/2afd9d01-c372-4230-afa9-2c55ce7376bc.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/d39da152-dd26-4f6b-bd5b-0e94582bce64.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/3d9a4ae9-6b11-478f-8537-f8480cb06026.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/912ee925-7435-472d-b2e8-8dc815201931.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/c8007164-03f8-4fd2-8d12-aa54dee71719.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/82cf5cf2-9d81-492a-b370-4b00bd09ece0.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/d753d848-a30f-4d41-8b7e-d4c46bb3d235.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/f5d0a722-cd8c-492e-af62-8b9db1125de6.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/c4fd7a24-816f-4575-b69a-556d0a078cd8.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/d5262f9b-fb81-497c-bb92-2f72992f94f2.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/a6c76c42-81dc-4635-af93-ffb2d1e08b44.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/7ca9e485-8107-433f-9406-517707521a48.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/e2050971-c8ff-44ef-975c-0355a557404a.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/51fa8f61-f4fe-495c-9ed1-d9d6050170e8.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Stopping analysis ... (CPAchecker.runAlgorithm, INFO)


PredicateCPA statistics
-----------------------
Number of abstractions:            0 (NaN% of all post computations)
Number of strengthen sat checks:   0
Number of coverage checks:         0
  BDD entailment checks:           0
Number of SMT sat checks:          0
  trivial:                         0
  cached:                          0

Max ABE block size:                       0
Avg ABE block size:                                0.00 (sum: 0, count: 0, min: 0, max: 0)
Number of predicates discovered:          0

Time for post operator:                                0.000s
  Time for path formula creation:                      0.000s
Time for strengthen operator:                          0.000s
Time for prec operator:                                0.000s
Time for coverage checks:                              0.000s
Total time for SMT solver (w/o itp):     0.000s

Number of path formula cache hits:   0 (NaN%)

Inside post operator:                  
  Inside path formula creation:        
    Time for path formula computation:     0.000s

Total number of created targets for pointer analysis: 0


Number of BDD nodes:                               202
Size of BDD node table:                            506837
Size of BDD node cleanup queue:                    0.00 (sum: 0, count: 19, min: 0, max: 0)
Time for BDD node cleanup:                             0.000s
Time for BDD garbage collection:                       0.000s (in 0 runs)

KeyValue statistics
-------------------
Init. function predicates:                         0
Init. global predicates:                           0
Init. location predicates:                         0

Invariant Generation statistics
-------------------------------

AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states:                                  1
Total time for successor computation:                  0.000s
Automaton transfers with branching:                0
Automaton transfer successors:                     0.00 (sum: 0, count: 0, min: 0, max: 0) []
Number of states with assumption transitions:      0

CPAchecker general statistics
-----------------------------
Number of program locations:                       50
Number of CFA edges (per node):                          54 (count: 50, min: 0, max: 3, avg: 1.08)
Number of relevant variables:                      6
Number of functions:                               3
Number of loops (and loop nodes):                         3 (sum: 39, min: 5, max: 21, avg: 13.00)
Size of reached set:             1
  Number of reached locations:   1 (2%)
    Avg states per location:     1
    Max states per location:     1 (at node N14)
  Number of reached functions:   1 (33%)
  Number of partitions:          1
    Avg size of partitions:      1
    Max size of partitions:      1
  Number of target states:       0
  Size of final wait list:       1

Time for analysis setup:          2.315s
  Time for loading CPAs:          0.873s
  Time for loading parser:        0.359s
  Time for CFA construction:      0.803s
    Time for parsing file(s):     0.445s
    Time for AST to CFA:          0.127s
    Time for CFA sanity check:    0.071s
    Time for post-processing:     0.124s
    Time for CFA export:          0.793s
      Time for function pointers resolving:            0.003s
        Function calls via function pointers:             0 (count: 1, min: 0, max: 0, avg: 0.00)
        Instrumented function pointer calls:              0 (count: 1, min: 0, max: 0, avg: 0.00)
        Function calls with function pointer arguments:        0 (count: 1, min: 0, max: 0, avg: 0.00)
        Instrumented function pointer arguments:          0 (count: 1, min: 0, max: 0, avg: 0.00)
      Time for classifying variables:                  0.043s
        Time for collecting variables:                 0.011s
        Time for solving dependencies:                 0.000s
        Time for building hierarchy:                   0.000s
        Time for building classification:              0.027s
        Time for exporting data:                       0.005s
Time for Analysis:                1.317s
CPU time for analysis:            1.320s
Total time for CPAchecker:        3.633s
Total CPU time for CPAchecker:    3.630s
Time for statistics:              0.107s

Time for Garbage Collector:       0.077s (in 7 runs)
Garbage Collector(s) used:    Copy, MarkSweepCompact
Used heap memory:                 50MB (    48 MiB) max;     29MB (    28 MiB) avg;     57MB (    54 MiB) peak
Used non-heap memory:             47MB (    45 MiB) max;     31MB (    30 MiB) avg;     48MB (    46 MiB) peak
Allocated heap memory:            91MB (    87 MiB) max;     91MB (    87 MiB) avg
Allocated non-heap memory:        51MB (    49 MiB) max;     35MB (    34 MiB) avg
Total process virtual memory:  12634MB ( 12048 MiB) max;  12615MB ( 12031 MiB) avg

Finished.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Report.html".
