/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/lu.cmp.yml/witness.graphml -stats -spec ../properties/unreach-call.prp -32 ../plain/lu.cmp.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/lu.cmp.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/1c69e0a7-5e5b-437d-878e-2b15d20a9708.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/d8cdc775-2991-4561-bfba-adc18a3f2c03.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/ee9bffe4-cb65-49e0-b6f2-173c169e1545.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/d4da9cfb-4c53-492d-a062-c34bda5b60f2.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/10ff20a8-4e45-4b9a-8f8e-73d9ddc6b1c2.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/cb88df6b-74fb-470b-b020-19ddc55ad3b7.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/f5f4ed42-5090-4542-8f24-00928a001867.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/aab674ef-e724-4afa-b311-44c869bf7a21.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/78c85f0e-737f-48a5-bde4-d9954d303aef.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/e83528b4-8c59-43fa-84c3-c31c4145fc43.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/21015fed-dd81-4f3e-b557-7179d7db89ea.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/4d8c1591-df91-4268-8e6d-4526927ba0e3.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/db4d143e-860d-4c43-8124-22601100b25a.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/7f51d5dc-52df-467a-bdf6-6e860c72568d.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/19a83ec6-4306-4c45-ac0b-a387f85ab565.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/542bb7c4-6e87-47e6-a27e-e5b4ce26d916.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/eb51799f-ea4a-469c-b575-995d91b74e4c.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/c08c7322-89ef-4d2f-a2f0-400664756ad6.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/b7c8a0cf-e095-4c43-8c68-037d231ad225.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/4bccda65-7950-43c2-9817-fdd828796739.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/a419b85b-a5d4-4101-8d92-0b63e9e7621f.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/bc643724-03f5-4504-89b6-933de910c78c.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/eb29c653-62db-4d14-aaab-28c0cfb7580a.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/188d9bd6-f26a-43e1-9ccb-6f13d873590d.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/1c74a5ff-5428-4c0e-b323-05d9d8895702.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/8e9f6a5e-45ac-42bb-ae39-c98b0041cc56.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/a2e60ce3-ba71-46ec-9e66-deb16a5f99ff.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/9b6bee5c-273c-40e9-8428-a702f615e23b.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/1b5c8214-51c0-4fdf-b3a6-376a7fb126a5.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/010c5c28-a301-42f3-b789-3a4e1be1faa3.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/05fd5446-b1fe-4aaf-b77e-504778d84b52.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/88bcbafe-1d1f-419a-8c85-2d04f89447fe.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/c782bc9c-6afa-4b70-a37e-78041e14c328.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/6c385577-baa6-480b-9fe5-dbcf3d3743ba.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/fb9f3526-a868-4a99-ad69-9d3f67843605.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/2bbaf874-be41-48a9-a8d6-23ce8eddf1d6.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/c95fbb9e-fdc2-4a42-958a-85cb77441c5e.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/0bca9162-4a7d-44c1-9669-bcef7a16694f.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/166671df-df2f-4a14-a8ce-c7d2e7424a82.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/96050dc9-e773-47a3-8a95-1450e38616fe.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/2465b36a-96fe-42f8-b42a-4f6372f8ffc5.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/ac28e0af-7648-4111-8cce-ea418e847f89.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/edf2fabd-94b9-4ee6-b567-ff9c67b6f690.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/b9873f8a-78d6-44ea-b9e9-f3e951504ed8.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/af67cb95-4e0a-4cee-8036-a88b2bcd7fe7.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/e8c5cf1a-f8de-4145-86bb-3f668f8ed11a.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/1b6dc8a8-cb5c-44cc-b04f-8316ea73bced.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/3ed64919-82c6-4599-9edb-3d8f19b3becb.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/dae79c39-1be6-476e-8ce4-5c48817bf04a.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/4e23ca76-b386-4458-825b-e57f384ed439.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/a3a0cb11-8a9e-4d24-83d1-506d458dc870.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/bcd11bfe-2e2e-4815-8e77-90b49134b326.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/c8fbd29a-3f78-4d2f-a338-69549fb3876d.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/7d805982-0ffa-4d9a-93a8-e60b870c0da7.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/9d4471c4-3dd9-4a76-b669-ce12e9c1a905.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/4fba8117-2dcc-49c4-83d2-7f9d98759c95.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/57fd6b2a-1f09-458f-9e99-09df01f6a504.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/27d4de16-0585-4163-92f8-475897129fb6.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/def379dd-e192-490b-bccc-efe1668f8dfe.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/2e830b0c-3b20-4cb2-8b1f-bb902c88e82c.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/dfec665d-96c0-4044-8323-0cfb1b523233.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/48aa1ce8-228c-481b-9f6f-923f83683a80.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/c635c159-6e40-44cf-9657-d31293b8ad01.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/3bfbf0b0-b5d5-4246-959f-6ff45f443505.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/5697c932-8e5f-453c-a105-6aa0fca02b4b.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/35a52863-c369-467b-b7e2-ae5258803e9e.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/efb893e0-da32-498d-a156-76915308d14c.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/4c006001-a8bd-4951-838e-f796b442cc9e.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/17a3c9b7-e4a8-490a-8cae-ddb194894a4b.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/6da8df88-d178-460c-8d3c-9096348e774e.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/500c8417-02e4-4c04-99d2-80b640a7ccc2.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/231e94c2-cb8b-4273-a8e9-3717839d1671.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/a07c9ea0-f404-4022-a91e-84f1cf44e946.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/f757751b-d060-4c7a-b744-4578ad5ed9f2.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/9b9dcb2b-a1bb-4851-9482-cc8e30ce1ef8.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/91e3a6d3-9161-439e-9f71-6cf6dc2d35c8.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/74853c8a-5612-4db1-84c0-b7e000688bf7.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/64f3aafc-c455-4a37-8e17-8f018d9fbe9f.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/a3746eba-8e46-47c6-b0c9-31a95cd905ea.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/02124598-17d5-4cb5-8a39-0acbcf18fed6.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/673244fb-c422-40f5-9a68-53ce7df15432.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/008f54a0-777e-40a6-99f5-08d21ef9e444.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/666f061e-e0fb-456f-a962-536bcfa63be7.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/4e42ce4c-250e-476c-bd0c-9fc4e8e35e0c.invariantwitness.yaml (InvariantWitnessWriter.exportInvariantWitness, INFO)

Exporting invariant ./output/invariantWitnesses/b5ca244e-1ea8-40ac-a567-e312d2f3cb8d.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: 67, 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:                       140
Number of CFA edges (per node):                         156 (count: 140, min: 0, max: 2, avg: 1.11)
Number of relevant variables:                      23
Number of functions:                               5
Number of loops (and loop nodes):                        11 (sum: 120, min: 4, max: 34, avg: 10.91)
Size of reached set:             1
  Number of reached locations:   1 (1%)
    Avg states per location:     1
    Max states per location:     1 (at node N24)
  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.433s
  Time for loading CPAs:          0.907s
  Time for loading parser:        0.326s
  Time for CFA construction:      0.932s
    Time for parsing file(s):     0.438s
    Time for AST to CFA:          0.266s
    Time for CFA sanity check:    0.049s
    Time for post-processing:     0.147s
    Time for CFA export:          0.867s
      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.078s
        Time for collecting variables:                 0.036s
        Time for solving dependencies:                 0.002s
        Time for building hierarchy:                   0.000s
        Time for building classification:              0.030s
        Time for exporting data:                       0.007s
Time for Analysis:                3.240s
CPU time for analysis:            3.240s
Total time for CPAchecker:        5.687s
Total CPU time for CPAchecker:    5.680s
Time for statistics:              0.107s

Time for Garbage Collector:       0.178s (in 13 runs)
Garbage Collector(s) used:    Copy, MarkSweepCompact
Used heap memory:                 82MB (    78 MiB) max;     41MB (    39 MiB) avg;     86MB (    82 MiB) peak
Used non-heap memory:             51MB (    49 MiB) max;     37MB (    35 MiB) avg;     52MB (    50 MiB) peak
Allocated heap memory:            91MB (    87 MiB) max;     91MB (    87 MiB) avg
Allocated non-heap memory:        55MB (    52 MiB) max;     41MB (    39 MiB) avg
Total process virtual memory:  12638MB ( 12052 MiB) max;  12624MB ( 12039 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".
