/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self2/ourtool.2023-02-15_09-12-33.files/ourtool/hard-ll.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self2/ourtool.2023-02-15_09-12-33.files/ourtool/hard-ll.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/hard-ll.c


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Witness] couldn't locate invariant: 0LL <= q (../plain/hard-ll.c:45:9)
[Warning][Witness] couldn't locate invariant: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:45:9)
[Warning][Witness] couldn't locate invariant: 0LL <= d (../plain/hard-ll.c:46:9)
[Warning][Witness] couldn't locate invariant: 1LL <= p (../plain/hard-ll.c:46:9)
[Warning][Witness] couldn't locate invariant: d <= 8589934590LL (../plain/hard-ll.c:46:9)
[Warning][Witness] couldn't locate invariant: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:46:9)
[Warning][Witness] couldn't locate invariant: 1LL <= p (../plain/hard-ll.c:48:13)
[Warning][Witness] couldn't locate invariant: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:48:13)
[Warning][Witness] couldn't locate invariant: 0LL <= d (../plain/hard-ll.c:50:9)
[Warning][Witness] couldn't locate invariant: d <= 8589934590LL (../plain/hard-ll.c:50:9)
[Warning][Witness] couldn't locate invariant: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:50:9)
[Warning][Witness] couldn't locate invariant: 0LL <= d (../plain/hard-ll.c:51:9)
[Warning][Witness] couldn't locate invariant: 2LL <= p (../plain/hard-ll.c:51:9)
[Warning][Witness] couldn't locate invariant: d <= 4294967295LL (../plain/hard-ll.c:51:9)
[Warning][Witness] couldn't locate invariant: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:51:9)
[Warning][Witness] couldn't locate invariant: p != 0LL (../plain/hard-ll.c:51:9)
[Warning][Witness] couldn't locate invariant: p != 1LL (../plain/hard-ll.c:51:9)
[Warning][Witness] couldn't locate invariant: 0LL <= d (../plain/hard-ll.c:52:13)
[Warning][Witness] couldn't locate invariant: 0LL <= q (../plain/hard-ll.c:52:13)
[Warning][Witness] couldn't locate invariant: 1LL <= p (../plain/hard-ll.c:52:13)
[Warning][Witness] couldn't locate invariant: d <= 4294967295LL (../plain/hard-ll.c:52:13)
[Warning][Witness] couldn't locate invariant: p <= 4611686018427387903LL (../plain/hard-ll.c:52:13)
[Warning][Witness] couldn't locate invariant: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:52:13)
[Warning][Witness] couldn't locate invariant: 0LL <= r (../plain/hard-ll.c:53:13)
[Warning][Witness] couldn't locate invariant: 0LL <= d (../plain/hard-ll.c:53:13)
[Warning][Witness] couldn't locate invariant: d <= 4294967295LL (../plain/hard-ll.c:53:13)
[Warning][Witness] couldn't locate invariant: (0LL - d) + r >= 0LL (../plain/hard-ll.c:53:13)
[Warning][Witness] couldn't locate invariant: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:53:13)
[Warning][Witness] couldn't locate invariant: -4294967295LL <= r (../plain/hard-ll.c:54:13)
[Warning][Witness] couldn't locate invariant: 0LL <= d (../plain/hard-ll.c:54:13)
[Warning][Witness] couldn't locate invariant: 0LL <= q (../plain/hard-ll.c:54:13)
[Warning][Witness] couldn't locate invariant: 1LL <= p (../plain/hard-ll.c:54:13)
[Warning][Witness] couldn't locate invariant: d <= 4294967295LL (../plain/hard-ll.c:54:13)
[Warning][Witness] couldn't locate invariant: p <= 4611686018427387903LL (../plain/hard-ll.c:54:13)
[Warning][Witness] couldn't locate invariant: r >= 0LL (../plain/hard-ll.c:54:13)
[Warning][Witness] couldn't locate invariant: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:54:13)
[Warning][Witness] couldn't locate invariant: 0LL <= d (../plain/hard-ll.c:58:5)
[Warning][Witness] couldn't locate invariant: 0LL <= q (../plain/hard-ll.c:58:5)
[Warning][Witness] couldn't locate invariant: d <= 8589934590LL (../plain/hard-ll.c:58:5)
[Warning][Witness] couldn't locate invariant: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:58:5)
[Warning][Witness] couldn't locate invariant: 0LL <= d (../plain/hard-ll.c:59:5)
[Warning][Witness] couldn't locate invariant: d <= 8589934590LL (../plain/hard-ll.c:59:5)
[Warning][Witness] couldn't locate invariant: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:59:5)
[Warning][Witness] couldn't locate invariant: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:60:5)

runtime: 00:00:10.149
vars: 71, evals: 2738

|rho|=71
|called|=11
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=2969.80MB, max=14.22MB, minor=2966.13MB, major=131.53MB, promoted=127.86MB
    minor collections=1430  major collections=32 compactions=0


runtime: 00:00:20.190
vars: 71, evals: 3595

|rho|=71
|called|=10
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=3911.35MB, max=14.22MB, minor=3907.65MB, major=170.33MB, promoted=166.63MB
    minor collections=1883  major collections=41 compactions=0


runtime: 00:00:30.208
vars: 71, evals: 4125

|rho|=71
|called|=10
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=4491.98MB, max=16.36MB, minor=4488.25MB, major=194.25MB, promoted=190.53MB
    minor collections=2163  major collections=47 compactions=0


runtime: 00:00:40.232
vars: 71, evals: 4505

|rho|=71
|called|=4
|stable|=70
|infl|=69
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=4920.41MB, max=16.36MB, minor=4916.67MB, major=211.90MB, promoted=208.17MB
    minor collections=2369  major collections=50 compactions=0


runtime: 00:00:50.270
vars: 71, evals: 4823

|rho|=71
|called|=10
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=5262.36MB, max=16.36MB, minor=5258.61MB, major=225.91MB, promoted=222.16MB
    minor collections=2533  major collections=53 compactions=0


runtime: 00:01:00.227
vars: 71, evals: 5079

|rho|=71
|called|=5
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=5544.31MB, max=16.36MB, minor=5540.55MB, major=237.53MB, promoted=233.77MB
    minor collections=2669  major collections=56 compactions=0


runtime: 00:01:10.253
vars: 71, evals: 5300

|rho|=71
|called|=10
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=5786.41MB, max=16.36MB, minor=5782.65MB, major=247.51MB, promoted=243.74MB
    minor collections=2786  major collections=58 compactions=0


runtime: 00:01:20.242
vars: 71, evals: 5503

|rho|=71
|called|=10
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=6006.17MB, max=16.36MB, minor=6002.40MB, major=256.50MB, promoted=252.72MB
    minor collections=2891  major collections=60 compactions=0


runtime: 00:01:30.285
vars: 71, evals: 5671

|rho|=71
|called|=5
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=6198.59MB, max=16.36MB, minor=6194.81MB, major=264.44MB, promoted=260.66MB
    minor collections=2984  major collections=61 compactions=0


runtime: 00:01:40.361
vars: 71, evals: 5830

|rho|=71
|called|=4
|stable|=70
|infl|=69
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=6378.03MB, max=16.36MB, minor=6374.24MB, major=271.74MB, promoted=267.96MB
    minor collections=3070  major collections=63 compactions=0


runtime: 00:01:50.287
vars: 71, evals: 5980

|rho|=71
|called|=9
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=6532.10MB, max=16.36MB, minor=6528.31MB, major=278.00MB, promoted=274.21MB
    minor collections=3144  major collections=64 compactions=0


runtime: 00:02:00.289
vars: 71, evals: 6110

|rho|=71
|called|=6
|stable|=71
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=6678.31MB, max=16.36MB, minor=6674.51MB, major=284.02MB, promoted=280.22MB
    minor collections=3214  major collections=65 compactions=0


runtime: 00:02:10.306
vars: 71, evals: 6245

|rho|=71
|called|=10
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=6824.08MB, max=16.36MB, minor=6820.28MB, major=290.01MB, promoted=286.21MB
    minor collections=3285  major collections=67 compactions=0


runtime: 00:02:20.401
vars: 71, evals: 6360

|rho|=71
|called|=10
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=6954.26MB, max=16.36MB, minor=6950.46MB, major=295.37MB, promoted=291.57MB
    minor collections=3347  major collections=68 compactions=0


runtime: 00:02:30.448
vars: 71, evals: 6466

|rho|=71
|called|=4
|stable|=70
|infl|=69
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=7079.46MB, max=16.36MB, minor=7075.66MB, major=300.53MB, promoted=296.72MB
    minor collections=3408  major collections=69 compactions=0


runtime: 00:02:40.374
vars: 71, evals: 6572

|rho|=71
|called|=6
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=7189.28MB, max=16.36MB, minor=7185.46MB, major=304.95MB, promoted=301.14MB
    minor collections=3460  major collections=70 compactions=0


runtime: 00:02:50.343
vars: 71, evals: 6678

|rho|=71
|called|=11
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=7304.58MB, max=16.36MB, minor=7300.77MB, major=309.75MB, promoted=305.94MB
    minor collections=3516  major collections=71 compactions=0


runtime: 00:03:00.538
vars: 71, evals: 6775

|rho|=71
|called|=10
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=7408.79MB, max=16.36MB, minor=7404.97MB, major=313.94MB, promoted=310.12MB
    minor collections=3566  major collections=71 compactions=0


runtime: 00:03:10.408
vars: 71, evals: 6852

|rho|=71
|called|=6
|stable|=71
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=7496.68MB, max=16.36MB, minor=7492.86MB, major=317.52MB, promoted=313.70MB
    minor collections=3608  major collections=72 compactions=0


runtime: 00:03:20.362
vars: 71, evals: 7026

|rho|=71
|called|=11
|stable|=69
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=7647.28MB, max=16.36MB, minor=7643.45MB, major=323.21MB, promoted=319.38MB
    minor collections=3680  major collections=73 compactions=0


runtime: 00:03:30.387
vars: 71, evals: 7332

|rho|=71
|called|=10
|stable|=70
|infl|=69
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=53
Found 9 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll.c:14:1-20:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
2	contexts for entry state of reach_error (1999) on ../plain/hard-ll.c:8:1-8:73
1	contexts for entry state of main (2012) on ../plain/hard-ll.c:22:1-61:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll.c:11:1-13:1

Memory statistics: total=7907.70MB, max=16.36MB, minor=7903.85MB, major=332.80MB, promoted=328.94MB
    minor collections=3806  major collections=75 compactions=0

[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((4294967295LL + (long long )A) - d >= 0LL && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && r <= 4294967295LL) && 1LL <= p) && 0LL <= d) && 0LL <= r) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 4294967295LL) && 0LL <= d) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL) && r <= 4294967295LL) && 0LL <= r) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:32:5-32:10)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/hard-ll.c:37:9-37:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/hard-ll.c:41:9-41:18)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((4294967295LL + (long long )A) - d >= 0LL && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && r <= 4294967295LL) && 1LL <= p) && 0LL <= d) && 0LL <= r) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 4294967295LL) && 0LL <= d) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL) && r <= 4294967295LL) && 0LL <= r) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL) && (long long )B >= 0LL) && (long long )A >= 0LL) && 4294967295LL - (long long )B >= 0LL) && 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:41:9-41:18)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((((4294967295LL - (long long )A >= 0LL && d <= 8589934590LL) && 1LL <= p) && 0LL <= q) && 0LL <= d) && 2LL * (long long )A - d >= 0LL) && (8589934590LL + 4LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && 1LL <= p) && 0LL <= d) && (long long )A - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 4294967295LL) && 0LL <= d) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && r <= 4294967295LL) && 1LL <= p) && 0LL <= d) && 0LL <= r) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && 1LL <= p) && 0LL <= d) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && r <= 4294967295LL) && 0LL <= r) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:34:12-34:13)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((((4294967295LL - (long long )A >= 0LL && d <= 8589934590LL) && 1LL <= p) && 0LL <= q) && 0LL <= d) && 2LL * (long long )A - d >= 0LL) && (8589934590LL + 4LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && 1LL <= p) && 0LL <= d) && (long long )A - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 4294967295LL) && 0LL <= d) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && r <= 4294967295LL) && 1LL <= p) && 0LL <= d) && 0LL <= r) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && 1LL <= p) && 0LL <= d) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && r <= 4294967295LL) && 0LL <= r) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:38:13-38:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/hard-ll.c:45:9-45:40)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/hard-ll.c:46:9-46:36)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/hard-ll.c:54:13-54:22)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((((4294967295LL - (long long )A >= 0LL && d <= 8589934590LL) && 1LL <= p) && 0LL <= q) && 0LL <= d) && 2LL * (long long )A - d >= 0LL) && (8589934590LL + 4LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && 1LL <= p) && 0LL <= d) && (long long )A - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 4294967295LL) && 0LL <= d) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && r <= 4294967295LL) && 1LL <= p) && 0LL <= d) && 0LL <= r) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && 1LL <= p) && 0LL <= d) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && r <= 4294967295LL) && 0LL <= r) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:54:13-54:22)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((((4294967295LL - (long long )A >= 0LL && d <= 8589934590LL) && 1LL <= p) && 0LL <= q) && 0LL <= d) && 2LL * (long long )A - d >= 0LL) && (8589934590LL + 4LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && 1LL <= p) && 0LL <= d) && (long long )A - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 4294967295LL) && 0LL <= d) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && r <= 4294967295LL) && 1LL <= p) && 0LL <= d) && 0LL <= r) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && d <= 8589934590LL) && 1LL <= p) && 0LL <= d) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL) && r <= 4294967295LL) && 0LL <= r) && (4294967295LL + (long long )A) - d >= 0LL) && (4294967295LL + 2LL * (long long )A) - d >= 0LL) && 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:52:13-52:19)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/hard-ll.c:58:5-58:36)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 36
  dead: 0
  total lines: 36
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/hard-ll.c:44:12-44:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/hard-ll.c:34:12-34:13)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:35:9)
[Warning][Witness] invariant unconfirmed: (4294967295LL + 2LL * (long long )A) - d >= 0LL (../plain/hard-ll.c:35:9)
[Warning][Witness] invariant unconfirmed: (4294967295LL + (long long )A) - d >= 0LL (../plain/hard-ll.c:35:9)
[Warning][Witness] invariant unconfirmed: 0LL <= r (../plain/hard-ll.c:36:9)
[Success][Witness] invariant confirmed: r <= 4294967295LL (../plain/hard-ll.c:36:9)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:36:9)
[Warning][Witness] invariant unconfirmed: (4294967295LL + 2LL * (long long )A) - d >= 0LL (../plain/hard-ll.c:36:9)
[Warning][Witness] invariant unconfirmed: (4294967295LL + (long long )A) - d >= 0LL (../plain/hard-ll.c:36:9)
[Success][Witness] invariant confirmed: 0LL <= d (../plain/hard-ll.c:37:9)
[Success][Witness] invariant confirmed: 1LL <= p (../plain/hard-ll.c:37:9)
[Success][Witness] invariant confirmed: d <= 8589934590LL (../plain/hard-ll.c:37:9)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:37:9)
[Warning][Witness] invariant unconfirmed: (4294967295LL + 2LL * (long long )A) - d >= 0LL (../plain/hard-ll.c:37:9)
[Warning][Witness] invariant unconfirmed: (4294967295LL + (long long )A) - d >= 0LL (../plain/hard-ll.c:37:9)
[Warning][Witness] invariant unconfirmed: 0LL <= r (../plain/hard-ll.c:38:13)
[Success][Witness] invariant confirmed: 0LL <= d (../plain/hard-ll.c:38:13)
[Success][Witness] invariant confirmed: 1LL <= p (../plain/hard-ll.c:38:13)
[Success][Witness] invariant confirmed: r <= 4294967295LL (../plain/hard-ll.c:38:13)
[Success][Witness] invariant confirmed: d <= 8589934590LL (../plain/hard-ll.c:38:13)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:38:13)
[Warning][Witness] invariant unconfirmed: (4294967295LL + 2LL * (long long )A) - d >= 0LL (../plain/hard-ll.c:38:13)
[Warning][Witness] invariant unconfirmed: (4294967295LL + (long long )A) - d >= 0LL (../plain/hard-ll.c:38:13)
[Success][Witness] invariant confirmed: 0LL <= d (../plain/hard-ll.c:40:9)
[Warning][Witness] invariant unconfirmed: d <= 4294967295LL (../plain/hard-ll.c:40:9)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:40:9)
[Warning][Witness] invariant unconfirmed: (4294967295LL + 2LL * (long long )A) - d >= 0LL (../plain/hard-ll.c:40:9)
[Warning][Witness] invariant unconfirmed: (long long )A - d >= 0LL (../plain/hard-ll.c:40:9)
[Success][Witness] invariant confirmed: 0LL <= d (../plain/hard-ll.c:41:9)
[Success][Witness] invariant confirmed: 1LL <= p (../plain/hard-ll.c:41:9)
[Success][Witness] invariant confirmed: d <= 8589934590LL (../plain/hard-ll.c:41:9)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:41:9)
[Success][Witness] invariant confirmed: (8589934590LL + 4LL * (long long )A) - d >= 0LL (../plain/hard-ll.c:41:9)
[Warning][Witness] invariant unconfirmed: 2LL * (long long )A - d >= 0LL (../plain/hard-ll.c:41:9)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:25:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )B >= 0LL (../plain/hard-ll.c:25:5)
[Success][Witness] invariant confirmed: (long long )A >= 0LL (../plain/hard-ll.c:25:5)
[Success][Witness] invariant confirmed: (long long )B >= 0LL (../plain/hard-ll.c:25:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:26:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )B >= 0LL (../plain/hard-ll.c:26:5)
[Success][Witness] invariant confirmed: (long long )A >= 0LL (../plain/hard-ll.c:26:5)
[Success][Witness] invariant confirmed: (long long )B >= 0LL (../plain/hard-ll.c:26:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:27:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )B >= 0LL (../plain/hard-ll.c:27:5)
[Success][Witness] invariant confirmed: (long long )A >= 0LL (../plain/hard-ll.c:27:5)
[Success][Witness] invariant confirmed: (long long )B >= 0LL (../plain/hard-ll.c:27:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:29:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )B >= 0LL (../plain/hard-ll.c:29:5)
[Success][Witness] invariant confirmed: (long long )A >= 0LL (../plain/hard-ll.c:29:5)
[Success][Witness] invariant confirmed: (long long )B >= 0LL (../plain/hard-ll.c:29:5)
[Success][Witness] invariant confirmed: 0LL <= r (../plain/hard-ll.c:30:5)
[Success][Witness] invariant confirmed: r <= 4294967295LL (../plain/hard-ll.c:30:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:30:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )B >= 0LL (../plain/hard-ll.c:30:5)
[Success][Witness] invariant confirmed: (long long )A >= 0LL (../plain/hard-ll.c:30:5)
[Success][Witness] invariant confirmed: (long long )B >= 0LL (../plain/hard-ll.c:30:5)
[Success][Witness] invariant confirmed: 0LL <= d (../plain/hard-ll.c:31:5)
[Warning][Witness] invariant unconfirmed: d <= 4294967295LL (../plain/hard-ll.c:31:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:31:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )B >= 0LL (../plain/hard-ll.c:31:5)
[Success][Witness] invariant confirmed: (long long )A >= 0LL (../plain/hard-ll.c:31:5)
[Success][Witness] invariant confirmed: (long long )B >= 0LL (../plain/hard-ll.c:31:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:32:5)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )B >= 0LL (../plain/hard-ll.c:32:5)
[Success][Witness] invariant confirmed: (long long )A >= 0LL (../plain/hard-ll.c:32:5)
[Success][Witness] invariant confirmed: (long long )B >= 0LL (../plain/hard-ll.c:32:5)
[Success][Witness] invariant confirmed: 0LL <= r (../plain/hard-ll.c:34:12)
[Success][Witness] invariant confirmed: 0LL <= d (../plain/hard-ll.c:34:12)
[Success][Witness] invariant confirmed: 1LL <= p (../plain/hard-ll.c:34:12)
[Success][Witness] invariant confirmed: r <= 4294967295LL (../plain/hard-ll.c:34:12)
[Success][Witness] invariant confirmed: d <= 8589934590LL (../plain/hard-ll.c:34:12)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:34:12)
[Warning][Witness] invariant unconfirmed: (4294967295LL + 2LL * (long long )A) - d >= 0LL (../plain/hard-ll.c:34:12)
[Warning][Witness] invariant unconfirmed: (4294967295LL + (long long )A) - d >= 0LL (../plain/hard-ll.c:34:12)
[Success][Witness] invariant confirmed: 0LL <= d (../plain/hard-ll.c:44:12)
[Success][Witness] invariant confirmed: 0LL <= q (../plain/hard-ll.c:44:12)
[Success][Witness] invariant confirmed: 1LL <= p (../plain/hard-ll.c:44:12)
[Success][Witness] invariant confirmed: d <= 8589934590LL (../plain/hard-ll.c:44:12)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )A >= 0LL (../plain/hard-ll.c:44:12)
[Info][Witness] witness validation summary:
  confirmed: 61
  unconfirmed: 17
  refuted: 0
  error: 44
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 122
SV-COMP result: unknown

vars = 71    evals = 8201    narrow_reuses = 130

Timings:
                                  cputime   walltime   allocated   count
Default                          217.381s   217.388s   8759.13MB      1×
  preprocess                         0.027s     0.025s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.14MB      4×
  Cabs2cil                           0.006s     0.006s      4.77MB      4×
  mergeCIL                           0.004s     0.004s      3.34MB      1×
  analysis                         217.335s   217.343s   8741.88MB      1×
    createCFG                          0.001s     0.001s      0.65MB      1×
      handle                             0.001s     0.001s      0.10MB     34×
      iter_connect                       0.001s     0.001s      0.43MB     34×
        computeSCCs                        0.001s     0.001s      0.25MB     35×
    FrontC                             0.004s     0.004s      1.13MB    156×
    Cabs2cil                           0.029s     0.029s     14.57MB    156×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                          217.200s   217.208s   8616.40MB      1×
      S.Dom.equal                        0.017s     0.037s      2.80MB   8331×
      base unassume                      7.029s     7.036s   4912.10MB   1738×
      cheap_full_reach                   0.001s     0.001s      0.03MB      1×
      postsolver                         0.029s     0.029s     15.90MB      1×
        postsolver_iter                    0.029s     0.029s     15.84MB      1×
    warn_global                        0.001s     0.001s      0.16MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
