./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/nla-digbench/fermat1.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/nla-digbench/fermat1.c:38:9-44:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/nla-digbench/fermat1.c:46:9-52:9 with factor 8
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] Setting "ana.int.interval" to true
[Info] function main uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __VERIFIER_nondet_double
[Info]     assume_abort_if_not
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]   "up":
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] __VERIFIER_assert, abort, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, r, u, v, A, R, cond, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )

[Info] runtime: 00:00:10.135
[Info] vars: 171, evals: 20800

[Info] |called|=72

Memory statistics: total=12057.25MB, max=18.81MB, minor=12054.20MB, major=135.70MB, promoted=132.65MB
    minor collections=5764  major collections=33 compactions=0


[Info] runtime: 00:00:20.197
[Info] vars: 171, evals: 39036

[Info] |called|=68

Memory statistics: total=23142.81MB, max=28.61MB, minor=23139.71MB, major=255.15MB, promoted=252.05MB
    minor collections=11059  major collections=51 compactions=0


[Info] runtime: 00:00:30.233
[Info] vars: 171, evals: 55670

[Info] |called|=73

Memory statistics: total=33600.39MB, max=37.84MB, minor=33597.27MB, major=368.64MB, promoted=365.52MB
    minor collections=16052  major collections=63 compactions=0


[Info] runtime: 00:00:40.301
[Info] vars: 171, evals: 71055

[Info] |called|=50

Memory statistics: total=43625.66MB, max=50.04MB, minor=43622.54MB, major=480.69MB, promoted=477.57MB
    minor collections=20836  major collections=71 compactions=0


[Info] runtime: 00:00:50.359
[Info] vars: 171, evals: 85352

[Info] |called|=73

Memory statistics: total=53209.26MB, max=57.55MB, minor=53206.13MB, major=588.78MB, promoted=585.65MB
    minor collections=25410  major collections=78 compactions=0


[Info] runtime: 00:01:00.410
[Info] vars: 171, evals: 98691

[Info] |called|=63

Memory statistics: total=62500.78MB, max=76.11MB, minor=62497.65MB, major=695.34MB, promoted=692.21MB
    minor collections=29843  major collections=83 compactions=0

