Tool CPAchecker 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]
Date of execution 2017-12-05 07:52:24 CET 2017-12-05 13:10:09 CET 2017-12-05 13:34:02 CET 2017-12-05 13:37:41 CET 2017-12-05 13:41:35 CET 2017-12-05 12:37:13 CET 2017-12-05 13:13:01 CET
Run set interpchecker.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-Recursive
Options -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/interpchecker.2017-12-05_0752.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 2.9 260 26 true -32 wit inspect 3.2 260 true -32 wit inspect 6.5 270 unknown 0 wit inspect 2.8 180 true -32 wit inspect .57 18 - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.3 270 29 true -32 wit inspect 3.2 260 false(unreach-call) 1 wit inspect 5.3 250 unknown 0 wit inspect 3.0 190 false(unreach-call) 1 wit inspect .61 18 - wit inspect - wit inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 2.8 270 25 true -32 wit inspect 2.1 260 true -32 wit inspect 4.1 230 unknown 0 wit inspect 2.7 180 true -32 wit inspect .57 18 - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 2.8 260 29 true -32 wit inspect 3.2 260 false(unreach-call) 1 wit inspect 5.7 260 unknown 0 wit inspect 2.6 180 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 2.7 270 25 true -32 wit inspect 3.1 260 true -32 wit inspect 7.7 310 unknown 0 wit inspect 2.7 220 true -32 wit inspect .58 18 - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 2.8 270 29 true -32 wit inspect 3.2 260 true -32 wit inspect 8.0 300 unknown 0 wit inspect 2.9 180 true -32 wit inspect .61 18 - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 2.8 260 25 true -32 wit inspect 3.1 260 true -32 wit inspect 6.5 270 unknown 0 wit inspect 2.8 180 true -32 wit inspect .60 18 - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c false(unreach-call) -16 wit inspect 2.9 260 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 260 true 2 wit inspect 10   350
recursive/Ackermann03_true-unreach-call_true-no-overflow.c false(unreach-call) -16 wit inspect 3.1 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7 260 true 2 wit inspect 6.7 270
recursive/Ackermann04_true-unreach-call_true-no-overflow.c false(unreach-call) -16 wit inspect 2.8 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4 260 true 2 wit inspect 6.8 270
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.2 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1 250 true 2 wit inspect 9.4 370
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.1 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1 260 true 2 wit inspect 7.0 430
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 2.9 260 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9 260 true 2 wit inspect 26   650
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c false(unreach-call) -16 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2 260 true 2 wit inspect 8.7 400
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2 250 true 2 wit inspect 9.1 290
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0 260 true 2 wit inspect 9.8 310
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2 260 true 2 wit inspect 6.6 270
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 2.9 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3 260 true 2 wit inspect 40   740
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c false(unreach-call) -16 wit inspect 3.6 270 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6 260 true 2 wit inspect 15   540
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.0 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6 270 true 2 wit inspect 8.4 310
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.1 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5 260 true 2 wit inspect 100   1000
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 3.0 280 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6 260 true 2 wit inspect 4.6 230
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7 260 true 2 wit inspect 5.1 260
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c false(unreach-call) -16 wit inspect 2.9 280 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0 250 true 2 wit inspect 9.6 370
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 280 25 false(unreach-call) 1 wit inspect 3.0 260 false(unreach-call) 1 wit inspect 4.2 240 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 270 26 false(unreach-call) 1 wit inspect 3.0 260 false(unreach-call) 1 wit inspect 4.1 220 unknown 0 wit inspect 2.6 190 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 2.8 280 21 true -32 wit inspect 3.3 250 true -32 wit inspect 7.7 310 unknown 0 wit inspect 2.6 180 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 2.7 270 27 true -32 wit inspect 3.1 250 true -32 wit inspect 7.4 300 unknown 0 wit inspect 2.9 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 2.7 270 27 true -32 wit inspect 3.1 260 true -32 wit inspect 8.2 310 unknown 0 wit inspect 2.6 210 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect 2.9 270 25 true -32 wit inspect 3.0 260 true -32 wit inspect 7.5 310 unknown 0 wit inspect 2.7 190 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 3.0 270 26 true -32 wit inspect 3.1 260 true -32 wit inspect 14   460 unknown 0 wit inspect 2.9 210 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 3.1 270 27 true -32 wit inspect 3.4 260 true -32 wit inspect 11   450 unknown 0 wit inspect 2.7 180 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 3.1 280 28 true -32 wit inspect 3.3 260 true -32 wit inspect 13   460 unknown 0 wit inspect 2.7 210 false(unreach-call) 1 wit inspect .58 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect 2.9 270 27 true -32 wit inspect 2.4 260 true -32 wit inspect 11   450 unknown 0 wit inspect 2.8 190 false(unreach-call) 1 wit inspect .58 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.0 270 25 true -32 wit inspect 3.1 270 false(unreach-call) 1 wit inspect 4.9 260 unknown 0 wit inspect 2.8 180 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.9 270 29 true -32 wit inspect 3.2 260 false(unreach-call) 1 wit inspect 17   520 unknown 0 wit inspect 2.7 210 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 3.0 260 28 true -32 wit inspect 3.2 260 true -32 wit inspect 16   500 unknown 0 wit inspect 2.9 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 2.9 270 24 true -32 wit inspect 3.4 260 true -32 wit inspect 11   440 unknown 0 wit inspect 2.9 190 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.0 280 28 true -32 wit inspect 3.2 260 true -32 wit inspect 10   440 unknown 0 wit inspect 2.9 210 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.0 260 27 true -32 wit inspect 3.1 260 true -32 wit inspect 8.2 310 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 270 25 true -32 wit inspect 3.4 270 true -32 wit inspect 7.6 290 unknown 0 wit inspect 2.7 210 false(unreach-call) 1 wit inspect .62 20 - wit inspect - wit inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 2.8 270 29 true -32 wit inspect 3.2 260 false(unreach-call) 1 wit inspect 5.1 260 unknown 0 wit inspect 2.9 180 true -32 wit inspect .65 23 - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.9 270 25 true -32 wit inspect 3.2 260 false(unreach-call) 1 wit inspect 8.8 360 unknown 0 wit inspect 2.7 210 false(unreach-call) 1 wit inspect .57 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 2.9 270 28 true -32 wit inspect 3.0 250 false(unreach-call) 1 wit inspect 5.7 270 unknown 0 wit inspect 2.8 210 true -32 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 2.8 280 24 true -32 wit inspect 3.0 250 true -32 wit inspect 7.9 310 unknown 0 wit inspect 2.6 180 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 280 25 true -32 wit inspect 3.0 260 true -32 wit inspect 7.8 320 unknown 0 wit inspect 2.7 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.7 270 26 true -32 wit inspect 3.4 280 true -32 wit inspect 7.5 310 unknown 0 wit inspect 2.9 210 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 2.9 270 22 true -32 wit inspect 3.3 260 true -32 wit inspect 7.6 320 unknown 0 wit inspect 2.6 210 false(unreach-call) 1 wit inspect .58 18 - wit inspect - wit inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.9 280 27 true -32 wit inspect 3.1 250 true -32 wit inspect 7.6 310 unknown 0 wit inspect 2.7 180 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 2.8 280 26 true -32 wit inspect 3.0 260 true -32 wit inspect 8.3 350 unknown 0 wit inspect 2.7 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 2.9 270 26 true -32 wit inspect 3.0 250 true -32 wit inspect 8.3 350 unknown 0 wit inspect 2.6 180 true -32 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 2.7 270 26 true -32 wit inspect 3.1 260 true -32 wit inspect 8.5 350 unknown 0 wit inspect 2.7 190 true -32 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 2.8 280 23 true -32 wit inspect 3.2 260 true -32 wit inspect 9.3 340 unknown 0 wit inspect 2.7 180 true -32 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 2.8 260 25 true -32 wit inspect 3.0 260 true -32 wit inspect 8.8 350 unknown 0 wit inspect 2.7 190 true -32 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 2.8 280 24 true -32 wit inspect 3.0 260 false(unreach-call) 1 wit inspect 6.9 270 unknown 0 wit inspect 2.7 180 true -32 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 260 23 true -32 wit inspect 3.0 260 true -32 wit inspect 8.1 320 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .60 19 - wit inspect - wit inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.7 260 26 true -32 wit inspect 3.1 260 true -32 wit inspect 8.1 320 unknown 0 wit inspect 2.7 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 260 27 true -32 wit inspect 3.0 250 true -32 wit inspect 8.2 330 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.7 270 25 true -32 wit inspect 3.1 260 true -32 wit inspect 7.9 330 unknown 0 wit inspect 2.6 190 false(unreach-call) 1 wit inspect .56 18 - wit inspect - wit inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.7 270 26 true -32 wit inspect 3.3 270 false(unreach-call) 1 wit inspect 5.3 270 unknown 0 wit inspect 2.8 180 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 2.9 270 27 true -32 wit inspect 3.1 260 false(unreach-call) 1 wit inspect 4.5 240 unknown 0 wit inspect 2.8 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 3.0 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7 250 true 2 wit inspect 5.1 250
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2 250 true 2 wit inspect 4.8 260
recursive-simple/fibo_10_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.8 260 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8 260 true 2 wit inspect 8.0 300
recursive-simple/fibo_15_true-unreach-call.c false(unreach-call) -16 wit inspect 2.9 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2 260 true 2 wit inspect 11   310
recursive-simple/fibo_20_true-unreach-call.c false(unreach-call) -16 wit inspect 2.8 270 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5 260 true 2 wit inspect 7.3 300
recursive-simple/fibo_25_true-unreach-call.c false(unreach-call) -16 wit inspect 2.9 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 260 true 2 wit inspect 7.5 300
recursive-simple/fibo_2calls_10_true-unreach-call.c false(unreach-call) -16 wit inspect 2.9 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8 260 true 2 wit inspect 16   550
recursive-simple/fibo_2calls_15_true-unreach-call.c false(unreach-call) -16 wit inspect 3.0 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9 260 true 2 wit inspect 11   460
recursive-simple/fibo_2calls_20_true-unreach-call.c false(unreach-call) -16 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2 260 true 2 wit inspect 14   450
recursive-simple/fibo_2calls_25_true-unreach-call.c false(unreach-call) -16 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9 270 true 2 wit inspect 13   450
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 4.4 290 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0 250 true 2 wit inspect 9.1 370
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.9 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 260 true 2 wit inspect 18   510
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.0 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0 260 true 2 wit inspect 16   510
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.9 260 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6 260 true 2 wit inspect 14   510
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 260 true 2 wit inspect 14   460
recursive-simple/fibo_5_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.9 280 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1 250 true 2 wit inspect 7.6 300
recursive-simple/fibo_7_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.7 260 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5 260 true 2 wit inspect 7.7 300
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.0 280 25 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5 250 true 2 wit inspect 10   430
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0 250 true 2 wit inspect 12   510
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.0 280 28 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9 250 true 2 wit inspect 12   480
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.9 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5 260 true 2 wit inspect 11   490
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.0 280 29 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0 250 true 2 wit inspect 8.6 350
recursive-simple/id_b3_o5_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.3 250 true 2 wit inspect 6.7 270
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.0 280 25 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0 250 true 2 wit inspect 6.2 260
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5 250 true 2 wit inspect 8.1 320
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0 260 true 2 wit inspect 7.8 310
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.7 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6 280 true 2 wit inspect 8.4 320
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.8 280 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1 260 true 2 wit inspect 8.1 320
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.8 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9 260 true 2 wit inspect 7.7 310
recursive-simple/sum_10x0_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3 280 true 2 wit inspect 7.6 310
recursive-simple/sum_15x0_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.7 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 250 true 2 wit inspect 11   320
recursive-simple/sum_20x0_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.8 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 260 true 2 wit inspect 8.7 320
recursive-simple/sum_25x0_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1 280 true 2 wit inspect 5.6 320
recursive-simple/sum_2x3_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5 250 true 2 wit inspect 8.7 350
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c false(unreach-call) -16 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3 270 true 2 wit inspect 9.6 300
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 -636 280 26000 2500 44 -1342 140   11000 44 -1012 360 14000 44 0 120 8600 44 -385 26   810 52 92 180 13000 52 104 630 20000
    correct results 43 52 130 12000 1100 2 2 6.0 520 12 12 77 3400 0 31 31 18   570 46 92 170 12000 52 104 630 20000
        correct true 9 18 28 2500 250 0 0 0 0 46 92 170 12000 52 104 630 20000
        correct false 34 34 98 9200 890 2 2 6.0 520 12 12 77 3400 0 31 31 18   570 0 0
    correct-unconfimed results 10 0 28 2700 250 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 10 0 28 2700 250 0 0 0 0 0 0
    incorrect results 43 -688 120 12000 1100 42 -1344 130   11000 32 -1024 280 11000 0 13 -416 7.7 240 0 0
        incorrect true 0 42 -1344 130   11000 32 -1024 280 11000 0 13 -416 7.7 240 0 0
        incorrect false 43 -688 120 12000 1100 0 0 0 0 0 0
score (96 tasks, max score: 148) -636 -1342 -1012 0 -385 92 104
Run set interpchecker.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-Recursive