./goblint --conf conf/svcomp23.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:38:5-42:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:44:5-48:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:52:5-56:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:65:5-69:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:71:5-75:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:79:5-83:5 with factor 12
Collected factors:
functions: 35
functionCalls: 32
loops: 12
loopBreaks: 0
controlFlowStatements: 282
expressions: 1439
instructions: 284
integralVars: (4,62)
arrayVars: (2,0)
pointerVars: (0,14)

Complexity estimates:
File: 4606
no thread creation -> disabeling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn"
Total: 15756
Congruence: 1678
Enabled congruence domain.
Octagon: 4000
Enabled octagon domain for:
__VERIFIER_nondet_int, abort, a, n, m, n_stones2, tmp, tmp___0, tmp___1, n_stones1, a, i, j, b, l, x, y, n, a, i, j, b, l, x, y, n, top, i, key, count, a, tmp, j, count, k, size, a, b, c, i, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val, val
Widening: 5472
Enabled widening thresholds
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:47:9-47:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:54:9-54:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:54:9-54:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:54:9-54:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:54:9-54:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:54:9-54:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:54:9-54:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:54:9-54:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:54:9-54:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:54:9-54:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:54:9-54:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:54:9-54:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:54:9-54:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:74:9-74:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:81:9-81:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:81:9-81:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:81:9-81:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:81:9-81:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:81:9-81:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:81:9-81:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:81:9-81:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:81:9-81:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:81:9-81:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:81:9-81:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:81:9-81:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:81:9-81:18)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 41
  dead: 0
  total: 41
[Warning][Deadcode][CWE-571] condition 'l < m' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:71:11-71:16)
[Warning][Deadcode][CWE-571] condition 'b < n' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:65:11-65:16)
[Warning][Deadcode][CWE-571] condition 'x < i' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:52:11-52:16)
[Warning][Deadcode][CWE-571] condition 'l < m' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:44:11-44:16)
[Warning][Deadcode][CWE-571] condition 'b < n' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:38:11-38:16)
[Warning][Deadcode][CWE-571] condition 'x < i' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops-crafted-1/theatreSquare.c:79:11-79:16)
SV-COMP result: unknown
