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* [apollon010; apollon035; apollon045; apollon077; apollon078; apollon138] [apollon007; apollon077; apollon078; apollon143] 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]
Date of execution 2017-12-01 08:49:27 CET 2017-12-01 22:53:44 CET 2017-12-01 23:38:04 CET 2017-12-01 23:47:42 CET 2017-12-01 23:55:24 CET 2017-12-01 22:20:30 CET 2017-12-01 23:01:53 CET
Run set esbmc-incr.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Recursive
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-incr.2017-12-01_0849.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 .33  30 4.0  false(unreach-call) 1 wit inspect 5.6  280 true -32 wit inspect 5.7   280   unknown 0 wit inspect 2.7  190 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 .26  28 2.7  false(unreach-call) 1 wit inspect 4.4  270 true -32 wit inspect 6.3   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .16  28 1.7  true -32 wit inspect 3.2  250 true -32 wit inspect 4.7   230   unknown 0 wit inspect 1.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .24  28 1.9  false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 3.5   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .23  28 2.0  false(unreach-call) 1 wit inspect 13    320 true -32 wit inspect 3.7   270   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.7   97 45    false(unreach-call) 1 wit inspect 51    500 true -32 wit inspect 5.8   250   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .17  28 1.4  false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.5   230   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 570     15000 7700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.9
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 520     15000 6700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .021 4.9
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 560     15000 5800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 820     15000 8100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .024 4.8
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 820     15000 8500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .020 4.9
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     1300 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .021 4.8
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 250     15000 2700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .025 4.8
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .12  26 1.5  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 38     2800  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 250     15000 2400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .020 4.9
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     14000 7000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .025 4.8
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 510     15000 6800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .018 4.9
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 710     15000 6900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .025 5.0
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     280 8500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .020 5.0
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     180 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .018 4.9
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 490     15000 5000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .024 5.0
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .27  26 2.9  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 3.8   260  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .43  26 5.4  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 31     750  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  28 .89 false(unreach-call) 1 wit inspect 3.8  260 true -32 wit inspect 4.3   220   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .094 28 .92 false(unreach-call) 1 wit inspect 3.3  260 true -32 wit inspect 5.5   260   unknown 0 wit inspect 3.0  230 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .17  28 1.7  false(unreach-call) 1 wit inspect 5.9  350 true -32 wit inspect 4.8   250   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect .87  33 11    false(unreach-call) 1 wit inspect 15    1200 true -32 wit inspect 5.4   260   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 14     220 200    out of memory 0 wit inspect 42    7000 true -32 wit inspect 4.9   250   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect 210     2400 2800    timeout 0 wit inspect 97    3700 true -32 wit inspect 5.0   250   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .12  28 1.0  false(unreach-call) 1 wit inspect 5.3  340 true -32 wit inspect 5.2   260   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect .71  31 8.7  false(unreach-call) 1 wit inspect 14    1200 true -32 wit inspect 5.1   260   unknown 0 wit inspect 2.7  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 8.4   170 120    out of memory 0 wit inspect 47    7000 true -32 wit inspect 5.9   270   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect 120     1700 1600    timeout 0 wit inspect 97    4000 true -32 wit inspect 5.0   270   unknown 0 wit inspect 2.6  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  28 .67 false(unreach-call) 1 wit inspect 3.4  260 true -32 wit inspect 5.7   260   unknown 0 wit inspect 2.0  190 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 .11  28 .86 false(unreach-call) 1 wit inspect 4.4  260 true -32 wit inspect 5.2   250   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  28 .89 false(unreach-call) 1 wit inspect 4.7  270 true -32 wit inspect 3.8   270   unknown 0 wit inspect 2.0  180 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 .082 28 1.1  false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 4.9   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .58   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.0  false(unreach-call) 1 wit inspect 6.0  290 true -32 wit inspect 3.5   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .096 28 1.1  false(unreach-call) 1 wit inspect 3.8  270 true -32 wit inspect 5.2   260   unknown 0 wit inspect 2.7  180 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 .12  28 1.1  false(unreach-call) 1 wit inspect 4.4  280 true -32 wit inspect 5.3   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .56   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 .28  28 2.5  false(unreach-call) 1 wit inspect 4.5  280 false(unreach-call) 1 wit inspect 4.6   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .080 28 .88 false(unreach-call) 1 wit inspect 3.7  260 true -32 wit inspect 3.5   260   unknown 0 wit inspect 1.9  210 false(unreach-call) 1 wit inspect .61   18    - 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 1.7  false(unreach-call) 1 wit inspect 4.7  280 false(unreach-call) 1 wit inspect 4.6   270   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .088 28 1.1  false(unreach-call) 1 wit inspect 4.6  260 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/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .10  28 1.0  false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 5.2   260   unknown 0 wit inspect 2.0  180 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 .11  28 1.3  false(unreach-call) 1 wit inspect 4.6  270 true -32 wit inspect 5.0   250   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  28 1.3  false(unreach-call) 1 wit inspect 3.7  270 true -32 wit inspect 4.9   260   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  28 1.0  false(unreach-call) 1 wit inspect 5.4  260 true -32 wit inspect 5.1   250   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 11000    error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0030 .29 - 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   36 29    timeout 0 wit inspect 91    1500 true -32 wit inspect 5.4   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .23  28 1.8  false(unreach-call) 1 wit inspect 8.6  310 true -32 wit inspect 6.1   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 13     85 180    timeout 0 wit inspect 91    1500 true -32 wit inspect 5.7   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .23  28 2.6  false(unreach-call) 1 wit inspect 34    620 true -32 wit inspect 5.5   270   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .20  28 1.6  false(unreach-call) 1 wit inspect 5.5  270 true -32 wit inspect 5.9   270   unknown 0 wit inspect 2.9  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 .093 28 .92 false(unreach-call) 1 wit inspect 3.7  280 true -32 wit inspect 5.1   260   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .56   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 4.0  270 true -32 wit inspect 5.1   260   unknown 0 wit inspect 2.0  180 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 .15  28 1.1  false(unreach-call) 1 wit inspect 3.8  270 true -32 wit inspect 4.9   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  28 1.4  false(unreach-call) 1 wit inspect 4.4  280 true -32 wit inspect 5.5   260   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .080 28 1.0  false(unreach-call) 1 wit inspect 4.0  270 true -32 wit inspect 3.3   270   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .57   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.0  false(unreach-call) 1 wit inspect 3.2  250 false(unreach-call) 1 wit inspect 3.1   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect .073 26 .73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.1  250 true 2 wit inspect 3.6   270  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect .096 26 .75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.0   260  
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect .18  26 1.6  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 62     4500  
recursive-simple/fibo_15_true-unreach-call.c true 1 wit inspect .96  32 12    - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 timeout 0 wit inspect 960     5500  
recursive-simple/fibo_20_true-unreach-call.c true 1 wit inspect 16     240 220    - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 timeout 0 wit inspect 960     6000  
recursive-simple/fibo_25_true-unreach-call.c true 1 wit inspect 240     2600 2800    - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.0  250 timeout 0 wit inspect 960     6000  
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect .13  26 1.3  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 110     4500  
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect .81  30 11    - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.1  250 timeout 0 wit inspect 960     5500  
recursive-simple/fibo_2calls_20_true-unreach-call.c true 1 wit inspect 10     180 160    - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 timeout 0 wit inspect 960     6000  
recursive-simple/fibo_2calls_25_true-unreach-call.c true 1 wit inspect 140     1900 2000    - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 timeout 0 wit inspect 960     5900  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .59 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 9.1   360  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect .076 26 .88 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 true 2 wit inspect 17     540  
recursive-simple/fibo_2calls_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 3.7  250 true 2 wit inspect 22     600  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .80 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 27     700  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect .098 26 1.0  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 55     1700  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .69 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 true 2 wit inspect 14     540  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .86 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 21     830  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1300 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9
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 .72 43 error (2) 0 wit inspect .023 4.9
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .020 4.9
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .70 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 15     490  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 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 .75 43 error (2) 0 wit inspect .024 4.9
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     890 9800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .021 4.9
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .85 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.0  250 true 2 wit inspect 14     540  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect .12  26 1.0  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.1  250 true 2 wit inspect 22     640  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect .10  26 1.1  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.0  250 true 2 wit inspect 33     730  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect .13  26 1.4  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 36     830  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .078 26 .83 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.8  250 true 2 wit inspect 7.2   430  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect .082 26 1.1  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 true 2 wit inspect 18     530  
recursive-simple/sum_15x0_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.8  250 true 2 wit inspect 23     690  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect .11  26 1.1  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 35     760  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect .12  26 1.4  - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 true 2 wit inspect 60     920  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .66 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 true 2 wit inspect 9.4   350  
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 .66 41 error (2) 0 wit inspect .019 4.9
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 17000   190000 190000 44 4 730   37000 44 -1211 210 11000 44 0 110 8300 44 43 25 790 52 6 120   8600 52 50 6500 61000
    correct results 68 93 380   6400 5100 36 36 270   12000 5 5 20 1300 0 43 43 25 790 3 6 9.4 750 25 50 690 26000
        correct true 25 50 3.2 660 31 0 0 0 0 3 6 9.4 750 25 50 690 26000
        correct false 43 43 380   5800 5100 36 36 270   12000 5 5 20 1300 0 43 43 25 790 0 0
    correct-unconfimed results 6 6 400   5000 5100 0 0 0 0 0 0
        correct-unconfirmed true 6 6 400   5000 5100 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 1 -32 3.2 250 38 -1216 190 9800 0 0 0 0
        incorrect true 0 1 -32 3.2 250 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-incr.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Recursive