Tool Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 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-12-01 19:46:39 CET 2017-12-01 22:34:51 CET 2017-12-01 23:03:48 CET 2017-12-01 23:06:19 CET 2017-12-01 23:09:14 CET 2017-12-01 22:04:37 CET 2017-12-01 22:38:34 CET
Run set map2check.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Recursive
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.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/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.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/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/map2check.2017-12-01_1946.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 .82 12 9.9 false(unreach-call) 1 wit inspect 6.2 280 true -32 wit inspect 8.0 270 unknown 0 wit inspect 3.7 210 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .69 12 9.0 false(unreach-call) 1 wit inspect 5.5 290 true -32 wit inspect 6.5 270 unknown 0 wit inspect 3.7 210 false(unreach-call) 1 wit inspect .66 18 - wit inspect - wit inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .38 12 4.2 false(unreach-call) 1 wit inspect 3.7 250 true -32 wit inspect 4.6 220 unknown 0 wit inspect 3.1 210 false(unreach-call) 1 wit inspect .61 18 - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .43 12 4.4 false(unreach-call) 1 wit inspect 3.4 260 false(unreach-call) 1 wit inspect 5.4 250 unknown 0 wit inspect 3.1 210 false(unreach-call) 1 wit inspect .67 18 - wit inspect - wit inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .62 12 9.4 false(unreach-call) 1 wit inspect 12   370 true -32 wit inspect 3.8 260 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .72 18 - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 1.1  12 14   false(unreach-call) 1 wit inspect 35   490 true -32 wit inspect 4.9 260 unknown 0 wit inspect 3.5 190 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .45 12 5.9 false(unreach-call) 1 wit inspect 3.4 260 false(unreach-call) 1 wit inspect 5.5 230 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 890    16 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .024 5.0
recursive/Ackermann03_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 890    16 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .028 5.0
recursive/Ackermann04_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 900    16 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .024 4.9
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 900    650 8200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.8
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 900    630 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .027 4.9
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 900    540 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 46 error (2) 0 wit inspect .023 4.8
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 890    13 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .024 4.9
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .29 11 3.6 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .024 4.9
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 890    13 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .024 4.8
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 900    120 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .024 4.8
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 900    190 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .026 4.8
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c unknown 0 wit inspect 900    190 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 5.0
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 890    92 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .023 4.8
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 890    33 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .023 5.0
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 890    12 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 45 error (2) 0 wit inspect .025 5.0
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 1.9  12 26   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 true 2 wit inspect 5.4   260  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 1.9  12 23   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 37     760  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .34 11 4.3 true -32 wit inspect 2.9 260 false(unreach-call) 1 wit inspect 6.9 260 unknown 0 wit inspect 3.2 180 false(unreach-call) 1 wit inspect .64 18 - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .34 11 3.8 true -32 wit inspect 3.9 260 false(unreach-call) 1 wit inspect 4.7 240 unknown 0 wit inspect 3.7 210 false(unreach-call) 1 wit inspect .62 18 - wit inspect - wit inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .35 11 3.9 true -32 wit inspect 4.9 260 true -32 wit inspect 8.2 330 unknown 0 wit inspect 2.1 210 false(unreach-call) 1 wit inspect .62 18 - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect .50 11 6.4 true -32 wit inspect 4.5 260 true -32 wit inspect 8.7 340 unknown 0 wit inspect 3.7 210 false(unreach-call) 1 wit inspect .69 18 - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 2.4  11 31   true -32 wit inspect 4.3 260 true -32 wit inspect 8.2 370 unknown 0 wit inspect 3.2 190 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 23    11 310   true -32 wit inspect 5.2 260 true -32 wit inspect 9.0 330 unknown 0 wit inspect 3.8 180 false(unreach-call) 1 wit inspect .62 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .36 11 5.0 true -32 wit inspect 5.7 270 true -32 wit inspect 5.0 230 unknown 0 wit inspect 3.8 210 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect .62 11 7.7 true -32 wit inspect 4.8 260 true -32 wit inspect 5.1 220 unknown 0 wit inspect 3.9 190 false(unreach-call) 1 wit inspect .59 19 - wit inspect - wit inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 3.5  11 43   true -32 wit inspect 5.1 260 true -32 wit inspect 4.8 230 unknown 0 wit inspect 3.5 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 36    11 490   true -32 wit inspect 4.3 260 true -32 wit inspect 4.9 230 unknown 0 wit inspect 3.7 210 false(unreach-call) 1 wit inspect .71 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .34 11 4.5 true -32 wit inspect 2.4 260 false(unreach-call) 1 wit inspect 5.4 260 unknown 0 wit inspect 3.0 210 false(unreach-call) 1 wit inspect .71 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .36 11 3.7 true -32 wit inspect 4.9 260 true -32 wit inspect 5.1 220 unknown 0 wit inspect 2.9 210 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 .34 11 3.8 true -32 wit inspect 4.6 260 true -32 wit inspect 7.3 230 unknown 0 wit inspect 3.3 190 false(unreach-call) 1 wit inspect .66 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .36 11 4.2 true -32 wit inspect 2.8 260 true -32 wit inspect 5.1 230 unknown 0 wit inspect 3.1 210 false(unreach-call) 1 wit inspect .76 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .34 11 4.8 true -32 wit inspect 5.2 280 true -32 wit inspect 5.0 220 unknown 0 wit inspect 3.6 210 false(unreach-call) 1 wit inspect .61 18 - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .31 11 4.1 true -32 wit inspect 5.0 260 true -32 wit inspect 5.8 330 unknown 0 wit inspect 3.9 210 false(unreach-call) 1 wit inspect .64 18 - wit inspect - wit inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .34 11 3.5 true -32 wit inspect 4.6 260 true -32 wit inspect 8.4 330 unknown 0 wit inspect 2.9 210 false(unreach-call) 1 wit inspect .67 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 .47 11 6.2 true -32 wit inspect 4.2 260 true -32 wit inspect 5.6 270 unknown 0 wit inspect 3.5 190 false(unreach-call) 1 wit inspect .61 18 - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .32 11 3.6 true -32 wit inspect 2.5 260 false(unreach-call) 1 wit inspect 9.1 350 unknown 0 wit inspect 3.4 180 false(unreach-call) 1 wit inspect .67 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 .52 12 6.3 false(unreach-call) 1 wit inspect 4.2 260 true -32 wit inspect 3.4 270 unknown 0 wit inspect 3.7 210 false(unreach-call) 1 wit inspect .58 19 - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .31 11 4.1 true -32 wit inspect 3.2 250 true -32 wit inspect 10   460 unknown 0 wit inspect 3.4 180 false(unreach-call) 1 wit inspect .58 18 - wit inspect - wit inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .32 11 4.3 true -32 wit inspect 4.2 260 true -32 wit inspect 11   460 unknown 0 wit inspect 3.3 190 false(unreach-call) 1 wit inspect .62 18 - wit inspect - wit inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .33 11 3.3 true -32 wit inspect 3.3 260 true -32 wit inspect 11   460 unknown 0 wit inspect 2.7 180 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 .31 11 3.3 true -32 wit inspect 4.4 260 true -32 wit inspect 11   460 unknown 0 wit inspect 2.0 190 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 .33 11 3.8 true -32 wit inspect 3.9 260 false(unreach-call) 1 wit inspect 8.9 320 unknown 0 wit inspect 2.6 180 false(unreach-call) 1 wit inspect .68 18 - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 180    210 1700   true -32 wit inspect 4.7 280 true -32 wit inspect 5.4 250 unknown 0 wit inspect 3.2 210 false(unreach-call) 1 wit inspect .58 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.0  13 59   true -32 wit inspect 4.0 260 true -32 wit inspect 3.5 260 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .69 18 - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .78 12 9.3 true -32 wit inspect 2.4 260 true -32 wit inspect 5.1 260 unknown 0 wit inspect 3.1 190 false(unreach-call) 1 wit inspect .58 18 - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 11    20 120   true -32 wit inspect 4.2 260 true -32 wit inspect 5.0 260 unknown 0 wit inspect 3.7 210 false(unreach-call) 1 wit inspect .73 18 - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 1.2  12 18   true -32 wit inspect 4.1 260 true -32 wit inspect 5.2 250 unknown 0 wit inspect 3.6 210 false(unreach-call) 1 wit inspect .59 19 - wit inspect - wit inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .50 11 5.7 true -32 wit inspect 4.2 270 true -32 wit inspect 5.0 260 unknown 0 wit inspect 3.6 210 false(unreach-call) 1 wit inspect .74 18 - wit inspect - wit inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .32 11 3.8 true -32 wit inspect 2.5 260 true -32 wit inspect 6.5 270 unknown 0 wit inspect 3.5 190 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .35 11 3.6 true -32 wit inspect 4.2 270 true -32 wit inspect 6.3 270 unknown 0 wit inspect 3.1 180 false(unreach-call) 1 wit inspect .76 18 - wit inspect - wit inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .31 11 4.2 true -32 wit inspect 4.1 260 true -32 wit inspect 4.8 270 unknown 0 wit inspect 2.8 180 false(unreach-call) 1 wit inspect .62 18 - wit inspect - wit inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .32 11 3.4 true -32 wit inspect 3.7 260 true -32 wit inspect 6.4 270 unknown 0 wit inspect 3.5 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 .31 11 3.6 true -32 wit inspect 4.3 270 false(unreach-call) 1 wit inspect 6.1 270 unknown 0 wit inspect 2.0 190 false(unreach-call) 1 wit inspect .73 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 .36 12 4.5 true -32 wit inspect 2.5 260 false(unreach-call) 1 wit inspect 4.5 240 unknown 0 wit inspect 3.5 210 false(unreach-call) 1 wit inspect .58 18 - wit inspect - wit inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect .32 11 3.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.1   270  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect .32 11 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.8   260  
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect .33 11 3.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 65     4500  
recursive-simple/fibo_15_true-unreach-call.c true 1 wit inspect .54 11 5.7 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.7  260 timeout 0 wit inspect 960     5400  
recursive-simple/fibo_20_true-unreach-call.c true 1 wit inspect 2.4  11 32   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 timeout 0 wit inspect 960     6000  
recursive-simple/fibo_25_true-unreach-call.c true 1 wit inspect 22    11 320   - 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_10_true-unreach-call.c true 2 wit inspect .35 11 5.2 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 130     4500  
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect .64 11 7.8 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  240 timeout 0 wit inspect 960     5500  
recursive-simple/fibo_2calls_20_true-unreach-call.c true 1 wit inspect 3.5  11 50   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 timeout 0 wit inspect 960     6200  
recursive-simple/fibo_2calls_25_true-unreach-call.c true 1 wit inspect 35    11 490   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 timeout 0 wit inspect 960     6100  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect .34 11 4.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 10     360  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect .33 11 4.7 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4  250 true 2 wit inspect 21     530  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect .33 11 4.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 26     660  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect .34 11 4.1 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 25     710  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect .37 11 4.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 72     1900  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect .32 11 3.4 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 14     560  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect .34 11 3.4 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 20     800  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 900    610 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .048 5.0
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 900    710 8500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .022 4.8
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 890    650 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .022 4.8
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .35 11 3.3 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 16     500  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 890    950 8200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .019 4.9
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 900    860 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .027 4.8
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 890    830 9300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect .33 11 3.4 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 15     550  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect .33 11 3.6 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 20     650  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect .33 11 4.3 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 34     730  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect .47 82 4.0 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 34     820  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .35 11 3.3 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 14     440  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect .34 11 4.2 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 23     550  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect .33 11 3.8 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  240 true 2 wit inspect 29     540  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect .31 11 4.1 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 32     790  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect .33 11 3.6 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 48     870  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect .33 11 3.8 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 11     370  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 900    760 8500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .023 4.8
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 96 98 19000 9000 230000 44 -1144 220 12000 44 -1111 280 13000 44 0 140 8800 44 44 28 810 52 6 110   8500 52 48 6500 58000
    correct results 68 92 290 1100 3100 8 8 73 2500 9 9 56 2400 0 44 44 28 810 3 6 9.4 750 24 48 710 23000
        correct true 24 48 11 340 140 0 0 0 0 3 6 9.4 750 24 48 710 23000
        correct false 44 44 280 710 3000 8 8 73 2500 9 9 56 2400 0 44 44 28 810 0 0
    correct-unconfimed results 6 6 65 67 900 0 0 0 0 0 0
        correct-unconfirmed true 6 6 65 67 900 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 36 -1152 150 9400 35 -1120 220 10000 0 0 0 0
        incorrect true 0 36 -1152 150 9400 35 -1120 220 10000 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 98 -1144 -1111 0 44 6 48
Run set map2check.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Recursive