/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/hard-u_valuebound1.yml.witness.yml --witness.yaml.validate pesco/hard-u_valuebound1.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/hard-u_valuebound1.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: (A >= (0U) && A <= (1U) && p >= (2U) && p <= (4294967295U)) || (A >= (0U) && A <= (1U) && (!(p >= (2U)) || (p >= (2U) && !(p <= (4294967295U)))) && !(d == (0U)) && !(p == (1U)) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && (!(p >= (2U)) || (p >= (2U) && !(p <= (4294967295U)))) && d == (0U) && d >= (0U) && d <= (2147483647U) && !(p == (1U)) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && (d == (0U) || (!(d == (0U)) && p == (1U)) || (!(d == (0U)) && !(p == (1U)) && !(q == (0U))) || (!(d == (0U)) && !(p == (1U)) && q == (0U) && !(r >= (0U))) || (!(d == (0U)) && !(p == (1U)) && q == (0U) && r >= (0U) && !(r <= (1U)))) && A <= (1U) && (p == (1U) || (!(p == (1U)) && !(q == (0U))) || (!(p == (1U)) && q == (0U) && !(r >= (0U))) || (!(p == (1U)) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(p >= (2U)) || (p >= (2U) && !(p <= (4294967295U)))) && d >= (0U) && d <= (2147483647U) && p <= (2147483647U) && p >= (1U)) || (A >= (0U) && A <= (1U) && p == (1U) && (!(p >= (2U)) || (p >= (2U) && !(p <= (4294967295U)))) && d >= (0U) && d <= (2147483647U) && p <= (2147483647U) && !(p >= (1U)) && p >= (0U) && q == (0U) && r >= (0U) && r <= (1U)) (../plain/hard-u_valuebound1.c:52:9)
[Warning][Witness] couldn't locate invariant: (A >= (0U) && A <= (1U) && !(d == (0U)) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && (d == (0U) || (!(d == (0U)) && !(q == (0U))) || (!(d == (0U)) && q == (0U) && !(r >= (0U))) || (!(d == (0U)) && q == (0U) && r >= (0U) && !(r <= (1U)))) && !(p == (0U))) (../plain/hard-u_valuebound1.c:48:9)
[Error][Witness] CIL couldn't parse invariant: cond == (1) (../plain/hard-u_valuebound1.c:19:5)
[Info][Witness] invariant has undefined variables or side effects: cond == (1) (../plain/hard-u_valuebound1.c:19:5)
../plain/hard-u_valuebound1.c:19: Error: Cannot resolve variable cond.
[Warning][Witness] couldn't locate invariant: A >= (0U) && A <= (1U) && p == (1U) (../plain/hard-u_valuebound1.c:50:24)
[Info][Witness] unassume invariant: ((((((((A >= 0U && q == 0U) && A <= 1U) && d >= 0U) && d <= 2U) && r >= 0U) && r <= 1U) || ((((((q == 0U && A >= 0U) && A <= 1U) && (((! (d >= 0U) || (d >= 0U && ! (d <= 2U))) || ((d >= 0U && d <= 2U) && ! (r >= 0U))) || (((d >= 0U && d <= 2U) && r >= 0U) && ! (r <= 1U)))) && d == B) && p == 1U) && r == A)) || ((((((q == 0U && A >= 0U) && A <= 1U) && (! (d >= 0U) || (d >= 0U && ! (d <= 2U)))) && ((! (d == B) || (d == B && ! (p == 1U))) || ((d == B && p == 1U) && ! (r == A)))) && r <= 1U) && r >= 0U)) && ((((((((A >= 0U && q == 0U) && A <= 1U) && d >= 0U) && d <= 2U) && r >= 0U) && r <= 1U) || ((((((q == 0U && A >= 0U) && A <= 1U) && (((! (d >= 0U) || (d >= 0U && ! (d <= 2U))) || ((d >= 0U && d <= 2U) && ! (r >= 0U))) || (((d >= 0U && d <= 2U) && r >= 0U) && ! (r <= 1U)))) && d == B) && p == 1U) && r == A)) || ((((((q == 0U && A >= 0U) && A <= 1U) && (! (d >= 0U) || (d >= 0U && ! (d <= 2U)))) && ((! (d == B) || (d == B && ! (p == 1U))) || ((d == B && p == 1U) && ! (r == A)))) && r <= 1U) && r >= 0U)) (../plain/hard-u_valuebound1.c:34:5-34:10)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/hard-u_valuebound1.c:39:9-39:38)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/hard-u_valuebound1.c:42:9-42:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/hard-u_valuebound1.c:43:9-43:18)
[Info][Witness] unassume invariant: ((((((((A >= 0U && q == 0U) && A <= 1U) && d >= 0U) && d <= 2U) && r >= 0U) && r <= 1U) || ((((((q == 0U && A >= 0U) && A <= 1U) && (((! (d >= 0U) || (d >= 0U && ! (d <= 2U))) || ((d >= 0U && d <= 2U) && ! (r >= 0U))) || (((d >= 0U && d <= 2U) && r >= 0U) && ! (r <= 1U)))) && d == B) && p == 1U) && r == A)) || ((((((q == 0U && A >= 0U) && A <= 1U) && (! (d >= 0U) || (d >= 0U && ! (d <= 2U)))) && ((! (d == B) || (d == B && ! (p == 1U))) || ((d == B && p == 1U) && ! (r == A)))) && r <= 1U) && r >= 0U)) && ((((((((A >= 0U && q == 0U) && A <= 1U) && d >= 0U) && d <= 2U) && r >= 0U) && r <= 1U) || ((((((q == 0U && A >= 0U) && A <= 1U) && (((! (d >= 0U) || (d >= 0U && ! (d <= 2U))) || ((d >= 0U && d <= 2U) && ! (r >= 0U))) || (((d >= 0U && d <= 2U) && r >= 0U) && ! (r <= 1U)))) && d == B) && p == 1U) && r == A)) || ((((((q == 0U && A >= 0U) && A <= 1U) && (! (d >= 0U) || (d >= 0U && ! (d <= 2U)))) && ((! (d == B) || (d == B && ! (p == 1U))) || ((d == B && p == 1U) && ! (r == A)))) && r <= 1U) && r >= 0U)) (../plain/hard-u_valuebound1.c:43:9-43:18)
[Info][Witness] unassume invariant: ((((((((q == 0U && r <= 1U) && d >= 0U) && A >= 0U) && A <= 1U) && r >= 0U) && (d <= 1U || (! (d <= 1U) && d <= 2U))) && ((((r <= 1U && A >= 0U) && q == 0U) && A <= 1U) && r >= 0U)) && ((((((A >= 0U && A <= 1U) && p >= 1U) && p <= 2147483647U) || (((((((((A >= 0U && A <= 1U) && p <= 2147483647U) && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && q == 0U) && r >= 0U) && r <= 1U)) || (((((((A >= 0U && A <= 1U) && (! (p >= 1U) || (p >= 1U && ! (p <= 2147483647U)))) && (((! (p <= 2147483647U) || ((p <= 2147483647U && ! (p >= 1U)) && ! (d >= 1U))) || (((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && ! (d <= 2147483647U))) || ((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && ! (p >= 0U)))) && ! (d == 0U)) && q == 0U) && r >= 0U) && r <= 1U)) || (((((A >= 0U && A <= 1U) && (! (p >= 1U) || (p >= 1U && ! (p <= 2147483647U)))) && ((((((! (p <= 2147483647U) || ((p <= 2147483647U && ! (p >= 1U)) && ! (d >= 1U))) || (((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && ! (d <= 2147483647U))) || ((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && ! (p >= 0U))) || (((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && ! (q == 0U))) || ((((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && q == 0U) && ! (r >= 0U))) || (((((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((d == 0U || (! (d == 0U) && ! (q == 0U))) || ((! (d == 0U) && q == 0U) && ! (r >= 0U))) || (((! (d == 0U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ! (p == 0U)))) && ((((r <= 1U && A >= 0U) && q == 0U) && A <= 1U) && r >= 0U) (../plain/hard-u_valuebound1.c:36:12-36:13)
[Info][Witness] unassume invariant: ((((((((q == 0U && r <= 1U) && d >= 0U) && A >= 0U) && A <= 1U) && r >= 0U) && (d <= 1U || (! (d <= 1U) && d <= 2U))) && ((((r <= 1U && A >= 0U) && q == 0U) && A <= 1U) && r >= 0U)) && ((((((A >= 0U && A <= 1U) && p >= 1U) && p <= 2147483647U) || (((((((((A >= 0U && A <= 1U) && p <= 2147483647U) && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && q == 0U) && r >= 0U) && r <= 1U)) || (((((((A >= 0U && A <= 1U) && (! (p >= 1U) || (p >= 1U && ! (p <= 2147483647U)))) && (((! (p <= 2147483647U) || ((p <= 2147483647U && ! (p >= 1U)) && ! (d >= 1U))) || (((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && ! (d <= 2147483647U))) || ((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && ! (p >= 0U)))) && ! (d == 0U)) && q == 0U) && r >= 0U) && r <= 1U)) || (((((A >= 0U && A <= 1U) && (! (p >= 1U) || (p >= 1U && ! (p <= 2147483647U)))) && ((((((! (p <= 2147483647U) || ((p <= 2147483647U && ! (p >= 1U)) && ! (d >= 1U))) || (((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && ! (d <= 2147483647U))) || ((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && ! (p >= 0U))) || (((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && ! (q == 0U))) || ((((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && q == 0U) && ! (r >= 0U))) || (((((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((d == 0U || (! (d == 0U) && ! (q == 0U))) || ((! (d == 0U) && q == 0U) && ! (r >= 0U))) || (((! (d == 0U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ! (p == 0U)))) && ((((r <= 1U && A >= 0U) && q == 0U) && A <= 1U) && r >= 0U) (../plain/hard-u_valuebound1.c:40:13-40:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/hard-u_valuebound1.c:47:9-47:40)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/hard-u_valuebound1.c:48:9-48:36)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/hard-u_valuebound1.c:55:13-55:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/hard-u_valuebound1.c:56:13-56:22)
[Info][Witness] unassume invariant: ((((((((q == 0U && r <= 1U) && d >= 0U) && A >= 0U) && A <= 1U) && r >= 0U) && (d <= 1U || (! (d <= 1U) && d <= 2U))) && ((((r <= 1U && A >= 0U) && q == 0U) && A <= 1U) && r >= 0U)) && ((((((A >= 0U && A <= 1U) && p >= 1U) && p <= 2147483647U) || (((((((((A >= 0U && A <= 1U) && p <= 2147483647U) && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && q == 0U) && r >= 0U) && r <= 1U)) || (((((((A >= 0U && A <= 1U) && (! (p >= 1U) || (p >= 1U && ! (p <= 2147483647U)))) && (((! (p <= 2147483647U) || ((p <= 2147483647U && ! (p >= 1U)) && ! (d >= 1U))) || (((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && ! (d <= 2147483647U))) || ((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && ! (p >= 0U)))) && ! (d == 0U)) && q == 0U) && r >= 0U) && r <= 1U)) || (((((A >= 0U && A <= 1U) && (! (p >= 1U) || (p >= 1U && ! (p <= 2147483647U)))) && ((((((! (p <= 2147483647U) || ((p <= 2147483647U && ! (p >= 1U)) && ! (d >= 1U))) || (((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && ! (d <= 2147483647U))) || ((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && ! (p >= 0U))) || (((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && ! (q == 0U))) || ((((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && q == 0U) && ! (r >= 0U))) || (((((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((d == 0U || (! (d == 0U) && ! (q == 0U))) || ((! (d == 0U) && q == 0U) && ! (r >= 0U))) || (((! (d == 0U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ! (p == 0U)))) && ((((r <= 1U && A >= 0U) && q == 0U) && A <= 1U) && r >= 0U) (../plain/hard-u_valuebound1.c:56:13-56:22)
[Info][Witness] unassume invariant: ((((((((q == 0U && r <= 1U) && d >= 0U) && A >= 0U) && A <= 1U) && r >= 0U) && (d <= 1U || (! (d <= 1U) && d <= 2U))) && ((((r <= 1U && A >= 0U) && q == 0U) && A <= 1U) && r >= 0U)) && ((((((A >= 0U && A <= 1U) && p >= 1U) && p <= 2147483647U) || (((((((((A >= 0U && A <= 1U) && p <= 2147483647U) && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && q == 0U) && r >= 0U) && r <= 1U)) || (((((((A >= 0U && A <= 1U) && (! (p >= 1U) || (p >= 1U && ! (p <= 2147483647U)))) && (((! (p <= 2147483647U) || ((p <= 2147483647U && ! (p >= 1U)) && ! (d >= 1U))) || (((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && ! (d <= 2147483647U))) || ((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && ! (p >= 0U)))) && ! (d == 0U)) && q == 0U) && r >= 0U) && r <= 1U)) || (((((A >= 0U && A <= 1U) && (! (p >= 1U) || (p >= 1U && ! (p <= 2147483647U)))) && ((((((! (p <= 2147483647U) || ((p <= 2147483647U && ! (p >= 1U)) && ! (d >= 1U))) || (((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && ! (d <= 2147483647U))) || ((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && ! (p >= 0U))) || (((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && ! (q == 0U))) || ((((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && q == 0U) && ! (r >= 0U))) || (((((((p <= 2147483647U && ! (p >= 1U)) && d >= 1U) && d <= 2147483647U) && p >= 0U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((d == 0U || (! (d == 0U) && ! (q == 0U))) || ((! (d == 0U) && q == 0U) && ! (r >= 0U))) || (((! (d == 0U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ! (p == 0U)))) && ((((r <= 1U && A >= 0U) && q == 0U) && A <= 1U) && r >= 0U) (../plain/hard-u_valuebound1.c:54:13-54:19)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/hard-u_valuebound1.c:60:5-60:36)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 38
  dead: 0
  total lines: 38
[Warning][Deadcode][CWE-571] condition 'B >= 0U' (possibly inserted by CIL) is always true (../plain/hard-u_valuebound1.c:28:5-28:38)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/hard-u_valuebound1.c:36:12-36:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/hard-u_valuebound1.c:46:12-46:13)
[Warning][Deadcode][CWE-571] condition 'A >= 0U' (possibly inserted by CIL) is always true (../plain/hard-u_valuebound1.c:26:5-26:38)
[Warning][Witness] invariant unconfirmed: (A >= (0U) && q == (0U) && A <= (1U) && d >= (0U) && d <= (2U) && r >= (0U) && r <= (1U)) || (q == (0U) && A >= (0U) && A <= (1U) && (!(d >= (0U)) || (d >= (0U) && !(d <= (2U))) || (d >= (0U) && d <= (2U) && !(r >= (0U))) || (d >= (0U) && d <= (2U) && r >= (0U) && !(r <= (1U)))) && d == B && p == (1U) && r == A) || (q == (0U) && A >= (0U) && A <= (1U) && (!(d >= (0U)) || (d >= (0U) && !(d <= (2U)))) && (!(d == B) || (d == B && !(p == (1U))) || (d == B && p == (1U) && !(r == A))) && r <= (1U) && r >= (0U)) (../plain/hard-u_valuebound1.c:36:5)
[Warning][Witness] invariant unconfirmed: r <= (1U) && A >= (0U) && q == (0U) && A <= (1U) && r >= (0U) (../plain/hard-u_valuebound1.c:39:9)
[Warning][Witness] invariant unconfirmed: (A >= (0U) && A <= (1U) && p >= (1U) && p <= (2147483647U)) || (A >= (0U) && A <= (1U) && p <= (2147483647U) && !(p >= (1U)) && d >= (1U) && d <= (2147483647U) && p >= (0U) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && (!(p >= (1U)) || (p >= (1U) && !(p <= (2147483647U)))) && (!(p <= (2147483647U)) || (p <= (2147483647U) && !(p >= (1U)) && !(d >= (1U))) || (p <= (2147483647U) && !(p >= (1U)) && d >= (1U) && !(d <= (2147483647U))) || (p <= (2147483647U) && !(p >= (1U)) && d >= (1U) && d <= (2147483647U) && !(p >= (0U)))) && !(d == (0U)) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && (!(p >= (1U)) || (p >= (1U) && !(p <= (2147483647U)))) && (!(p <= (2147483647U)) || (p <= (2147483647U) && !(p >= (1U)) && !(d >= (1U))) || (p <= (2147483647U) && !(p >= (1U)) && d >= (1U) && !(d <= (2147483647U))) || (p <= (2147483647U) && !(p >= (1U)) && d >= (1U) && d <= (2147483647U) && !(p >= (0U))) || (p <= (2147483647U) && !(p >= (1U)) && d >= (1U) && d <= (2147483647U) && p >= (0U) && !(q == (0U))) || (p <= (2147483647U) && !(p >= (1U)) && d >= (1U) && d <= (2147483647U) && p >= (0U) && q == (0U) && !(r >= (0U))) || (p <= (2147483647U) && !(p >= (1U)) && d >= (1U) && d <= (2147483647U) && p >= (0U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (d == (0U) || (!(d == (0U)) && !(q == (0U))) || (!(d == (0U)) && q == (0U) && !(r >= (0U))) || (!(d == (0U)) && q == (0U) && r >= (0U) && !(r <= (1U)))) && !(p == (0U))) (../plain/hard-u_valuebound1.c:40:24)
[Warning][Witness] invariant unconfirmed: r <= (1U) && A >= (0U) && q == (0U) && A <= (1U) && r >= (0U) (../plain/hard-u_valuebound1.c:38:9)
[Warning][Witness] invariant unconfirmed: q == (0U) && r <= (1U) && d >= (0U) && A >= (0U) && A <= (1U) && r >= (0U) && (d <= (1U) || (!(d <= (1U)) && d <= (2U))) (../plain/hard-u_valuebound1.c:42:9)
../plain/hard-u_valuebound1.c:19: Error: Cannot resolve variable cond.
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 6
  refuted: 0
  error: 4
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 10
SV-COMP result: unknown

vars = 88    evals = 232    narrow_reuses = 8

Timings:
                                  cputime   walltime   allocated   count
Default                            2.357s     2.358s    257.42MB      1×
  preprocess                         0.024s     0.023s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.15MB      4×
  Cabs2cil                           0.005s     0.005s      4.80MB      4×
  mergeCIL                           0.003s     0.003s      3.35MB      1×
  analysis                           2.316s     2.317s    240.10MB      1×
    createCFG                          0.001s     0.001s      0.69MB      1×
      handle                             0.001s     0.001s      0.12MB     34×
      iter_connect                       0.001s     0.001s      0.45MB     34×
        computeSCCs                        0.001s     0.001s      0.27MB     35×
    FrontC                             0.002s     0.002s      1.19MB     14×
    Cabs2cil                           0.010s     0.010s      2.20MB     14×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            2.064s     2.064s    212.56MB      1×
      S.Dom.equal                        0.001s     0.001s      0.09MB    240×
      base unassume                      0.114s     0.114s    108.61MB     36×
      cheap_full_reach                   0.001s     0.001s      0.04MB      1×
      postsolver                         0.074s     0.074s     19.67MB      1×
        postsolver_iter                    0.074s     0.074s     19.59MB      1×
    warn_global                        0.001s     0.001s      0.26MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
