/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 pesco/divbin2_unwindbound5.yml.witness.yml --witness.yaml.validate pesco/divbin2_unwindbound5.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/divbin2_unwindbound5.i


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


--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: (B == (1U) && counter == (6) && A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && r == (0U)) || (B == (1U) && (!(counter == (6)) || (counter == (6) && !(A >= (2U))) || (counter == (6) && A >= (2U) && !(A <= (3U))) || (counter == (6) && A >= (2U) && A <= (3U) && !(b == (1U))) || (counter == (6) && A >= (2U) && A <= (3U) && b == (1U) && !(q == (2U))) || (counter == (6) && A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && !(r == (0U)))) && counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && q == (0U) && r == A) || (B == (1U) && (!(counter == (6)) || (counter == (6) && !(A >= (2U))) || (counter == (6) && A >= (2U) && !(A <= (3U))) || (counter == (6) && A >= (2U) && A <= (3U) && !(q == (2U))) || (counter == (6) && A >= (2U) && A <= (3U) && q == (2U) && !(r == (0U)))) && (!(counter == (7)) || (counter == (7) && !(A >= (16U))) || (counter == (7) && A >= (16U) && !(A <= (4294967295U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && !(b == (32U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && !(q == (0U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && q == (0U) && !(r == A))) && counter == (4) && A == (1U) && b == (1U) && q == (1U)) || (B == (1U) && (!(q == (2U)) || (q == (2U) && !(r == (0U)))) && (!(counter == (7)) || (counter == (7) && !(A >= (16U))) || (counter == (7) && A >= (16U) && !(A <= (4294967295U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && !(b == (32U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && !(q == (0U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && q == (0U) && !(r == A))) && (!(counter == (4)) || (counter == (4) && !(A == (1U))) || (counter == (4) && A == (1U) && !(q == (1U)))) && counter == (6) && A >= (2U) && A <= (3U) && b == (1U) && q == (3U)) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (2U))) || (A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && !(r == (0U)))) && (!(counter == (7)) || (counter == (7) && !(A >= (16U))) || (counter == (7) && A >= (16U) && !(A <= (4294967295U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && !(b == (32U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && !(q == (0U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && q == (0U) && !(r == A))) && (!(counter == (4)) || (counter == (4) && !(A == (1U))) || (counter == (4) && A == (1U) && !(b == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (3U)))) && counter == (6) && A >= (4U) && A <= (7U) && b == (4U) && q == (1U)) || (B == (1U) && (!(counter == (6)) || (counter == (6) && !(A >= (2U))) || (counter == (6) && A >= (2U) && !(A <= (3U))) || (counter == (6) && A >= (2U) && A <= (3U) && !(q == (2U))) || (counter == (6) && A >= (2U) && A <= (3U) && q == (2U) && !(r == (0U)))) && (!(counter == (7)) || (counter == (7) && !(A >= (16U))) || (counter == (7) && A >= (16U) && !(A <= (4294967295U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && !(b == (32U)))) && (!(counter == (4)) || (counter == (4) && !(A == (1U))) || (counter == (4) && A == (1U) && !(q == (1U)))) && (!(counter == (6)) || (counter == (6) && !(A >= (2U))) || (counter == (6) && A >= (2U) && !(A <= (3U))) || (counter == (6) && A >= (2U) && A <= (3U) && !(q == (3U)))) && (!(counter == (6)) || (counter == (6) && !(A >= (4U))) || (counter == (6) && A >= (4U) && !(A <= (7U))) || (counter == (6) && A >= (4U) && A <= (7U) && !(b == (4U))) || (counter == (6) && A >= (4U) && A <= (7U) && b == (4U) && !(q == (1U)))) && counter == (2) && A == (0U) && b == (1U) && q == (0U) && r == A) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (2U))) || (A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && !(r == (0U)))) && (!(counter == (7)) || (counter == (7) && !(A >= (16U))) || (counter == (7) && A >= (16U) && !(A <= (4294967295U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && !(b == (32U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && !(r == A))) && (!(counter == (4)) || (counter == (4) && !(A == (1U))) || (counter == (4) && A == (1U) && !(b == (1U))) || (counter == (4) && A == (1U) && b == (1U) && !(q == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (3U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(q == (1U)))) && (!(counter == (2)) || (counter == (2) && !(A == (0U))) || (counter == (2) && A == (0U) && !(b == (1U))) || (counter == (2) && A == (0U) && b == (1U) && !(r == A))) && counter == (6) && A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && r >= (8U) && r <= (15U)) (../plain/divbin2_unwindbound5.i:40:24)
[Warning][Witness] couldn't locate invariant: (B == (1U) && counter == (3) && A == (1U) && b == (2U) && q == (0U) && r == (1U)) || (B == (1U) && (!(counter == (3)) || (counter == (3) && !(b == (2U))) || (counter == (3) && b == (2U) && !(q == (0U))) || (counter == (3) && b == (2U) && q == (0U) && !(r == (1U)))) && counter == (4) && A == (1U) && b == (1U) && q == (1U)) || (B == (1U) && (!(counter == (3)) || (counter == (3) && !(A == (1U))) || (counter == (3) && A == (1U) && !(b == (2U))) || (counter == (3) && A == (1U) && b == (2U) && !(r == (1U)))) && (!(counter == (4)) || (counter == (4) && !(A == (1U))) || (counter == (4) && A == (1U) && !(q == (1U)))) && counter == (2) && A == (0U) && b == (1U) && q == (0U) && r == A) || (B == (1U) && (!(counter == (3)) || (counter == (3) && !(A == (1U))) || (counter == (3) && A == (1U) && !(b == (2U))) || (counter == (3) && A == (1U) && b == (2U) && !(r == (1U)))) && (!(counter == (4)) || (counter == (4) && !(A == (1U))) || (counter == (4) && A == (1U) && !(b == (1U))) || (counter == (4) && A == (1U) && b == (1U) && !(q == (1U)))) && (!(counter == (2)) || (counter == (2) && !(A == (0U))) || (counter == (2) && A == (0U) && !(b == (1U))) || (counter == (2) && A == (0U) && b == (1U) && !(r == A))) && counter == (5) && A >= (4U) && A <= (7U) && b == (8U) && q == (0U) && r >= (4U) && r <= (7U)) || (B == (1U) && (!(counter == (3)) || (counter == (3) && !(A == (1U))) || (counter == (3) && A == (1U) && !(b == (2U))) || (counter == (3) && A == (1U) && b == (2U) && !(r == (1U)))) && (!(A == (1U)) || (A == (1U) && !(b == (1U))) || (A == (1U) && b == (1U) && !(q == (1U)))) && (!(counter == (2)) || (counter == (2) && !(A == (0U))) || (counter == (2) && A == (0U) && !(b == (1U))) || (counter == (2) && A == (0U) && b == (1U) && !(r == A))) && (!(counter == (5)) || (counter == (5) && !(A >= (4U))) || (counter == (5) && A >= (4U) && !(A <= (7U))) || (counter == (5) && A >= (4U) && A <= (7U) && !(b == (8U))) || (counter == (5) && A >= (4U) && A <= (7U) && b == (8U) && !(r >= (4U))) || (counter == (5) && A >= (4U) && A <= (7U) && b == (8U) && r >= (4U) && !(r <= (7U)))) && counter == (4) && A >= (2U) && A <= (3U) && b == (4U) && q == (0U) && r >= (2U) && r <= (3U)) || (B == (1U) && (!(counter == (3)) || (counter == (3) && !(A == (1U))) || (counter == (3) && A == (1U) && !(q == (0U))) || (counter == (3) && A == (1U) && q == (0U) && !(r == (1U)))) && (!(counter == (4)) || (counter == (4) && !(A == (1U))) || (counter == (4) && A == (1U) && !(b == (1U)))) && (!(counter == (2)) || (counter == (2) && !(A == (0U))) || (counter == (2) && A == (0U) && !(b == (1U))) || (counter == (2) && A == (0U) && b == (1U) && !(q == (0U))) || (counter == (2) && A == (0U) && b == (1U) && q == (0U) && !(r == A))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (8U))) || (A >= (4U) && A <= (7U) && b == (8U) && !(q == (0U))) || (A >= (4U) && A <= (7U) && b == (8U) && q == (0U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (8U) && q == (0U) && r >= (4U) && !(r <= (7U)))) && (!(counter == (4)) || (counter == (4) && !(b == (4U))) || (counter == (4) && b == (4U) && !(q == (0U))) || (counter == (4) && b == (4U) && q == (0U) && !(r >= (2U))) || (counter == (4) && b == (4U) && q == (0U) && r >= (2U) && !(r <= (3U)))) && counter == (5) && A >= (2U) && A <= (3U) && b == (2U) && q == (1U)) (../plain/divbin2_unwindbound5.i:39:9)
[Warning][Witness] couldn't locate invariant: (B == (1U) && counter == (6) && A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && r == (0U)) || (B == (1U) && (!(counter == (6)) || (counter == (6) && !(A >= (2U))) || (counter == (6) && A >= (2U) && !(A <= (3U))) || (counter == (6) && A >= (2U) && A <= (3U) && !(b == (1U))) || (counter == (6) && A >= (2U) && A <= (3U) && b == (1U) && !(q == (2U))) || (counter == (6) && A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && !(r == (0U)))) && counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && q == (0U) && r == A) || (B == (1U) && (!(counter == (6)) || (counter == (6) && !(A >= (2U))) || (counter == (6) && A >= (2U) && !(A <= (3U))) || (counter == (6) && A >= (2U) && A <= (3U) && !(q == (2U))) || (counter == (6) && A >= (2U) && A <= (3U) && q == (2U) && !(r == (0U)))) && (!(counter == (7)) || (counter == (7) && !(A >= (16U))) || (counter == (7) && A >= (16U) && !(A <= (4294967295U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && !(b == (32U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && !(q == (0U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && q == (0U) && !(r == A))) && counter == (4) && A == (1U) && b == (1U) && q == (1U)) || (B == (1U) && (!(q == (2U)) || (q == (2U) && !(r == (0U)))) && (!(counter == (7)) || (counter == (7) && !(A >= (16U))) || (counter == (7) && A >= (16U) && !(A <= (4294967295U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && !(b == (32U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && !(q == (0U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && q == (0U) && !(r == A))) && (!(counter == (4)) || (counter == (4) && !(A == (1U))) || (counter == (4) && A == (1U) && !(q == (1U)))) && counter == (6) && A >= (2U) && A <= (3U) && b == (1U) && q == (3U)) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (2U))) || (A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && !(r == (0U)))) && (!(counter == (7)) || (counter == (7) && !(A >= (16U))) || (counter == (7) && A >= (16U) && !(A <= (4294967295U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && !(b == (32U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && !(q == (0U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && q == (0U) && !(r == A))) && (!(counter == (4)) || (counter == (4) && !(A == (1U))) || (counter == (4) && A == (1U) && !(b == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (3U)))) && counter == (6) && A >= (4U) && A <= (7U) && b == (4U) && q == (1U)) || (B == (1U) && (!(counter == (6)) || (counter == (6) && !(A >= (2U))) || (counter == (6) && A >= (2U) && !(A <= (3U))) || (counter == (6) && A >= (2U) && A <= (3U) && !(q == (2U))) || (counter == (6) && A >= (2U) && A <= (3U) && q == (2U) && !(r == (0U)))) && (!(counter == (7)) || (counter == (7) && !(A >= (16U))) || (counter == (7) && A >= (16U) && !(A <= (4294967295U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && !(b == (32U)))) && (!(counter == (4)) || (counter == (4) && !(A == (1U))) || (counter == (4) && A == (1U) && !(q == (1U)))) && (!(counter == (6)) || (counter == (6) && !(A >= (2U))) || (counter == (6) && A >= (2U) && !(A <= (3U))) || (counter == (6) && A >= (2U) && A <= (3U) && !(q == (3U)))) && (!(counter == (6)) || (counter == (6) && !(A >= (4U))) || (counter == (6) && A >= (4U) && !(A <= (7U))) || (counter == (6) && A >= (4U) && A <= (7U) && !(b == (4U))) || (counter == (6) && A >= (4U) && A <= (7U) && b == (4U) && !(q == (1U)))) && counter == (2) && A == (0U) && b == (1U) && q == (0U) && r == A) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (2U))) || (A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && !(r == (0U)))) && (!(counter == (7)) || (counter == (7) && !(A >= (16U))) || (counter == (7) && A >= (16U) && !(A <= (4294967295U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && !(b == (32U))) || (counter == (7) && A >= (16U) && A <= (4294967295U) && b == (32U) && !(r == A))) && (!(counter == (4)) || (counter == (4) && !(A == (1U))) || (counter == (4) && A == (1U) && !(b == (1U))) || (counter == (4) && A == (1U) && b == (1U) && !(q == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (3U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(q == (1U)))) && (!(counter == (2)) || (counter == (2) && !(A == (0U))) || (counter == (2) && A == (0U) && !(b == (1U))) || (counter == (2) && A == (0U) && b == (1U) && !(r == A))) && counter == (6) && A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && r >= (8U) && r <= (15U)) (../plain/divbin2_unwindbound5.i:48:5)

runtime: 00:00:10.227
vars: 25, evals: 53

|rho|=25
|called|=6
|stable|=25
|infl|=18
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=18
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2030) on ../plain/divbin2_unwindbound5.i:26:1-50:1
1	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

Memory statistics: total=1204.60MB, max=37.84MB, minor=1201.11MB, major=78.40MB, promoted=74.90MB
    minor collections=586  major collections=12 compactions=0


runtime: 00:00:20.248
vars: 47, evals: 78

|rho|=47
|called|=6
|stable|=47
|infl|=43
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=33
Found 4 contexts for 4 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2026) on ../plain/divbin2_unwindbound5.i:18:1-24:1
1	contexts for entry state of main (2030) on ../plain/divbin2_unwindbound5.i:26:1-50:1
1	contexts for entry state of reach_error (2015) on ../plain/divbin2_unwindbound5.i:12:1-12:161
1	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

Memory statistics: total=2332.89MB, max=57.55MB, minor=2329.33MB, major=150.37MB, promoted=146.80MB
    minor collections=1138  major collections=17 compactions=0


runtime: 00:00:30.249
vars: 47, evals: 81

|rho|=47
|called|=6
|stable|=40
|infl|=43
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=33
Found 4 contexts for 4 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2026) on ../plain/divbin2_unwindbound5.i:18:1-24:1
1	contexts for entry state of main (2030) on ../plain/divbin2_unwindbound5.i:26:1-50:1
1	contexts for entry state of reach_error (2015) on ../plain/divbin2_unwindbound5.i:12:1-12:161
1	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

Memory statistics: total=3102.28MB, max=66.18MB, minor=3098.66MB, major=198.55MB, promoted=194.94MB
    minor collections=1518  major collections=20 compactions=0


runtime: 00:00:40.290
vars: 57, evals: 96

|rho|=57
|called|=6
|stable|=57
|infl|=53
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=41
Found 6 contexts for 4 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_assert (2026) on ../plain/divbin2_unwindbound5.i:18:1-24:1
2	contexts for entry state of reach_error (2015) on ../plain/divbin2_unwindbound5.i:12:1-12:161
1	contexts for entry state of main (2030) on ../plain/divbin2_unwindbound5.i:26:1-50:1
1	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

Memory statistics: total=4227.93MB, max=66.18MB, minor=4224.24MB, major=270.68MB, promoted=266.99MB
    minor collections=2069  major collections=24 compactions=0


runtime: 00:00:50.274
vars: 57, evals: 99

|rho|=57
|called|=6
|stable|=50
|infl|=53
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=41
Found 6 contexts for 4 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_assert (2026) on ../plain/divbin2_unwindbound5.i:18:1-24:1
2	contexts for entry state of reach_error (2015) on ../plain/divbin2_unwindbound5.i:12:1-12:161
1	contexts for entry state of main (2030) on ../plain/divbin2_unwindbound5.i:26:1-50:1
1	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

Memory statistics: total=4998.20MB, max=66.18MB, minor=4994.46MB, major=318.68MB, promoted=314.94MB
    minor collections=2450  major collections=29 compactions=0


runtime: 00:01:00.285
vars: 57, evals: 114

|rho|=57
|called|=6
|stable|=50
|infl|=53
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=41
Found 6 contexts for 4 functions. Top 5 functions:
2	contexts for entry state of __VERIFIER_assert (2026) on ../plain/divbin2_unwindbound5.i:18:1-24:1
2	contexts for entry state of reach_error (2015) on ../plain/divbin2_unwindbound5.i:12:1-12:161
1	contexts for entry state of main (2030) on ../plain/divbin2_unwindbound5.i:26:1-50:1
1	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

Memory statistics: total=6125.22MB, max=66.18MB, minor=6121.40MB, major=390.83MB, promoted=387.01MB
    minor collections=3001  major collections=33 compactions=0

