Tool 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:29:20 CET 2017-12-01 08:07:14 CET 2017-12-01 08:15:38 CET 2017-12-01 08:19:10 CET 2017-12-01 04:11:27 CET 2017-12-01 07:35:08 CET
Run set cpa-seq.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Recursive
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-seq.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 4.6 290 44 false(unreach-call) 1 wit inspect 3.9  280 false(unreach-call) 1 wit inspect 6.0   320   unknown 0 wit inspect 3.3  180 false(unreach-call) 1 wit inspect .63   19    - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.7 290 32 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 3.0  190 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 2.8 260 25 false(unreach-call) 1 wit inspect 3.2  260 true -32 wit inspect 5.0   230   unknown 0 wit inspect 3.5  180 false(unreach-call) 1 wit inspect .83   18    - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.3 270 31 false(unreach-call) 1 wit inspect 3.5  280 false(unreach-call) 1 wit inspect 5.6   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 7.4 380 70 false(unreach-call) 1 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 25     940   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .63   19    - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 22   500 270 false(unreach-call) 1 wit inspect 6.0  310 timeout 0 wit inspect 96     4400   unknown 0 wit inspect 4.2  220 false(unreach-call) 1 wit inspect .64   21    - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.2 280 30 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.1   230   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c true 2 wit inspect 4.9 290 41 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 true 2 wit inspect 13     500  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   3100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.9
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   6700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .021 4.9
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .023 4.9
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   3700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.9
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   14000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.8
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   1500 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 46 error (2) 0 wit inspect .020 5.0
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 5.7 420 47 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 35     2700  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   4400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .030 4.9
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 3.5 290 32 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 8.9   280  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .021 4.9
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 wit inspect 900   1400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.9
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 4.6 300 40 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 8.9   340  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   730 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .019 4.9
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c exception 0 wit inspect 5.1 310 42 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .024 4.8
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   8400 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 250 25 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 5.1   250   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.7 260 24 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.5   240   unknown 0 wit inspect 2.7  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 6.2 390 52 false(unreach-call) 1 wit inspect 8.3  380 timeout 0 wit inspect 97     5400   unknown 0 wit inspect 5.2  220 false(unreach-call) 1 wit inspect .69   25    - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 30   1500 290 false(unreach-call) 1 wit inspect 37    2000 timeout 0 wit inspect 96     6300   unknown 0 wit inspect 22    1000 false(unreach-call) 1 wit inspect 1.9    94    - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c timeout 0 wit inspect 960   10000 7100 error (invalid witness file) 0 wit inspect .59 44 error (invalid witness file) 0 wit inspect 3.5   200   error (invalid witness file) 0 wit inspect .84 50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c out of memory 0 wit inspect 220   15000 1900 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .77 48 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect 6.4 400 54 false(unreach-call) 1 wit inspect 8.5  360 timeout 0 wit inspect 96     5300   unknown 0 wit inspect 5.0  220 false(unreach-call) 1 wit inspect .70   25    - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 27   1500 230 false(unreach-call) 1 wit inspect 33    1500 timeout 0 wit inspect 94     7000   unknown 0 wit inspect 17    700 false(unreach-call) 1 wit inspect 2.3    94    - wit inspect - wit inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 0 wit inspect 960   10000 7100 error (invalid witness file) 0 wit inspect .69 45 error (invalid witness file) 0 wit inspect 3.2   190   error (invalid witness file) 0 wit inspect .90 51 error (invalid witness file) 0 wit inspect .0041 .30 - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c out of memory 0 wit inspect 230   15000 1900 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 27 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 5.9   250   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 300 32 false(unreach-call) 1 wit inspect 3.8  270 false(unreach-call) 1 wit inspect 6.4   330   unknown 0 wit inspect 3.6  180 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.1 300 39 false(unreach-call) 1 wit inspect 4.2  270 out of memory 0 wit inspect 71     7000   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.4 310 34 false(unreach-call) 1 wit inspect 4.4  280 false(unreach-call) 1 wit inspect 44     1300   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.2 330 43 false(unreach-call) 1 wit inspect 6.6  310 timeout 0 wit inspect 98     4600   unknown 0 wit inspect 4.6  220 false(unreach-call) 1 wit inspect .71   21    - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.8 300 32 false(unreach-call) 1 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 25     980   unknown 0 wit inspect 3.1  210 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 4.3 310 41 false(unreach-call) 1 wit inspect 5.3  290 timeout 0 wit inspect 97     2700   unknown 0 wit inspect 4.6  230 false(unreach-call) 1 wit inspect .63   20    - wit inspect - wit inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 3.9 300 29 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 6.1   270   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.8 300 32 false(unreach-call) 1 wit inspect 3.5  270 false(unreach-call) 1 wit inspect 5.4   250   unknown 0 wit inspect 3.0  190 false(unreach-call) 1 wit inspect .70   19    - wit inspect - wit inspect
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 3.6 300 35 false(unreach-call) 1 wit inspect 2.3  260 false(unreach-call) 1 wit inspect 6.3   250   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.7 300 35 false(unreach-call) 1 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 6.9   390   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.8 300 32 false(unreach-call) 1 wit inspect 4.8  270 false(unreach-call) 1 wit inspect 9.8   470   unknown 0 wit inspect 4.1  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.8 310 32 false(unreach-call) 1 wit inspect 5.0  280 false(unreach-call) 1 wit inspect 18     710   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 310 37 false(unreach-call) 1 wit inspect 5.5  280 false(unreach-call) 1 wit inspect 19     930   unknown 0 wit inspect 4.5  220 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 280 29 false(unreach-call) 1 wit inspect 3.7  280 false(unreach-call) 1 wit inspect 5.1   270   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 120   4700 1200 exception 0 wit inspect 11    390 timeout 0 wit inspect 98     6000   timeout 0 wit inspect 8.4  310 false(unreach-call) 1 wit inspect 1.1    45    - wit inspect - wit inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 9.0 510 77 false(unreach-call) 1 wit inspect 15    620 timeout 0 wit inspect 97     7000   unknown 0 wit inspect 8.3  330 false(unreach-call) 1 wit inspect .63   21    - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 3.8 300 34 false(unreach-call) 1 wit inspect 4.4  270 false(unreach-call) 1 wit inspect 8.2   420   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 13   730 100 false(unreach-call) 1 wit inspect 30    1400 timeout 0 wit inspect 96     6400   unknown 0 wit inspect 15    500 false(unreach-call) 1 wit inspect .68   24    - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 4.2 310 36 false(unreach-call) 1 wit inspect 6.2  280 false(unreach-call) 1 wit inspect 15     690   unknown 0 wit inspect 4.5  220 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 3.5 280 29 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 6.1   250   unknown 0 wit inspect 3.1  190 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.9 300 29 false(unreach-call) 1 wit inspect 2.9  270 false(unreach-call) 1 wit inspect 6.8   390   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 310 37 false(unreach-call) 1 wit inspect 4.6  270 false(unreach-call) 1 wit inspect 11     490   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 310 40 false(unreach-call) 1 wit inspect 5.6  280 false(unreach-call) 1 wit inspect 17     600   unknown 0 wit inspect 4.1  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 310 35 false(unreach-call) 1 wit inspect 5.8  290 false(unreach-call) 1 wit inspect 18     880   unknown 0 wit inspect 3.9  220 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.6 290 31 false(unreach-call) 1 wit inspect 4.4  260 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 3.4 290 31 false(unreach-call) 1 wit inspect 3.3  250 false(unreach-call) 1 wit inspect 5.7   250   unknown 0 wit inspect 2.8  180 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 2.3 240 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.8   320  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 2.4 250 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.3   260  
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect 6.4 460 56 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.2  270 true 2 wit inspect 55     4500  
recursive-simple/fibo_15_true-unreach-call.c true 1 wit inspect 36   2100 500 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 timeout 0 wit inspect 960     5400  
recursive-simple/fibo_20_true-unreach-call.c timeout 0 wit inspect 910   3900 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .020 4.9
recursive-simple/fibo_25_true-unreach-call.c timeout 0 wit inspect 960   5000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .019 4.9
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect 7.7 470 59 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 130     4500  
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect 54   2100 690 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 timeout 0 wit inspect 960     6100  
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 wit inspect 910   3900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.9
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 wit inspect 960   5200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .020 4.9
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 2.6 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 11     360  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect 3.8 290 30 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 16     550  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect 4.0 290 35 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 21     610  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect 4.2 290 33 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 28     750  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect 5.6 370 51 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 55     1700  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect 3.7 300 31 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 14     550  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect 4.4 300 40 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 19     650  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.9 290 34 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 11     430  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.7 290 31 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 12     490  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.6 280 32 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 13     470  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 3.7 290 35 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 12     490  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.4 290 28 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 9.0   330  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.4 290 32 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 6.5   260  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.5 290 32 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 6.7   270  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 3.6 290 29 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 14     520  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 3.7 290 32 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 22     640  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 3.8 290 29 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 30     740  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect 3.8 300 36 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 36     810  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 3.6 300 35 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 12     440  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect 4.0 300 33 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  260 true 2 wit inspect 17     560  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect 4.1 300 37 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 25     700  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect 4.3 300 39 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 35     770  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect 4.8 300 37 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 59     880  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect 3.5 290 31 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 9.3   360  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.8 300 33 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 7.9   300  
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 96 108 17000 150000 210000 44 6 280   16000 44 -4 1400   76000 44 0 200 10000 44 40 29 950 52 6 130   9500 52 66 2700 40000
    correct results 73 106 490 30000 4500 38 38 270   15000 28 28 310   13000 0 40 40 29 950 3 6 9.3 740 33 66 770 28000
        correct true 33 66 130 10000 1200 0 0 0 0 3 6 9.3 740 33 66 770 28000
        correct false 40 40 360 20000 3400 38 38 270   15000 28 28 310   13000 0 40 40 29 950 0 0
    correct-unconfimed results 2 2 91 4200 1200 0 0 0 0 0 0
        correct-unconfirmed true 2 2 91 4200 1200 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 1 -32 3.0 260 1 -32 5.0 230 0 0 0 0
        incorrect true 0 1 -32 3.0 260 1 -32 5.0 230 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 108 6 -4 0 40 6 66
Run set cpa-seq.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Recursive