/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/in-de51.yml/witness.graphml -stats -spec ../properties/unreach-call.prp -32 ../plain/in-de51.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/in-de51.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/18109d1e-a44d-4ca1-afb7-19298c01e28c.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/75de32ed-1875-4927-b3c3-eee2470e8363.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/4d2ef1fd-4e60-4c16-b069-d8b91a91bdf6.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/be5f7a67-3fad-43f5-b02c-bcf74bca2501.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/6b81f1e1-9041-42b0-b82d-9b3d5b8e36b6.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/1699d6cf-0b9d-45e2-a0b2-57144eff36b1.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/e111451b-fd80-46b6-80e1-6b0134cf58ab.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/db5c9449-b57e-4016-8c81-421519f747a5.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/2c44f2c1-4f0d-440d-973e-a06ebc59fa74.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/84af1ec1-1125-43f5-bcfe-2d600ea8ae6b.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/e161e3f0-d0a9-41fe-8341-e95577a1308b.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/da87c898-e1d6-41ec-ae55-03d4e4b27f28.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/8306ed4a-5795-4137-abc7-5ed51ddb6d5a.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/557ab27e-b0e3-4fbd-af02-0f7c9bca40a1.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/48b7e93a-584b-4822-98e6-bf894c172c46.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/2e23435c-b1d6-499e-b24b-cf7a8e1487b4.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/992af446-7066-4b3f-8078-475783458cb1.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/366a757f-f8d8-4418-9ae3-127ada2e15d6.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/68afa63d-e851-42dc-869f-0bcce043c854.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/989bd820-94d3-471b-8c02-bd076e3a8c9d.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/3e987674-0c3f-4992-8de7-4c8f633fce84.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/ec5d21de-a807-4433-af52-8233570fa3a8.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/b0978dfe-ff1c-48d0-ae16-6b0f6821ed57.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/bcf27631-8899-4ef0-a4c2-8da83bcffd3f.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/36de49f3-b6a3-47e5-8389-571d69abdda8.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/b8dd3351-2a38-49e9-8c35-175ba05b02e7.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/347a5ec5-f036-458a-9d04-c303108f0bc9.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/e06617a8-ed14-45f7-acb2-f75dfbdd1e8a.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/c3e6b982-1977-4646-833a-d9da390a8ed5.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/32046a3c-2407-4b14-9448-681c10ce2fee.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/17c88a86-d82c-41ef-aa99-8b817f325c0e.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: 31, 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:                       76
Number of CFA edges (per node):                          78 (count: 76, min: 0, max: 2, avg: 1.03)
Number of relevant variables:                      7
Number of functions:                               3
Number of loops (and loop nodes):                         5 (sum: 40, min: 8, max: 8, avg: 8.00)
Size of reached set:             1
  Number of reached locations:   1 (1%)
    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.236s
  Time for loading CPAs:          0.827s
  Time for loading parser:        0.326s
  Time for CFA construction:      0.817s
    Time for parsing file(s):     0.434s
    Time for AST to CFA:          0.170s
    Time for CFA sanity check:    0.076s
    Time for post-processing:     0.103s
    Time for CFA export:          0.795s
      Time for function pointers resolving:            0.017s
        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.046s
        Time for collecting variables:                 0.023s
        Time for solving dependencies:                 0.001s
        Time for building hierarchy:                   0.000s
        Time for building classification:              0.018s
        Time for exporting data:                       0.004s
Time for Analysis:                1.293s
CPU time for analysis:            1.300s
Total time for CPAchecker:        3.530s
Total CPU time for CPAchecker:    3.530s
Time for statistics:              0.114s

Time for Garbage Collector:       0.093s (in 7 runs)
Garbage Collector(s) used:    Copy, MarkSweepCompact
Used heap memory:                 51MB (    48 MiB) max;     30MB (    28 MiB) avg;     59MB (    57 MiB) peak
Used non-heap memory:             46MB (    44 MiB) max;     31MB (    29 MiB) avg;     47MB (    45 MiB) peak
Allocated heap memory:            91MB (    87 MiB) max;     91MB (    87 MiB) avg
Allocated non-heap memory:        51MB (    48 MiB) max;     35MB (    34 MiB) avg
Total process virtual memory:  12635MB ( 12049 MiB) max;  12615MB ( 12030 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".
