Tool CBMC 5.8 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-11-30 11:20:26 CET 2017-12-01 07:26:01 CET 2017-12-01 07:56:00 CET 2017-12-01 08:08:00 CET 2017-12-01 08:15:34 CET 2017-12-01 04:22:29 CET 2017-12-01 07:31:28 CET
Run set cbmc.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Recursive
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cbmc.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) 1 wit inspect 1.9  94 21   timeout 0 wit inspect 91    2500 false(unreach-call) 1 wit inspect 13     370   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .29 33 2.3 false(unreach-call) 1 wit inspect 4.4  280 false(unreach-call) 1 wit inspect 6.0   260   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .25 33 2.2 true -32 wit inspect 3.3  260 true -32 wit inspect 7.4   290   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .26 33 2.2 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.8   250   unknown 0 wit inspect 3.0  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) 1 wit inspect .90 42 9.4 timeout 0 wit inspect 91    2400 false(unreach-call) 1 wit inspect 19     630   unknown 0 wit inspect 7.7  270 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    270 3100   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .25 33 2.1 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.4   250   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (42) 0 wit inspect 870    380 2700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .022 4.9
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (42) 0 wit inspect 870    370 2500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .050 4.8
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (42) 0 wit inspect 870    370 2400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .019 4.8
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 880    8600 8300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .033 4.8
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 880    14000 7600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.9
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    8700 6500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .018 4.9
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (42) 0 wit inspect 870    260 2800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .022 4.8
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 1.3  33 12   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  260 true 2 wit inspect 35     2700  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    280 3600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .018 4.9
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    1400 3500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 4.9
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    450 2500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .034 4.9
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (42) 0 wit inspect 870    340 2800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.8
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    3300 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 4.9
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    190 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .025 4.8
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    810 3000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .023 4.8
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 2.5  35 26   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 6.1   260  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 2.5  35 27   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 29     750  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .27 33 2.0 true -32 wit inspect 3.0  250 false(unreach-call) 1 wit inspect 5.1   240   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .23 33 2.3 true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 5.9   270   unknown 0 wit inspect 3.0  180 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 1.1  35 12   timeout 0 wit inspect 92    2800 timeout 0 wit inspect 97     5300   timeout 0 wit inspect 92    3500 false(unreach-call) 1 wit inspect .85   20    - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 3.4  73 41   exception 0 wit inspect 12    410 out of memory 0 wit inspect 78     7000   timeout 0 wit inspect 9.9  500 false(unreach-call) 1 wit inspect 1.5    41    - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 170    770 1200   exception 0 wit inspect 40    2500 out of memory 0 wit inspect 88     7000   timeout 0 wit inspect 37    2500 false(unreach-call) 1 wit inspect 8.8    300    - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c error (42) 0 wit inspect 870    480 4300   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .90 47 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .77 33 7.6 timeout 0 wit inspect 91    2600 timeout 0 wit inspect 98     5300   timeout 0 wit inspect 92    3500 false(unreach-call) 1 wit inspect .68   21    - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 3.4  80 35   exception 0 wit inspect 13    580 timeout 0 wit inspect 90     7000   timeout 0 wit inspect 8.4  510 false(unreach-call) 1 wit inspect 1.3    43    - wit inspect - wit inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 170    840 1300   exception 0 wit inspect 38    2800 out of memory 0 wit inspect 88     7000   timeout 0 wit inspect 52    3000 false(unreach-call) 1 wit inspect 8.6    320    - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c error (42) 0 wit inspect 870    480 6000   error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0013 .35 - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .26 33 2.1 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 8.2   270   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .72   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .24 33 1.9 true -32 wit inspect 6.1  290 false(unreach-call) 1 wit inspect 22     480   unknown 0 wit inspect 5.1  210 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .25 33 2.1 true -32 wit inspect 9.4  460 false(unreach-call) 1 wit inspect 29     670   unknown 0 wit inspect 5.0  260 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .25 33 2.4 true -32 wit inspect 28    930 false(unreach-call) 1 wit inspect 32     870   unknown 0 wit inspect 9.9  430 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .64 33 7.5 timeout 0 wit inspect 91    2900 timeout 0 wit inspect 97     4600   unknown 0 wit inspect 49    2500 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .62 33 6.5 false(unreach-call) 1 wit inspect 12    430 false(unreach-call) 1 wit inspect 22     620   unknown 0 wit inspect 5.7  230 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .65 33 6.1 false(unreach-call) 1 wit inspect 45    2100 true -32 wit inspect 44     1600   unknown 0 wit inspect 16    800 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .25 33 2.3 false(unreach-call) 1 wit inspect 4.2  270 false(unreach-call) 1 wit inspect 6.2   260   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .25 33 2.3 true -32 wit inspect 4.6  260 false(unreach-call) 1 wit inspect 7.6   270   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .62   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 .26 33 2.0 false(unreach-call) 1 wit inspect 5.0  280 false(unreach-call) 1 wit inspect 6.3   260   unknown 0 wit inspect 3.5  190 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.0  33 10   false(unreach-call) 1 wit inspect 4.7  270 true -32 wit inspect 4.5   220   unknown 0 wit inspect 3.4  210 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 1.4  35 14   false(unreach-call) 1 wit inspect 5.3  280 true -32 wit inspect 5.3   230   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .69   19    - wit inspect - wit inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.7  33 20   false(unreach-call) 1 wit inspect 6.4  290 true -32 wit inspect 6.1   240   unknown 0 wit inspect 4.8  220 false(unreach-call) 1 wit inspect .67   19    - wit inspect - wit inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.1  33 20   false(unreach-call) 1 wit inspect 6.8  350 true -32 wit inspect 4.3   240   unknown 0 wit inspect 4.9  230 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .64 33 5.7 false(unreach-call) 1 wit inspect 4.1  260 false(unreach-call) 1 wit inspect 7.9   270   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 47    410 490   exception 0 wit inspect 8.9  370 true -32 wit inspect 13     1100   timeout 0 wit inspect 7.0  290 false(unreach-call) 1 wit inspect .97   30    - wit inspect - wit inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 3.5  51 36   timeout 0 wit inspect 91    2200 true -32 wit inspect 5.1   350   unknown 0 wit inspect 12    490 false(unreach-call) 1 wit inspect .62   20    - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .99 33 9.4 false(unreach-call) 1 wit inspect 4.3  380 true -32 wit inspect 5.6   220   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .67   19    - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 3.3  47 35   timeout 0 wit inspect 96    2400 true -32 wit inspect 7.7   480   unknown 0 wit inspect 22    1500 false(unreach-call) 1 wit inspect .64   21    - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 1.8  33 18   false(unreach-call) 1 wit inspect 19    660 true -32 wit inspect 4.6   240   unknown 0 wit inspect 4.8  220 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .62 33 5.7 false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 4.9   240   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.0  33 10   false(unreach-call) 1 wit inspect 3.1  270 true -32 wit inspect 4.6   220   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.4  33 17   false(unreach-call) 1 wit inspect 5.5  270 true -32 wit inspect 5.7   240   unknown 0 wit inspect 3.9  220 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.8  33 17   false(unreach-call) 1 wit inspect 7.4  300 true -32 wit inspect 5.1   250   unknown 0 wit inspect 3.9  220 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.3  33 22   false(unreach-call) 1 wit inspect 7.4  360 true -32 wit inspect 4.7   250   unknown 0 wit inspect 5.1  230 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .24 33 2.2 false(unreach-call) 1 wit inspect 3.5  280 false(unreach-call) 1 wit inspect 5.8   270   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .74   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 .26 33 2.4 false(unreach-call) 1 wit inspect 3.8  270 false(unreach-call) 1 wit inspect 4.5   230   unknown 0 wit inspect 3.1  180 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect .41 33 4.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 5.2   270  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect .39 33 5.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.2   260  
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect 1.3  33 13   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  260 true 2 wit inspect 53     4500  
recursive-simple/fibo_15_true-unreach-call.c true 1 wit inspect 4.2  40 58   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  260 timeout 0 wit inspect 960     5400  
recursive-simple/fibo_20_true-unreach-call.c true 1 wit inspect 340    400 2700   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 5.6  410 timeout 0 wit inspect 960     6100  
recursive-simple/fibo_25_true-unreach-call.c error (42) 0 wit inspect 870    470 4000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .018 4.9
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect .95 33 9.2 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.2  260 true 2 wit inspect 140     4500  
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect 4.3  41 55   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 timeout 0 wit inspect 960     5700  
recursive-simple/fibo_2calls_20_true-unreach-call.c true 1 wit inspect 370    420 2200   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 5.6  420 timeout 0 wit inspect 960     6100  
recursive-simple/fibo_2calls_25_true-unreach-call.c error (42) 0 wit inspect 870    480 5300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .023 4.9
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect .44 33 3.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.3   360  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect .41 33 4.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 16     550  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect .41 33 4.4 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 23     610  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect .45 33 4.2 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4  240 true 2 wit inspect 26     690  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect .88 33 7.9 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  240 true 2 wit inspect 54     1800  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect .79 33 9.2 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 14     470  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect .86 33 8.2 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 true 2 wit inspect 19     780  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    5200 5000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    5200 6200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.9
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    5200 7500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .033 4.8
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .43 33 3.3 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.2  250 true 2 wit inspect 13     460  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    10000 3900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .024 4.9
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    5200 7300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 4.9
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    11000 4000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 4.9
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 1.2  33 11   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  240 true 2 wit inspect 13     510  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 1.6  35 16   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 21     620  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 1.9  33 25   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.1  250 true 2 wit inspect 28     730  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect 2.4  33 25   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 35     840  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .82 33 7.7 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4  250 true 2 wit inspect 10     430  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect 1.2  33 11   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 18     550  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect 1.6  33 14   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 25     670  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect 2.0  33 18   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 38     770  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect 2.4  33 24   - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 53     940  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect .41 33 3.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  260 true 2 wit inspect 11     360  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    290 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.9
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 96 95 24000 89000 140000 44 -235 980 36000 44 -461 980 56000 44 0 520 26000 44 41 44 1400 52 6 120 8600 52 50 4500 49000
    correct results 66 91 460 4300 3700 21 21 160 8400 19 19 220 7000 0 41 41 44 1400 3 6 11 770 25 50 700 25000
        correct true 25 50 30 830 300 0 0 0 0 3 6 11 770 25 50 700 25000
        correct false 41 41 430 3500 3400 21 21 160 8400 19 19 220 7000 0 41 41 44 1400 0 0
    correct-unconfimed results 4 4 720 900 5000 0 0 0 0 0 0
        correct-unconfirmed true 4 4 720 900 5000 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 8 -256 60 3000 15 -480 130 6200 0 0 0 0
        incorrect true 0 8 -256 60 3000 15 -480 130 6200 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 95 -235 -461 0 41 6 50
Run set cbmc.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Recursive