/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-self2/ourtool.2023-02-15_09-12-33.files/ourtool/trex04.yml/witness.graphml -stats -spec ../properties/unreach-call.prp -32 ../plain/trex04.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/trex04.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/243606c1-520a-4430-9218-faa567cc840c.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/f98de21b-3ea8-4c8a-8008-d2ce19c4c731.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/07973aa0-3af9-47e6-88a4-ccf8d11e6ae1.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/26e8479c-27ca-43a5-9b22-d44b35d382fd.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/e1c4cd21-6d1a-4b4b-8aee-a8ca8e8d8e97.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/4aaa7bda-6947-4be0-8aac-d335a2bd764d.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/ca713bab-2082-4b36-956f-a8a4b5d80b6c.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/ff34400d-a94f-4942-b1e1-0fbe9884fdb1.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/9de458a1-8753-40f2-af8b-237cb900a82e.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/473387ac-de96-47c1-8e84-47e3d7e69de9.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/e5f7cea0-52a0-4ab0-a9d5-cdb7576a68af.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/66ae6638-6e99-405a-8b19-aede21a6d39a.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/5b83e06e-d61f-4281-afdd-9819832564fb.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/e5a82fa1-a2bf-48f1-93ef-207d7703d573.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/e67bbe58-e967-4c74-b3ef-0ccc1c069356.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/56a04ee1-62a6-4a0f-b39f-c00af738a077.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/88f97322-bab1-4823-a7b8-295b95a8ac11.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/e243df28-992e-481f-bb19-75784d973a0f.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/57953853-83ac-4db5-827e-c0355fba7af7.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/15b8bfa5-0db2-4c60-94a8-770bbe6ce3bd.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/c1e77716-6332-4730-acc5-b9064218c221.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/0df88e88-6144-452f-af77-91e9404376b6.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/c410aee9-12ca-4a3f-9914-15f5c69f2266.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/32d3a621-e671-4494-b9b1-9d6dcfd67c7a.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/0ebaeaba-fec9-4e27-a339-58da220cc59c.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/3a8ae6b3-734a-49ba-b03d-d3f74b7b73d1.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/c5eaa5f7-ff0c-461a-afa4-0e439d0e7b03.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/cb7a594a-a1e9-416f-8a01-e5a307a9c3cb.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/679287d4-5956-4900-8ac3-d97a737ef2f6.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/90d24814-a9ba-4f91-8ba9-a82cf9a2e66e.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/6084023e-1122-4193-99be-12b303a3e16b.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/d0dc3bf5-4afd-41c8-a7ac-ea332b934fcd.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: 7, 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:                       83
Number of CFA edges (per node):                          90 (count: 83, min: 0, max: 2, avg: 1.08)
Number of relevant variables:                      11
Number of functions:                               5
Number of loops (and loop nodes):                         1 (sum: 3, min: 3, max: 3, avg: 3.00)
Size of reached set:             1
  Number of reached locations:   1 (1%)
    Avg states per location:     1
    Max states per location:     1 (at node N40)
  Number of reached functions:   1 (20%)
  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.256s
  Time for loading CPAs:          0.845s
  Time for loading parser:        0.326s
  Time for CFA construction:      0.817s
    Time for parsing file(s):     0.413s
    Time for AST to CFA:          0.195s
    Time for CFA sanity check:    0.054s
    Time for post-processing:     0.096s
    Time for CFA export:          0.789s
      Time for function pointers resolving:            0.002s
        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.041s
        Time for collecting variables:                 0.018s
        Time for solving dependencies:                 0.000s
        Time for building hierarchy:                   0.000s
        Time for building classification:              0.020s
        Time for exporting data:                       0.003s
Time for Analysis:                1.697s
CPU time for analysis:            1.700s
Total time for CPAchecker:        3.955s
Total CPU time for CPAchecker:    3.960s
Time for statistics:              0.087s

Time for Garbage Collector:       0.101s (in 7 runs)
Garbage Collector(s) used:    Copy, MarkSweepCompact
Used heap memory:                 58MB (    55 MiB) max;     32MB (    30 MiB) avg;     63MB (    60 MiB) peak
Used non-heap memory:             49MB (    46 MiB) max;     33MB (    31 MiB) avg;     50MB (    48 MiB) peak
Allocated heap memory:            91MB (    87 MiB) max;     91MB (    87 MiB) avg
Allocated non-heap memory:        53MB (    50 MiB) max;     37MB (    35 MiB) avg
Total process virtual memory:  12635MB ( 12049 MiB) max;  12617MB ( 12032 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".
