Tool CPAchecker 1.6.1-svn 26758M 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*
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: 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-11-30 11:20:26 CET 2017-12-01 07:36:48 CET 2017-12-01 08:27:40 CET 2017-12-01 08:32:13 CET 2017-12-01 08:39:14 CET 2017-12-01 04:24:39 CET 2017-12-01 07:43:13 CET
Run set cpa-bam-slicing.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Recursive
Options -ldv-bam-svcomp -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-slicing.2017-11-30_1120.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) 0 wit inspect 3.2 280 29 true -32 wit inspect 3.7 260 true -32 wit inspect 5.3 230 unknown 0 wit inspect 3.0 210 true -32 wit inspect .61 19 - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 3.5 280 33 true -32 wit inspect 3.4 260 true -32 wit inspect 4.3 230 unknown 0 wit inspect 2.9 180 error (2) 0 wit inspect .59 19 - wit inspect - wit inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 3.1 280 28 true -32 wit inspect 3.2 250 true -32 wit inspect 5.9 290 unknown 0 wit inspect 2.8 180 true -32 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 3.3 280 31 true -32 wit inspect 3.6 260 true -32 wit inspect 4.4 230 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 3.2 280 27 true -32 wit inspect 4.5 260 true -32 wit inspect 5.8 220 unknown 0 wit inspect 2.9 180 true -32 wit inspect .59 18 - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 3.2 280 29 true -32 wit inspect 3.6 260 true -32 wit inspect 4.6 230 unknown 0 wit inspect 2.8 210 true -32 wit inspect .62 18 - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 3.2 280 27 true -32 wit inspect 3.2 260 true -32 wit inspect 4.3 230 unknown 0 wit inspect 2.8 180 true -32 wit inspect .59 18 - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c false(unreach-call) -16 wit inspect 3.4 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4 260 true 2 wit inspect 4.7 220
recursive/Ackermann03_true-unreach-call_true-no-overflow.c false(unreach-call) -16 wit inspect 3.4 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4 260 true 2 wit inspect 4.2 230
recursive/Ackermann04_true-unreach-call_true-no-overflow.c false(unreach-call) -16 wit inspect 3.3 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 250 true 2 wit inspect 4.9 230
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.4 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4 260 true 2 wit inspect 5.6 220
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.7 290 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 260 true 2 wit inspect 4.2 220
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.2 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8 280 true 2 wit inspect 6.6 240
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c false(unreach-call) -16 wit inspect 3.2 280 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2 260 true 2 wit inspect 5.9 220
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.2 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4 250 true 2 wit inspect 5.8 230
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.3 280 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4 260 true 2 wit inspect 4.7 220
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.3 290 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 260 true 2 wit inspect 4.9 220
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.4 280 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2 250 true 2 wit inspect 4.3 230
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c false(unreach-call) -16 wit inspect 3.9 290 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3 260 true 2 wit inspect 5.6 230
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.1 280 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.3 250 true 2 wit inspect 5.7 230
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.6 290 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4 260 true 2 wit inspect 4.8 230
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.3 280 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1 260 true 2 wit inspect 4.7 230
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.1 290 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4 260 true 2 wit inspect 4.7 210
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.3 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3 260 true 2 wit inspect 4.8 220
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 30 true -32 wit inspect 3.3 260 false(unreach-call) 1 wit inspect 4.4 240 unknown 0 wit inspect 2.8 180 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 27 true -32 wit inspect 3.0 260 false(unreach-call) 1 wit inspect 4.8 220 unknown 0 wit inspect 2.7 180 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 290 33 true -32 wit inspect 3.8 260 true -32 wit inspect 4.4 220 unknown 0 wit inspect 2.7 180 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 3.3 280 33 true -32 wit inspect 3.6 250 true -32 wit inspect 6.9 290 unknown 0 wit inspect 3.1 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 3.1 280 28 true -32 wit inspect 4.0 260 true -32 wit inspect 4.5 230 unknown 0 wit inspect 2.9 180 false(unreach-call) 1 wit inspect .63 18 - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect 3.2 290 27 true -32 wit inspect 3.2 260 true -32 wit inspect 4.3 230 unknown 0 wit inspect 2.1 220 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect 3.5 290 34 true -32 wit inspect 4.2 260 true -32 wit inspect 4.7 230 unknown 0 wit inspect 3.0 180 false(unreach-call) 1 wit inspect .58 19 - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 3.3 280 30 true -32 wit inspect 3.5 260 true -32 wit inspect 4.7 230 unknown 0 wit inspect 2.8 190 false(unreach-call) 1 wit inspect .60 19 - wit inspect - wit inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 3.3 290 32 true -32 wit inspect 3.4 260 true -32 wit inspect 4.5 230 unknown 0 wit inspect 2.9 180 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect 3.6 290 34 true -32 wit inspect 4.2 260 true -32 wit inspect 4.8 230 unknown 0 wit inspect 3.0 210 false(unreach-call) 1 wit inspect .59 19 - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 290 29 true -32 wit inspect 3.0 260 true -32 wit inspect 4.4 230 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .60 19 - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 290 28 true -32 wit inspect 3.6 260 true -32 wit inspect 4.2 230 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .61 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 290 31 true -32 wit inspect 4.0 260 true -32 wit inspect 4.4 230 unknown 0 wit inspect 2.9 190 false(unreach-call) 1 wit inspect .61 19 - wit inspect - wit inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 290 32 true -32 wit inspect 3.5 260 true -32 wit inspect 4.8 230 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 280 30 true -32 wit inspect 3.6 270 true -32 wit inspect 4.6 220 unknown 0 wit inspect 2.9 180 false(unreach-call) 1 wit inspect .59 19 - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 27 true -32 wit inspect 3.1 260 true -32 wit inspect 5.8 230 unknown 0 wit inspect 2.8 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 3.3 290 29 true -32 wit inspect 3.3 260 true -32 wit inspect 4.6 220 unknown 0 wit inspect 2.7 210 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 3.3 280 27 true -32 wit inspect 3.4 260 true -32 wit inspect 5.0 230 unknown 0 wit inspect 2.9 180 true -32 wit inspect .59 19 - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 28 true -32 wit inspect 3.3 250 true -32 wit inspect 4.4 220 unknown 0 wit inspect 2.9 180 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) 0 wit inspect 3.1 280 31 true -32 wit inspect 3.4 260 true -32 wit inspect 4.8 220 unknown 0 wit inspect 2.8 190 true -32 wit inspect .63 19 - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 27 true -32 wit inspect 3.7 260 true -32 wit inspect 4.1 210 unknown 0 wit inspect 2.6 180 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 280 28 true -32 wit inspect 3.2 260 true -32 wit inspect 4.4 220 unknown 0 wit inspect 2.9 190 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 280 26 true -32 wit inspect 3.5 260 true -32 wit inspect 4.4 210 unknown 0 wit inspect 2.7 180 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 30 true -32 wit inspect 3.1 250 true -32 wit inspect 4.3 210 unknown 0 wit inspect 2.7 180 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 29 true -32 wit inspect 3.6 260 true -32 wit inspect 4.4 210 unknown 0 wit inspect 2.8 180 false(unreach-call) 1 wit inspect .61 18 - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 3.1 280 29 true -32 wit inspect 3.3 260 true -32 wit inspect 4.9 220 unknown 0 wit inspect 2.8 180 true -32 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 3.2 280 27 true -32 wit inspect 3.3 260 true -32 wit inspect 4.6 220 unknown 0 wit inspect 2.9 210 true -32 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 3.3 290 29 true -32 wit inspect 3.2 260 true -32 wit inspect 4.7 210 unknown 0 wit inspect 2.8 180 true -32 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 3.1 280 31 true -32 wit inspect 3.3 260 true -32 wit inspect 4.2 220 unknown 0 wit inspect 2.7 210 true -32 wit inspect .58 18 - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 3.3 280 27 true -32 wit inspect 3.3 260 true -32 wit inspect 4.3 210 unknown 0 wit inspect 3.1 230 true -32 wit inspect .58 18 - wit inspect - wit inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 3.1 280 29 true -32 wit inspect 4.3 260 true -32 wit inspect 4.3 220 unknown 0 wit inspect 3.1 230 true -32 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 28 true -32 wit inspect 3.1 250 true -32 wit inspect 4.4 230 unknown 0 wit inspect 2.8 180 false(unreach-call) 1 wit inspect .61 18 - wit inspect - wit inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 280 28 true -32 wit inspect 3.4 260 true -32 wit inspect 5.4 290 unknown 0 wit inspect 2.8 180 false(unreach-call) 1 wit inspect .57 19 - wit inspect - wit inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 280 28 true -32 wit inspect 3.3 260 true -32 wit inspect 4.7 230 unknown 0 wit inspect 1.9 210 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 3.3 280 33 true -32 wit inspect 3.2 260 true -32 wit inspect 4.7 230 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .61 18 - wit inspect - wit inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 280 31 true -32 wit inspect 3.2 260 true -32 wit inspect 4.7 220 unknown 0 wit inspect 2.8 180 false(unreach-call) 1 wit inspect .58 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 3.3 290 29 true -32 wit inspect 3.7 260 true -32 wit inspect 4.4 220 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 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 250 true 2 wit inspect 5.1 270
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0 250 true 2 wit inspect 5.6 260
recursive-simple/fibo_10_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.2 280 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2 260 true 2 wit inspect 4.9 220
recursive-simple/fibo_15_true-unreach-call.c false(unreach-call) -16 wit inspect 3.2 280 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1 260 true 2 wit inspect 4.6 220
recursive-simple/fibo_20_true-unreach-call.c false(unreach-call) -16 wit inspect 3.5 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 260 true 2 wit inspect 4.6 230
recursive-simple/fibo_25_true-unreach-call.c false(unreach-call) -16 wit inspect 3.2 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1 250 true 2 wit inspect 4.9 230
recursive-simple/fibo_2calls_10_true-unreach-call.c false(unreach-call) -16 wit inspect 3.3 290 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0 260 true 2 wit inspect 6.3 220
recursive-simple/fibo_2calls_15_true-unreach-call.c false(unreach-call) -16 wit inspect 3.4 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7 260 true 2 wit inspect 5.6 230
recursive-simple/fibo_2calls_20_true-unreach-call.c false(unreach-call) -16 wit inspect 3.4 290 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6 260 true 2 wit inspect 5.8 230
recursive-simple/fibo_2calls_25_true-unreach-call.c false(unreach-call) -16 wit inspect 3.2 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3 260 true 2 wit inspect 5.9 220
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7 250 true 2 wit inspect 12   370
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.5 290 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5 260 true 2 wit inspect 5.0 220
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.3 290 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 260 true 2 wit inspect 5.1 230
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.5 290 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5 260 true 2 wit inspect 4.6 230
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.5 290 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 260 true 2 wit inspect 4.3 220
recursive-simple/fibo_5_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.3 290 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2 260 true 2 wit inspect 5.6 220
recursive-simple/fibo_7_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.1 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2 260 true 2 wit inspect 5.7 220
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.1 270 28 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2 250 true 2 wit inspect 12   420
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.1 270 25 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.1 240 true 2 wit inspect 11   500
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.1 270 28 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2 250 true 2 wit inspect 13   490
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.2 290 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 260 true 2 wit inspect 4.8 220
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5 250 true 2 wit inspect 9.6 350
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 2.9 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1 250 true 2 wit inspect 6.4 270
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.0 270 28 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3 250 true 2 wit inspect 6.9 260
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.1 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5 260 true 2 wit inspect 4.2 220
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.1 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 260 true 2 wit inspect 4.4 210
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.2 280 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1 260 true 2 wit inspect 5.6 210
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.3 280 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2 260 true 2 wit inspect 4.2 220
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.2 280 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9 260 true 2 wit inspect 4.6 220
recursive-simple/sum_10x0_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.1 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0 260 true 2 wit inspect 5.4 230
recursive-simple/sum_15x0_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.3 280 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6 280 true 2 wit inspect 5.1 230
recursive-simple/sum_20x0_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.2 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2 260 true 2 wit inspect 4.6 230
recursive-simple/sum_25x0_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.3 280 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4 270 true 2 wit inspect 4.5 230
recursive-simple/sum_2x3_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.2 280 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6 260 true 2 wit inspect 4.5 230
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c false(unreach-call) -16 wit inspect 3.2 290 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2 260 true 2 wit inspect 4.7 230
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 -640 310 27000 2800 44 -1408 150 11000 44 -1342 210   10000 44 0 120 8500 44 -386 26   810 52 92 190 13000 52 104 300 13000
    correct results 39 48 120 11000 1100 0 2 2 9.2 460 0 30 30 18   550 46 92 170 12000 52 104 300 13000
        correct true 9 18 27 2400 230 0 0 0 0 46 92 170 12000 52 104 300 13000
        correct false 30 30 98 8500 890 0 2 2 9.2 460 0 30 30 18   550 0 0
    correct-unconfimed results 14 0 45 3900 400 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 14 0 45 3900 400 0 0 0 0 0 0
    incorrect results 43 -688 140 12000 1300 44 -1408 150 11000 42 -1344 200   9600 0 13 -416 7.8 240 0 0
        incorrect true 0 44 -1408 150 11000 42 -1344 200   9600 0 13 -416 7.8 240 0 0
        incorrect false 43 -688 140 12000 1300 0 0 0 0 0 0
score (96 tasks, max score: 148) -640 -1408 -1342 0 -386 92 104
Run set cpa-bam-slicing.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Recursive