Tool skink 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* [apollon077; apollon078; apollon155] [apollon030; apollon077; apollon078] [apollon077; apollon078] 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 4, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33554 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 22:03:39 CET 2017-12-02 00:36:21 CET 2017-12-02 01:00:42 CET 2017-12-02 01:03:22 CET 2017-12-02 01:04:20 CET 2017-12-02 00:04:19 CET 2017-12-02 00:40:05 CET
Run set skink.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Recursive
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.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/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.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/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/skink.2017-12-01_2203.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 unknown 0 wit inspect 4.1 260 42 error (invalid witness file) 0 wit inspect .42 42 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0026 .30 - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 11   360 130 false(unreach-call) 1 wit inspect 4.9  270 false(unreach-call) 1 wit inspect 3.7   270   unknown 0 wit inspect 2.8  180 error (2) 0 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 7.0 320 59 true -32 wit inspect 3.4  260 true -32 wit inspect 3.0   230   unknown 0 wit inspect 2.9  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 5.7 330 49 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 5.4   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 3.9 250 33 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .87 48 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 3.8 250 34 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0039 .28 - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 4.1 240 36 error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0010 .27 - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 3.7 250 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .023 5.0
recursive/Ackermann03_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 4.0 250 39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 5.0
recursive/Ackermann04_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 3.9 320 40 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 5.0
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 210   670 2300 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  270 true 2 wit inspect 8.8   320  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1600 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 5.0
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 260   740 2600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .021 4.9
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 3.9 250 35 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .024 4.8
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 4.0 240 42 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 46 error (2) 0 wit inspect .019 4.9
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 3.8 250 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.8
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 3.8 250 35 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .019 4.8
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1500 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .020 4.9
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c unknown 0 wit inspect 4.8 300 44 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 5.0
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 34   730 380 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 11     350  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 210   740 2900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 42 error (2) 0 wit inspect .019 4.9
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 3.9 270 32 - 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/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 3.7 240 38 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .021 4.8
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 3.7 240 35 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.8
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c unknown 0 wit inspect 3.9 250 38 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c unknown 0 wit inspect 3.6 230 31 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c unknown 0 wit inspect 4.1 340 35 error (invalid witness file) 0 wit inspect .71 42 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0035 .28 - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c unknown 0 wit inspect 3.9 250 31 error (invalid witness file) 0 wit inspect .72 46 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .69 50 error (invalid witness file) 0 wit inspect .0033 .29 - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c unknown 0 wit inspect 3.9 250 33 error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c unknown 0 wit inspect 3.7 250 31 error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .70 52 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c unknown 0 wit inspect 4.2 270 37 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0035 .31 - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c unknown 0 wit inspect 4.2 270 35 error (invalid witness file) 0 wit inspect .42 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c unknown 0 wit inspect 4.1 270 34 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .70 50 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c unknown 0 wit inspect 4.1 270 36 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .68 51 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.4 320 43 false(unreach-call) 1 wit inspect 4.0  260 true -32 wit inspect 3.3   230   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c unknown 0 wit inspect 4.0 270 41 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c unknown 0 wit inspect 4.0 270 34 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c unknown 0 wit inspect 4.3 270 39 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c unknown 0 wit inspect 4.3 270 42 error (invalid witness file) 0 wit inspect .67 45 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .85 48 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c unknown 0 wit inspect 3.8 250 35 error (invalid witness file) 0 wit inspect .41 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c unknown 0 wit inspect 3.9 240 38 error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .030 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0036 .28 - wit inspect - wit inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 4.2 260 39 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0035 .28 - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c unknown 0 wit inspect 3.9 250 35 error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 3.8 260 37 error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.9 290 42 false(unreach-call) 1 wit inspect 3.6  270 true -32 wit inspect 4.1   220   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.7 290 39 false(unreach-call) 1 wit inspect 2.8  270 true -32 wit inspect 2.9   220   unknown 0 wit inspect 1.8  180 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 5.0 290 45 false(unreach-call) 1 wit inspect 3.7  270 true -32 wit inspect 3.1   220   unknown 0 wit inspect 2.6  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 5.0 290 43 false(unreach-call) 1 wit inspect 3.9  270 true -32 wit inspect 4.1   210   unknown 0 wit inspect 2.7  190 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 4.8 290 46 false(unreach-call) 1 wit inspect 3.5  270 true -32 wit inspect 5.0   210   unknown 0 wit inspect 2.6  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 5.3 310 49 timeout 0 wit inspect 91    2500 true -32 wit inspect 3.8   260   unknown 0 wit inspect 2.6  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 5.1 290 43 false(unreach-call) 1 wit inspect 5.0  440 true -32 wit inspect 3.4   260   unknown 0 wit inspect 2.7  180 true -32 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 5.1 290 47 false(unreach-call) 1 wit inspect 2.5  270 true -32 wit inspect 5.3   260   unknown 0 wit inspect 1.9  180 true -32 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 5.0 300 46 false(unreach-call) 1 wit inspect 8.0  670 true -32 wit inspect 3.9   260   unknown 0 wit inspect 1.9  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) 1 wit inspect 5.0 280 50 false(unreach-call) 1 wit inspect 4.5  290 true -32 wit inspect 5.2   260   unknown 0 wit inspect 2.6  180 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 5.2 300 47 false(unreach-call) 1 wit inspect 4.3  260 true -32 wit inspect 5.0   260   unknown 0 wit inspect 1.9  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.0 300 45 false(unreach-call) 1 wit inspect 3.4  270 true -32 wit inspect 5.1   220   unknown 0 wit inspect 2.6  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 5.0 300 46 false(unreach-call) 1 wit inspect 2.7  270 true -32 wit inspect 3.7   220   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.2 320 44 false(unreach-call) 1 wit inspect 4.7  290 true -32 wit inspect 4.6   220   unknown 0 wit inspect 1.9  180 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 5.2 300 44 false(unreach-call) 1 wit inspect 4.3  270 true -32 wit inspect 3.7   210   unknown 0 wit inspect 2.0  180 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 5.1 330 45 false(unreach-call) 1 wit inspect 3.5  260 true -32 wit inspect 3.6   230   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .56   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 5.0 290 43 false(unreach-call) 1 wit inspect 3.4  250 true -32 wit inspect 3.0   230   unknown 0 wit inspect 2.1  180 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect 4.1 260 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.2   260  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 3.9 240 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 5.2   260  
recursive-simple/fibo_10_true-unreach-call_true-termination.c unknown 0 wit inspect 4.0 240 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8
recursive-simple/fibo_15_true-unreach-call.c unknown 0 wit inspect 3.9 250 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.9
recursive-simple/fibo_20_true-unreach-call.c unknown 0 wit inspect 3.9 240 40 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .021 5.0
recursive-simple/fibo_25_true-unreach-call.c unknown 0 wit inspect 3.4 250 31 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.9
recursive-simple/fibo_2calls_10_true-unreach-call.c unknown 0 wit inspect 4.0 270 44 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9
recursive-simple/fibo_2calls_15_true-unreach-call.c unknown 0 wit inspect 4.0 260 42 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .021 4.9
recursive-simple/fibo_2calls_20_true-unreach-call.c unknown 0 wit inspect 3.8 270 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8
recursive-simple/fibo_2calls_25_true-unreach-call.c unknown 0 wit inspect 4.1 270 39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .020 5.0
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 4.6 280 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.3   370  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c unknown 0 wit inspect 4.1 270 37 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .019 4.8
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c unknown 0 wit inspect 4.2 280 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .024 5.0
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c unknown 0 wit inspect 3.8 260 35 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c unknown 0 wit inspect 3.9 270 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .019 4.8
recursive-simple/fibo_5_true-unreach-call_true-termination.c unknown 0 wit inspect 3.8 240 39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .018 4.8
recursive-simple/fibo_7_true-unreach-call_true-termination.c unknown 0 wit inspect 3.9 240 32 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 5.0
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 3.6 260 34 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .47 43 error (2) 0 wit inspect .024 4.8
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 4.3 260 35 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .48 45 error (2) 0 wit inspect .020 4.8
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 3.9 250 39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c unknown 0 wit inspect 4.0 250 37 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 4.0 250 38 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .023 5.0
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 3.8 240 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.9
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 3.8 240 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .024 5.0
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 3.9 240 38 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 16     510  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 3.7 240 36 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4  250 true 2 wit inspect 19     640  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 3.8 240 39 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.0  250 true 2 wit inspect 27     750  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect 3.4 230 31 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 37     810  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 3.6 240 35 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.4  250 true 2 wit inspect 11     430  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect 3.7 240 34 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.0  240 true 2 wit inspect 21     550  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect 3.9 240 35 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 29     680  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect 3.7 240 33 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 34     760  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect 3.8 240 34 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.8  250 true 2 wit inspect 48     910  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect 3.8 240 34 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 9.5   360  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.2 240 42 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 11     320  
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 51 2900 30000 31000 44 -13 180   9400 44 -606 85   5100 44 0 67 5000 44 -211 12   390 52 6 73   5600 52 32 300 8500
    correct results 35 51 400 11000 4200 19 19 77   5700 2 2 9.1 520 0 13 13 7.6 240 3 6 9.8 760 16 32 300 8300
        correct true 16 32 290 4800 3200 0 0 0 0 3 6 9.8 760 16 32 300 8300
        correct false 19 19 100 5800 940 19 19 77   5700 2 2 9.1 520 0 13 13 7.6 240 0 0
    correct-unconfimed results 2 0 12 630 110 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 2 0 12 630 110 0 0 0 0 0 0
    incorrect results 0 1 -32 3.4 260 19 -608 76   4400 0 7 -224 4.0 130 0 0
        incorrect true 0 1 -32 3.4 260 19 -608 76   4400 0 7 -224 4.0 130 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 51 -13 -606 0 -211 6 32
Run set skink.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Recursive