Tool VeriAbs 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* [apollon020; apollon077; apollon078; apollon084; apollon149; apollon164] apollon* [apollon037; apollon065; apollon077; apollon078; apollon155; apollon159] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 18:04:04 CET 2017-12-03 04:46:33 CET 2017-12-03 06:08:30 CET 2017-12-03 06:21:09 CET 2017-12-03 06:27:12 CET 2017-12-03 03:55:53 CET 2017-12-03 04:55:47 CET
Run set veriabs.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Recursive
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/veriabs.2017-12-02_1804.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 670   190 2800 true -32 wit inspect 4.1  270 false(unreach-call) 1 wit inspect 11     370   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 580   2200 6600 true -32 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 3.4   250   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .60   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.2 220 65 error (invalid witness file) 0 wit inspect 2.3  170 true -32 wit inspect 4.9   230   error (invalid witness file) 0 wit inspect 2.5  180 error (1) 0 wit inspect .55   18    - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 7.9 250 66 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 4.9   250   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 670   160 3000 true -32 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 19     610   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 690   780 2800 true -32 wit inspect 4.1  270 timeout 0 wit inspect 96     4700   unknown 0 wit inspect 2.4  220 false(unreach-call) 1 wit inspect .63   20    - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 670   160 2900 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 3.5   240   unknown 0 wit inspect 1.9  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   4400 5300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .031 4.8
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   4400 5900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .024 4.8
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error 0 wit inspect 900   8300 5500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .019 5.0
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 610   2200 6700 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 8.5   320  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 610   2200 6700 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 true 2 wit inspect 430     4600  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error 0 wit inspect 7.6 160 73 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .018 5.0
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   3000 4500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .046 5.0
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.6 270 75 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.5  250 true 2 wit inspect 34     2800  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   3000 5500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .019 4.9
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   4000 5000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .48 43 error (2) 0 wit inspect .020 4.9
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   5800 7100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .021 5.0
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 wit inspect 900   3000 7500 - 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/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   2300 9600 - 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/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   3100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .017 4.9
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   8400 7200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.9
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c error 0 wit inspect 6.9 160 67 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .022 5.0
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c error 0 wit inspect 6.8 160 63 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .023 4.8
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c unknown 0 wit inspect 23   160 210 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .70 49 error (invalid witness file) 0 wit inspect .0035 .30 - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.0 220 67 true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 8.0   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.6 240 80 true -32 wit inspect 4.9  270 timeout 0 wit inspect 97     6600   unknown 0 wit inspect 3.9  230 false(unreach-call) 1 wit inspect .62   21    - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 11   210 120 true -32 wit inspect 8.5  490 out of memory 0 wit inspect 77     7000   unknown 0 wit inspect 6.7  360 false(unreach-call) 1 wit inspect 1.2    40    - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c error 0 wit inspect 250   240 2100 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c error 0 wit inspect 6.8 160 56 error (invalid witness file) 0 wit inspect .57 41 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 .29 - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect 7.7 240 69 true -32 wit inspect 2.9  270 timeout 0 wit inspect 97     5100   unknown 0 wit inspect 2.7  220 false(unreach-call) 1 wit inspect .64   20    - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 12   240 110 true -32 wit inspect 5.4  550 out of memory 0 wit inspect 85     7000   unknown 0 wit inspect 5.3  510 false(unreach-call) 1 wit inspect 1.3    41    - wit inspect - wit inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 0 wit inspect 900   270 5300 error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0027 .28 - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 0 wit inspect 900   270 6700 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.2 240 69 true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 6.1   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.6 240 68 true -32 wit inspect 3.5  250 false(unreach-call) 1 wit inspect 14     520   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.3 250 71 true -32 wit inspect 4.1  280 false(unreach-call) 1 wit inspect 46     2500   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .57   19    - wit inspect - wit inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.2 220 64 true -32 wit inspect 2.4  260 false(unreach-call) 1 wit inspect 27     890   unknown 0 wit inspect 2.2  210 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.1 250 71 true -32 wit inspect 4.0  270 timeout 0 wit inspect 97     4200   unknown 0 wit inspect 2.3  220 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.3 240 72 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 18     680   unknown 0 wit inspect 3.2  230 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.6 240 62 true -32 wit inspect 3.9  260 true -32 wit inspect 27     1300   unknown 0 wit inspect 3.0  210 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 8.0 240 73 true -32 wit inspect 3.7  250 false(unreach-call) 1 wit inspect 6.4   260   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.3 250 67 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.9   270   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .71   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 7.4 250 73 true -32 wit inspect 2.3  260 false(unreach-call) 1 wit inspect 5.0   280   unknown 0 wit inspect 2.1  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.4 240 64 true -32 wit inspect 3.5  250 true -32 wit inspect 4.4   220   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.5 240 65 true -32 wit inspect 3.9  260 true -32 wit inspect 4.6   230   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.4 240 68 true -32 wit inspect 3.5  260 true -32 wit inspect 4.6   230   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c error 0 wit inspect 6.7 160 61 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.1 240 68 true -32 wit inspect 2.3  260 false(unreach-call) 1 wit inspect 5.0   280   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c error 0 wit inspect 7.0 160 61 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect - wit inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c error 0 wit inspect 7.0 160 60 error (invalid witness file) 0 wit inspect .83 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 7.1 220 64 true -32 wit inspect 3.6  260 true -32 wit inspect 4.7   220   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c error 0 wit inspect 6.8 160 68 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .84 50 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 7.4 240 55 true -32 wit inspect 4.1  260 true -32 wit inspect 5.0   240   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 7.2 220 60 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 5.3   240   unknown 0 wit inspect 2.6  180 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 7.3 240 63 true -32 wit inspect 3.7  260 true -32 wit inspect 4.8   230   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.0 220 62 true -32 wit inspect 3.5  260 true -32 wit inspect 4.9   240   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.5 250 68 true -32 wit inspect 3.5  260 true -32 wit inspect 4.8   250   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c error 0 wit inspect 6.5 160 62 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.2 220 70 true -32 wit inspect 2.1  250 false(unreach-call) 1 wit inspect 6.1   280   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .59   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 7.3 250 62 true -32 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 2.0  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 7.9 270 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.1  250 true 2 wit inspect 3.8   260  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 7.5 270 64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.5   260  
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect 7.5 260 70 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 57     4500  
recursive-simple/fibo_15_true-unreach-call.c true 1 wit inspect 9.9 270 90 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 timeout 0 wit inspect 960     5400  
recursive-simple/fibo_20_true-unreach-call.c error 0 wit inspect 250   250 2300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .022 4.9
recursive-simple/fibo_25_true-unreach-call.c error 0 wit inspect 6.5 160 58 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.8
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect 7.8 270 57 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 120     4500  
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect 9.9 270 96 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4  250 timeout 0 wit inspect 960     5600  
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 wit inspect 900   260 5700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 wit inspect 900   270 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .020 4.9
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 8.2 270 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 9.1   370  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect 8.0 260 70 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 18     530  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect 7.8 280 66 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 true 2 wit inspect 23     630  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect 7.7 270 65 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 28     730  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect 7.8 270 70 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 34     1700  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect 7.5 260 69 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 14     540  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect 8.3 270 86 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.6  250 true 2 wit inspect 19     800  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error 0 wit inspect 7.5 160 78 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.9
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error 0 wit inspect 7.4 160 75 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .024 4.8
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error 0 wit inspect 7.6 160 79 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .018 4.8
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 7.6 270 60 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 12     490  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error 0 wit inspect 7.2 150 66 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 5.0
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error 0 wit inspect 6.9 160 66 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .020 4.9
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error 0 wit inspect 7.1 160 59 - 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-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 7.7 260 69 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 16     530  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 7.6 270 61 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.4  250 true 2 wit inspect 20     640  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 7.5 260 66 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 27     730  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c error 0 wit inspect 6.5 160 54 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .022 4.8
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 7.6 260 61 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 12     430  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect 7.7 260 60 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  240 true 2 wit inspect 16     540  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect 7.8 270 59 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.7  270 true 2 wit inspect 22     700  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect 7.4 260 60 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.6  250 true 2 wit inspect 35     790  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c error 0 wit inspect 6.7 160 64 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .024 4.8
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect 7.5 260 61 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 true 2 wit inspect 10     350  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c error 0 wit inspect 19   160 220 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .024 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 81 19000   75000 140000 44 -1056 130 9700 44 -302 820 47000 44 0 100 8000 44 33 22 680 52 6 96   7400 52 46 2900 39000
    correct results 56 79 4900   20000 35000 0 18 18 200 8700 0 33 33 21 660 3 6 10   740 23 46 970 28000
        correct true 23 46 1400   9900 15000 0 0 0 0 3 6 10   740 23 46 970 28000
        correct false 33 33 3500   10000 20000 0 18 18 200 8700 0 33 33 21 660 0 0
    correct-unconfimed results 3 2 27   750 250 0 0 0 0 0 0
        correct-unconfirmed true 2 2 20   530 190 0 0 0 0 0 0
        correct-unconfirmed false 1 0 7.2 220 65 0 0 0 0 0 0
    incorrect results 0 33 -1056 120 9100 10 -320 69 3400 0 0 0 0
        incorrect true 0 33 -1056 120 9100 10 -320 69 3400 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 81 -1056 -302 0 33 6 46
Run set veriabs.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Recursive