./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/recursified_nla-digbench/recursified_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] 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]     func_to_recursive_line_33_to_36_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     func_to_recursive_line_46_to_51_0
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     func_to_recursive_line_38_to_43_0
[Info]     func_to_recursive_line_33_to_36_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     func_to_recursive_line_46_to_51_0
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     func_to_recursive_line_38_to_43_0
[Info]     func_to_recursive_line_33_to_36_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     func_to_recursive_line_46_to_51_0
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     func_to_recursive_line_38_to_43_0
[Info]     func_to_recursive_line_33_to_36_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     func_to_recursive_line_46_to_51_0
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     func_to_recursive_line_38_to_43_0
[Info]     func_to_recursive_line_33_to_36_0
[Info]     __VERIFIER_assert
[Info]     reach_error
[Info]     func_to_recursive_line_46_to_51_0
[Info]     __VERIFIER_assert
[Info]     func_to_recursive_line_46_to_51_0
[Info]     func_to_recursive_line_38_to_43_0
[Info]     __VERIFIER_assert
[Info]     func_to_recursive_line_38_to_43_0
[Info]     func_to_recursive_line_33_to_36_0
[Info]     __VERIFIER_assert
[Info]     func_to_recursive_line_46_to_51_0
[Info]     func_to_recursive_line_38_to_43_0
[Info]     func_to_recursive_line_33_to_36_0
[Info]   "up":
[Info] function func_to_recursive_line_46_to_51_0 is recursive, disable interval and interval_set contexts
[Info] function func_to_recursive_line_38_to_43_0 is recursive, disable interval and interval_set contexts
[Info] function func_to_recursive_line_33_to_36_0 is recursive, disable interval and interval_set contexts
[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 widening thresholds
[Info] Enabled octagon domain ONLY for:
[Info] __VERIFIER_assert, abort, i, count, tmp, key, a, count, i, j, i___0, j___0, k, size, r, top, expression, A, R, u, v, A, v, u, r, v, r, A, u, u, r, A, v, cond, cond
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )

[Info] runtime: 00:00:10.155
[Info] vars: 11898, evals: 9057

[Info] |called|=1138

Memory statistics: total=19866.93MB, max=50.04MB, minor=19855.32MB, major=98.93MB, promoted=87.32MB
    minor collections=9475  major collections=15 compactions=0


[Info] runtime: 00:00:20.220
[Info] vars: 16456, evals: 12530

[Info] |called|=1573

Memory statistics: total=36414.63MB, max=66.18MB, minor=36395.63MB, major=145.09MB, promoted=126.09MB
    minor collections=17363  major collections=17 compactions=0


[Info] runtime: 00:00:30.254
[Info] vars: 19837, evals: 15106

[Info] |called|=1895

Memory statistics: total=51682.28MB, max=76.11MB, minor=51656.92MB, major=182.24MB, promoted=156.87MB
    minor collections=24640  major collections=18 compactions=0


[Info] runtime: 00:00:40.291
[Info] vars: 22530, evals: 17157

[Info] |called|=2149

Memory statistics: total=65839.58MB, max=87.53MB, minor=65808.05MB, major=213.52MB, promoted=181.99MB
    minor collections=31389  major collections=20 compactions=0


[Info] runtime: 00:00:50.333
[Info] vars: 24855, evals: 18929

[Info] |called|=2373

Memory statistics: total=79365.07MB, max=100.66MB, minor=79328.00MB, major=241.93MB, promoted=204.87MB
    minor collections=37836  major collections=20 compactions=0


[Info] runtime: 00:01:00.368
[Info] vars: 26872, evals: 20466

[Info] |called|=2564

Memory statistics: total=92193.15MB, max=115.77MB, minor=92150.54MB, major=267.39MB, promoted=224.78MB
    minor collections=43951  major collections=21 compactions=0

