Tool DIVINE CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-10 10:00:20 CET 2018-12-10 10:48:16 CET 2018-12-10 11:10:44 CET 2018-12-10 11:13:11 CET 2018-12-12 20:23:24 CET 2018-12-10 10:29:49 CET 2018-12-10 10:51:28 CET
Run set divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive
Options --no-symbolic -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 0 8.2 8.3 430 110 0   0      0 .60 .37 40 0   0      0 .031 .033 5.6 0    0      0 .95 .60 47 0   0   0 .0018 .0023 .54 0     0      - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 0 8.3 8.3 430 100 0   0      0 .62 .37 41 0   0      0 .020 .020 5.6 0    0      0 1.0  .65 47 0   0   0 .0047 .0062 .54 0     0      - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 0 8.1 8.2 430 96 0   0      0 .61 .38 40 0   0      0 .026 .027 5.5 0    0      0 .93 .61 46 0   0   0 .0058 .015  .52 0     0      - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 0 8.1 8.2 430 92 0   0      0 .59 .35 41 0   0      0 .050 .051 5.5 0    0      0 .95 .62 47 0   0   0 .0053 .0069 .53 0     0      - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 0 8.2 8.2 430 110 0   0      0 .58 .35 40 0   0      0 .052 .054 5.5 0    0      0 .96 .61 47 0   0   0 .0045 .0051 .40 0     0      - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 8.2 8.2 430 110 0   0      0 .60 .37 41 0   0      0 .020 .020 5.6 0    0      0 .92 .59 46 0   0   0 .0057 .0073 .52 0     0      - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 0 8.4 8.4 430 110 0   0      0 .61 .38 41 0   0      0 .023 .025 5.6 0    0      0 .96 .61 47 0   0   0 .0048 .0058 .53 0     0      - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 8.2 8.2 430 110 0   0      - - - - 0 .60 .36 40 0   0   0 .048 .050 5.7 0    0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 8.2 8.2 430 100 0   0      - - - - 0 .62 .38 41 0   0   0 .050 .051 5.5 0    0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 8.1 8.1 430 110 0   0      - - - - 0 .65 .40 40 0   0   0 .049 .050 5.5 0    0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 8.2 8.3 430 110 0   0      - - - - 0 .58 .35 41 0   0   0 .021 .021 5.6 0    0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 8.2 8.2 430 120 0   0      - - - - 0 .58 .37 40 0   0   0 .024 .026 5.7 0    0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 8.2 8.2 430 110 0   0      - - - - 0 .58 .35 40 0   0   0 .020 .020 5.6 0    0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 8.0 8.0 430 120 0   0      - - - - 0 .62 .41 40 0   0   0 .021 .021 5.6 0    0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 2 8.1 8.1 370 99 0   0      - - - - 0 3.4  1.9  250 0   0   2 42     26     1500   .66 0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 8.2 8.2 430 100 0   0      - - - - 0 .60 .37 41 0   0   0 .021 .023 5.6 0    0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 0 8.1 8.1 430 130 0   0      - - - - 0 .57 .35 41 0   0   0 .023 .024 5.6 0    0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 8.2 8.2 430 99 0   0      - - - - 0 .63 .40 41 0   0   0 .023 .024 5.6 0    0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 8.2 8.2 430 120 0   0      - - - - 0 .63 .39 41 0   0   0 .026 .027 5.6 0    0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 0 8.2 8.2 430 95 0   .0041 - - - - 0 .61 .36 41 0   0   0 .033 .035 5.6 0    0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 8.2 8.2 430 89 0   0      - - - - 0 .58 .38 41 0   0   0 .052 .053 5.5 0    0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 8.0 8.0 430 89 0   0      - - - - 0 .61 .40 42 0   0   0 .021 .021 5.6 0    0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 0 8.3 8.3 430 98 0   0      - - - - 0 .61 .38 43 0   0   0 .053 .054 5.5 0    0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 0 8.2 8.2 430 100 0   0      - - - - 0 .62 .39 41 0   0   0 .020 .021 5.6 0    0  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 1 8.1 8.1 430 100 0   0      -32 4.1  2.4  250 0   0      1 6.7   3.9   300   .62 0      0 3.4  1.9  250 0   0   1 .58   .58   20    .045 0      - -
recursive-simple/afterrec_false-unreach-call_true-termination.c 1 8.2 8.3 430 110 0   0      -32 3.6  2.0  250 0   0      1 7.4   4.2   320   .62 0      0 3.2  1.9  250 0   0   1 .62   .63   20    .045 0      - -
recursive-simple/fibo_10_false-unreach-call_true-termination.c 1 8.1 8.1 430 92 0   0      1 6.8  3.8  330 0   .016  -32 6.8   4.3   310   .62 .0041 1 3.5  2.0  250 0   0   1 .57   .57   20    .049 0      - -
recursive-simple/fibo_15_false-unreach-call.c 1 8.2 8.2 430 100 0   0      1 21    13    1200 0   0      -32 6.7   4.3   300   .62 0      1 3.4  2.0  250 0   0   1 .60   .60   20    .049 .0041 - -
recursive-simple/fibo_20_false-unreach-call.c 1 8.9 8.6 440 110 0   0      0 44    33    7000 0   0      -32 7.3   4.4   310   .62 0      1 3.5  2.1  240 0   0   1 .57   .57   20    .049 0      - -
recursive-simple/fibo_25_false-unreach-call.c 1 18   14   640 190 0   0      0 97    63    3800 0   0      -32 7.1   4.4   310   .62 0      1 3.5  2.1  250 0   0   1 .58   .58   20    .049 0      - -
recursive-simple/fibo_2calls_10_false-unreach-call.c 1 8.1 8.1 430 100 0   0      1 7.1  3.9  330 0   0      -32 7.0   4.4   310   .62 0      1 3.4  2.0  250 0   0   1 .60   .61   20    .049 0      - -
recursive-simple/fibo_2calls_15_false-unreach-call.c 1 8.5 8.5 430 110 0   0      1 21    14    1200 0   0      -32 6.8   4.3   300   .66 0      1 3.3  1.9  250 0   0   1 .57   .57   20    .049 0      - -
recursive-simple/fibo_2calls_20_false-unreach-call.c 1 8.8 8.5 440 110 0   0      0 49    38    7000 0   0      -32 7.2   4.1   310   .62 0      1 3.4  2.0  240 0   0   1 .61   .61   20    .049 .0041 - -
recursive-simple/fibo_2calls_25_false-unreach-call.c 1 19   14   640 200 0   0      0 97    61    4000 0   0      -32 7.6   4.2   310   .62 0      1 3.4  2.0  250 0   0   1 .57   .57   20    .049 0      - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 1 8.2 8.2 430 92 0   0      1 3.5  2.0  250 0   .0041 -32 7.2   4.5   310   .62 0      1 3.5  2.1  250 0   0   1 .57   .57   20    .049 0      - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 1 8.1 8.1 430 100 0   0      1 4.3  2.4  260 0   0      -32 7.1   4.1   310   .62 0      1 3.4  2.0  250 0   0   1 .61   .60   20    .049 0      - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 1 8.3 8.3 430 100 0   0      1 4.6  2.6  270 0   0      -32 6.7   4.3   310   .62 0      1 3.6  2.1  250 0   0   1 .57   .57   20    .049 0      - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 1 8.2 8.2 430 110 0   0      1 4.7  2.6  270 0   0      -32 7.1   4.5   310   .62 0      1 3.6  2.1  250 0   0   1 .58   .59   20    .049 0      - -
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c 1 8.0 8.0 430 96 0   0      1 5.6  3.1  290 0   0      -32 7.3   4.6   310   .62 0      1 3.5  2.0  240 0   0   1 .60   .60   20    .049 0      - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c 1 8.0 8.0 430 110 0   0      1 4.4  2.5  260 0   0      -32 7.0   4.0   310   .62 0      1 3.4  2.0  250 0   0   1 .57   .57   20    .049 0      - -
recursive-simple/fibo_7_false-unreach-call_true-termination.c 1 8.3 8.3 430 100 0   .0041 1 4.8  2.7  270 0   0      -32 7.1   4.5   310   .62 0      1 3.6  2.1  250 0   0   1 .58   .58   20    .049 0      - -
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 0 8.2 8.2 430 110 0   0      0 .63 .38 41 0   0      0 .019 .020 5.6 0    0      0 .95 .63 47 0   0   0 .0049 .0061 .53 0     0      - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 1 8.2 8.2 430 80 0   0      1 4.0  2.3  260 0   .033  -32 7.2   4.5   310   .66 0      1 3.5  2.0  250 0   0   1 .58   .58   20    .049 .0041 - -
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 0 8.3 8.3 430 100 0   0      0 .61 .37 40 0   0      0 .020 .021 5.6 0    0      0 .96 .63 48 0   0   0 .0017 .0022 .54 0     0      - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 1 8.1 8.2 430 110 0   0      1 4.4  2.5  260 0   0      -32 6.9   3.9   300   .62 0      1 3.4  2.0  250 0   0   1 .57   .57   20    .045 0      - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 1 8.1 8.1 430 110 0   0      1 4.7  2.6  270 0   0      -32 7.0   4.5   310   .62 0      1 3.5  2.0  250 0   0   1 .58   .58   20    .045 0      - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 1 8.3 8.3 430 100 0   0      1 4.3  2.4  270 0   0      -32 6.8   4.3   310   .66 0      1 3.3  2.0  250 0   0   1 .58   .58   20    .045 0      - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 1 8.1 8.1 430 110 0   0      1 4.7  2.6  270 0   0      -32 6.6   4.2   310   .62 0      1 3.6  2.1  250 0   0   1 .59   .59   20    .045 0      - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 1 8.3 8.3 430 110 0   0      1 4.1  2.3  260 0   0      -32 6.9   4.0   310   .62 0      1 3.4  2.0  250 0   0   1 .57   .57   20    .045 0      - -
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 0 8.2 8.2 430 100 0   0      0 .60 .38 41 0   0      0 .032 .035 5.6 0    0      0 .97 .64 47 0   0   0 .0020 .0026 .53 0     0      - -
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 0 8.1 8.1 430 97 0   0      0 .59 .37 40 0   0      0 .020 .021 5.6 0    0      0 .95 .61 47 0   0   0 .0016 .0020 .53 0     0      - -
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 0 8.2 8.2 430 110 0   .0041 0 .59 .36 42 0   0      0 .025 .026 5.6 0    0      0 .96 .64 46 0   0   0 .0046 .0074 .48 0     0      - -
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 0 8.2 8.2 430 110 0   0      0 .60 .37 40 0   0      0 .019 .020 5.6 0    0      0 .94 .63 46 0   0   0 .0049 .0061 .54 0     0      - -
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 0 8.1 8.1 430 110 0   0      0 .65 .42 41 0   0      0 .020 .020 5.6 0    0      0 .91 .60 47 0   0   0 .0054 .0095 .40 0     0      - -
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 0 8.2 8.2 430 110 0   0      0 .60 .38 41 0   0      0 .020 .021 5.6 0    0      0 .90 .57 47 0   0   0 .0050 .0066 .53 0     0      - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 1 8.2 8.3 430 95 0   0      1 4.2  2.3  270 0   0      -32 6.9   3.9   300   .62 0      1 3.3  2.0  250 0   0   1 .60   .61   20    .045 0      - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 1 8.3 8.3 430 96 0   0      1 4.3  2.5  270 0   0      -32 7.2   4.0   310   .62 0      1 3.3  2.0  250 0   0   1 .59   .59   20    .045 0      - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 1 8.2 8.2 430 99 0   0      1 5.2  2.9  270 0   .029  -32 6.7   4.2   300   .62 0      1 3.5  2.0  250 0   0   1 .57   .57   20    .045 0      - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 1 8.1 8.1 430 120 0   0      1 4.5  2.6  270 0   0      -32 6.6   4.2   300   .62 0      1 3.4  2.0  240 0   0   1 .58   .58   20    .045 0      - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 1 8.1 8.1 430 91 0   0      1 4.2  2.4  260 0   0      -32 7.0   4.4   310   .62 0      1 3.3  2.0  250 0   0   1 .58   .58   20    .045 0      - -
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 0 8.2 8.2 430 100 0   0      0 .61 .37 43 0   0      0 .049 .050 5.5 0    0      0 .95 .62 47 0   0   0 .0056 .0083 .48 0     0      - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 2 8.2 8.2 370 110 0   0      - - - - 2 3.4  1.9  250 0   0   2 6.9   3.9   320   .66 0  
recursive-simple/afterrec_true-unreach-call_true-termination.c 2 8.0 8.1 370 100 0   0      - - - - 2 3.3  1.8  250 0   0   2 7.2   4.1   310   .62 0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c 2 8.2 8.2 370 110 0   0      - - - - 0 3.6  2.1  250 0   0   2 42     27     2700   .62 0  
recursive-simple/fibo_15_true-unreach-call.c 2 8.2 8.3 370 100 0   0      - - - - 0 3.5  1.9  250 0   0   2 570     520     6300   .62 0  
recursive-simple/fibo_20_true-unreach-call.c 1 8.6 8.4 370 120 0   0      - - - - 0 3.4  1.9  250 0   0   0 960     910     5200   .63 0  
recursive-simple/fibo_25_true-unreach-call.c 1 14   9.4 400 160 0   0      - - - - 0 3.4  1.9  250 0   0   0 960     910     5600   .64 0  
recursive-simple/fibo_2calls_10_true-unreach-call.c 2 8.0 8.0 370 100 0   0      - - - - 0 3.4  1.9  250 0   0   2 93     62     4500   .62 0  
recursive-simple/fibo_2calls_15_true-unreach-call.c 1 8.2 8.2 370 91 0   0      - - - - 0 3.4  1.9  250 0   0   0 960     900     5500   .63 0  
recursive-simple/fibo_2calls_20_true-unreach-call.c 1 8.3 8.0 370 99 0   0      - - - - 0 3.4  1.9  250 0   0   0 960     910     5400   .63 0  
recursive-simple/fibo_2calls_25_true-unreach-call.c 1 14   9.5 400 150 0   0      - - - - 0 3.4  1.9  250 0   0   0 960     900     6000   .64 0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 2 8.3 8.3 370 110 0   0      - - - - 2 3.4  1.9  250 0   0   2 11     6.1   380   .66 0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 2 8.0 8.0 370 98 0   0      - - - - 0 3.4  1.9  250 0   0   2 16     9.8   480   .62 0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 2 8.2 8.2 370 91 0   0      - - - - 0 3.4  1.9  260 0   0   2 21     13     500   .62 0  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 2 8.2 8.2 370 120 0   0      - - - - 0 3.3  1.8  250 0   0   2 28     18     720   .62 0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 2 8.1 8.1 370 110 0   0      - - - - 0 3.5  2.0  250 0   0   2 49     30     1000   .62 0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c 2 8.1 8.1 370 94 0   0      - - - - 0 3.3  1.9  250 0   0   2 16     9.8   470   .62 0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c 2 8.2 8.2 370 110 0   0      - - - - 0 3.3  1.8  260 0   0   2 21     13     540   .62 0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 0 8.1 8.1 430 99 0   0      - - - - 0 .58 .35 40 0   0   0 .051 .053 5.5 0    0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 8.1 8.1 430 120 0   0      - - - - 0 .59 .37 40 0   0   0 .022 .022 5.6 0    0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 8.1 8.1 430 96 0   0      - - - - 0 .59 .37 41 0   0   0 .023 .025 5.6 0    0  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 2 8.1 8.1 370 95 0   0      - - - - 0 3.4  1.9  250 0   0   2 13     8.4   520   .62 0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 0 8.2 8.2 430 95 0   0      - - - - 0 .61 .37 41 0   0   0 .023 .024 5.6 0    0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 8.3 8.4 430 100 0   0      - - - - 0 .59 .36 41 0   0   0 .022 .022 5.6 0    0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 8.2 8.3 430 100 0   0      - - - - 0 .56 .35 40 0   0   0 .020 .021 5.6 0    0  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 2 8.2 8.2 370 100 0   0      - - - - 0 3.1  1.8  250 0   0   2 18     11     520   .62 0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 2 8.1 8.1 370 110 0   0      - - - - 0 3.6  2.0  260 0   0   2 23     14     610   .62 0  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 2 8.4 8.4 370 110 0   0      - - - - 0 3.4  1.9  250 0   0   2 29     18     670   .62 0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 2 8.4 8.7 480 92 0   120      - - - - 0 3.3  1.9  250 0   0   2 37     23     750   .62 0  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 2 8.1 8.1 370 110 0   0      - - - - 0 3.3  1.8  250 0   0   2 11     6.3   430   .62 0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 2 8.2 8.3 370 100 0   0      - - - - 0 3.3  1.9  260 0   0   2 17     11     590   .62 0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 2 8.0 8.0 370 100 0   0      - - - - 0 3.2  1.8  250 0   0   2 25     16     640   .62 0  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 2 8.0 8.1 370 110 0   0      - - - - 0 3.3  1.8  250 0   0   2 35     22     560   .62 0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 2 8.2 8.2 370 100 0   0      - - - - 0 3.3  1.9  250 0   0   2 48     31     710   .62 0  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 2 8.1 8.1 370 100 0   0      - - - - 0 3.4  1.9  250 0   0   2 10     6.4   380   .62 0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 0 8.2 8.2 430 110 0   0      - - - - 0 .60 .37 41 0   0   0 .021 .023 5.6 0    0  
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 96 81 820 800 40000 10000 0   120      44 -42 440   290   31000 0   .082 44 -830 200 120   8700 18   .0041 44 26 110 66 7700 0   0   44 28 16 16 580 1.3 .012 52 6 110 63   8200 0   0   52 48 6000 5400 54000 18 0  
    correct results 52 76 450 440 21000 5600 0   120      22 22 140   80   7900 0   .082 2 2 14 8.1 620 1.2 0      26 26 90 53 6400 0   0   28 28 16 16 570 1.3 .012 3 6 10 5.6 750 0   0   24 48 1200 900 26000 15 0  
        correct true 24 48 200 200 9000 2500 0   120      0 0 0 0 3 6 10 5.6 750 0   0   24 48 1200 900 26000 15 0  
        correct false 28 28 250 240 12000 3100 0   .0041 22 22 140   80   7900 0   .082 2 2 14 8.1 620 1.2 0      26 26 90 53 6400 0   0   28 28 16 16 570 1.3 .012 0 0
    correct-unconfimed results 5 5 53 44 1900 610 0   0      0 0 0 0 0 0
        correct-unconfirmed true 5 5 53 44 1900 610 0   0      0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 2 -64 7.8 4.4 500 0   0     26 -832 180 110   8000 16   .0041 0 0 0 0
        incorrect true 0 2 -64 7.8 4.4 500 0   0     26 -832 180 110   8000 16   .0041 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 81 -42 -830 26 28 6 48
Run set divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Recursive