Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
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* [apollon073; apollon077; apollon078; apollon119; apollon130] apollon* [apollon077; apollon078; apollon091; apollon114] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 12:59:33 CET 2017-12-02 09:20:19 CET 2017-12-02 10:53:45 CET 2017-12-02 11:06:16 CET 2017-12-02 11:21:21 CET 2017-12-02 06:57:43 CET 2017-12-02 09:56:59 CET
Run set esbmc-kind.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Recursive
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -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 --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .27  28 2.9  false(unreach-call) 1 wit inspect 5.9  280 true -32 wit inspect 5.4   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .25  28 2.1  false(unreach-call) 1 wit inspect 4.4  280 true -32 wit inspect 6.7   260   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .21  28 1.5  true -32 wit inspect 2.0  260 true -32 wit inspect 4.5   220   unknown 0 wit inspect 1.9  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .22  28 2.1  false(unreach-call) 1 wit inspect 2.4  260 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .25  28 2.9  false(unreach-call) 1 wit inspect 9.6  430 true -32 wit inspect 5.2   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.0   56 35    false(unreach-call) 1 wit inspect 47    500 true -32 wit inspect 6.7   260   unknown 0 wit inspect 2.6  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .17  28 2.5  false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 3.3   240   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 340     15000 4200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .019 4.8
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 540     15000 6600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.9
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 340     15000 4200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.9
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 540     15000 6400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .020 4.8
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 540     15000 6300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .017 4.9
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     1300 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.9
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 470     15000 4100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .020 4.9
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .14  26 1.3  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 true 2 wit inspect 38     3000  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 460     15000 5800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .022 4.9
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     7600 8400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 770     15000 7700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .023 4.8
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 450     15000 4900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 5.0
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     450 9300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .023 4.8
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     220 9600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.9
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 280     15000 3300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .018 4.8
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .29  26 3.7  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 5.6   260  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .44  26 4.6  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 31     840  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .085 28 .77 false(unreach-call) 1 wit inspect 2.0  260 true -32 wit inspect 4.3   210   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .084 28 .90 false(unreach-call) 1 wit inspect 3.2  260 true -32 wit inspect 6.1   270   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  28 1.7  false(unreach-call) 1 wit inspect 6.3  340 true -32 wit inspect 5.1   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 1.0   34 15    false(unreach-call) 1 wit inspect 10    1200 true -32 wit inspect 5.3   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 13     200 190    out of memory 0 wit inspect 32    7000 true -32 wit inspect 3.7   260   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect 230     2600 3100    timeout 0 wit inspect 97    3900 true -32 wit inspect 4.6   250   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .15  28 1.6  false(unreach-call) 1 wit inspect 3.8  340 true -32 wit inspect 4.3   270   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect .54  29 7.5  false(unreach-call) 1 wit inspect 12    1200 true -32 wit inspect 6.1   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 6.5   150 83    out of memory 0 wit inspect 42    7000 true -32 wit inspect 5.1   260   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect 140     1900 1700    timeout 0 wit inspect 97    3800 true -32 wit inspect 5.0   260   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  28 .95 false(unreach-call) 1 wit inspect 3.2  260 true -32 wit inspect 5.2   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .084 28 .80 false(unreach-call) 1 wit inspect 2.9  260 true -32 wit inspect 5.0   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  28 .83 false(unreach-call) 1 wit inspect 2.7  270 true -32 wit inspect 5.2   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  28 .83 false(unreach-call) 1 wit inspect 2.6  270 true -32 wit inspect 3.7   260   unknown 0 wit inspect 1.9  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .10  28 1.1  false(unreach-call) 1 wit inspect 5.5  310 true -32 wit inspect 4.3   270   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .082 28 1.1  false(unreach-call) 1 wit inspect 2.4  270 true -32 wit inspect 5.9   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  28 1.1  false(unreach-call) 1 wit inspect 2.7  280 true -32 wit inspect 3.8   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .26  28 2.6  false(unreach-call) 1 wit inspect 2.6  280 false(unreach-call) 1 wit inspect 5.9   260   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .082 28 .84 false(unreach-call) 1 wit inspect 4.0  270 true -32 wit inspect 5.5   260   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   19    - wit inspect - wit inspect
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .30  28 2.0  false(unreach-call) 1 wit inspect 4.1  260 false(unreach-call) 1 wit inspect 7.1   270   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .089 28 .88 false(unreach-call) 1 wit inspect 3.7  270 true -32 wit inspect 5.1   260   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .097 28 1.2  false(unreach-call) 1 wit inspect 5.1  280 true -32 wit inspect 5.2   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  28 1.3  false(unreach-call) 1 wit inspect 2.6  270 true -32 wit inspect 3.5   260   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .15  28 1.4  false(unreach-call) 1 wit inspect 4.8  270 true -32 wit inspect 3.5   260   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .081 28 .86 false(unreach-call) 1 wit inspect 2.3  270 true -32 wit inspect 4.9   260   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 9900    error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0027 .30 - wit inspect - wit inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 2.3   37 30    timeout 0 wit inspect 91    1400 true -32 wit inspect 5.6   260   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .19  28 2.0  false(unreach-call) 1 wit inspect 5.9  370 true -32 wit inspect 5.3   250   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 14     86 170    timeout 0 wit inspect 91    1400 true -32 wit inspect 5.7   260   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .28  28 2.4  false(unreach-call) 1 wit inspect 30    590 true -32 wit inspect 6.5   250   unknown 0 wit inspect 1.9  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .19  28 1.8  false(unreach-call) 1 wit inspect 2.7  270 true -32 wit inspect 6.0   270   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .089 28 .94 false(unreach-call) 1 wit inspect 3.7  270 true -32 wit inspect 3.5   270   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  28 1.1  false(unreach-call) 1 wit inspect 2.6  270 true -32 wit inspect 6.2   260   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  28 1.2  false(unreach-call) 1 wit inspect 2.6  270 true -32 wit inspect 4.8   250   unknown 0 wit inspect 2.6  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16  28 1.6  false(unreach-call) 1 wit inspect 2.8  280 true -32 wit inspect 4.8   260   unknown 0 wit inspect 2.1  200 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .099 28 1.1  false(unreach-call) 1 wit inspect 3.9  260 true -32 wit inspect 3.5   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .20  28 2.2  false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 3.5   230   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect .084 26 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 6.6   250  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect .10  26 .73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 5.8   260  
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect .17  26 1.4  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 55     4500  
recursive-simple/fibo_15_true-unreach-call.c true 1 wit inspect 1.1   33 16    - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 timeout 0 wit inspect 960     5400  
recursive-simple/fibo_20_true-unreach-call.c true 1 wit inspect 15     220 180    - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 timeout 0 wit inspect 960     6000  
recursive-simple/fibo_25_true-unreach-call.c true 1 wit inspect 260     2800 3300    - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 timeout 0 wit inspect 960     6000  
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect .12  26 1.3  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 120     4500  
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect .68  28 8.2  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 timeout 0 wit inspect 960     5500  
recursive-simple/fibo_2calls_20_true-unreach-call.c true 1 wit inspect 8.3   160 110    - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 timeout 0 wit inspect 960     6200  
recursive-simple/fibo_2calls_25_true-unreach-call.c true 1 wit inspect 160     2100 1800    - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 timeout 0 wit inspect 960     5600  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect .10  26 .72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 13     370  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .65 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 17     540  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .67 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 23     590  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect .10  26 .70 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 30     750  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect .085 26 1.0  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 51     1700  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .76 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.2  260 true 2 wit inspect 15     560  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect .11  26 1.0  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  240 true 2 wit inspect 20     660  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .79 43 error (2) 0 wit inspect .018 5.0
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.8
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 9400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .019 5.0
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .10  26 .73 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  240 true 2 wit inspect 13     480  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 9800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.8
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     890 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .022 5.0
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     890 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .45 43 error (2) 0 wit inspect .020 5.0
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect .12  26 .76 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 14     560  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect .093 26 1.1  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 20     640  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect .13  26 1.1  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 26     750  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect .11  26 1.4  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 42     820  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .093 26 .78 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  240 true 2 wit inspect 10     430  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect .10  26 1.0  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 17     580  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect .093 26 1.2  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 24     710  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect .10  26 1.3  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  270 true 2 wit inspect 38     740  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect .12  26 1.3  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.8  250 true 2 wit inspect 52     930  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect .10  26 .84 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 11     360  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     240 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .020 4.8
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 96 99 16000   180000 190000 44 4 670   37000 44 -1211 220 11000 44 0 97 8600 44 43 25 790 52 6 120 8600 52 50 6500 61000
    correct results 68 93 420   6700 5400 36 36 220   13000 5 5 25 1300 0 43 43 25 790 3 6 10 750 25 50 700 26000
        correct true 25 50 3.2 660 31 0 0 0 0 3 6 10 750 25 50 700 26000
        correct false 43 43 420   6000 5400 36 36 220   13000 5 5 25 1300 0 43 43 25 790 0 0
    correct-unconfimed results 6 6 450   5300 5500 0 0 0 0 0 0
        correct-unconfirmed true 6 6 450   5300 5500 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 1 -32 2.0 260 38 -1216 190 9800 0 0 0 0
        incorrect true 0 1 -32 2.0 260 38 -1216 190 9800 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 99 4 -1211 0 43 6 50
Run set esbmc-kind.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Recursive