Tool VerifierIntegerAssignmentPrograms File not exits 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*
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-03 03:42:11 CET 2017-12-03 04:30:19 CET 2017-12-03 04:52:11 CET 2017-12-03 04:56:53 CET 2017-12-03 05:05:18 CET 2017-12-03 04:20:47 CET 2017-12-03 04:35:31 CET
Run set viap.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-viap.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-viap.sv-comp18-correctness-witness.ReachSafety-Recursive
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/viap.2017-12-03_0342.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/viap.2017-12-03_0342.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/viap.2017-12-03_0342.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/viap.2017-12-03_0342.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/viap.2017-12-03_0342.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/viap.2017-12-03_0342.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 120   780 1200 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 10   100 130 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 2.1  180 error (2) 0 wit inspect .75   18    - wit inspect - wit inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 7.8 110 110 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 110   220 1400 error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   100 11000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 48 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   93 11000 error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0021 .29 - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 110   470 1600 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .028 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c true 2 wit inspect 22   160 290 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 18     500  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 110   600 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .027 5.0
recursive/Ackermann04_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 120   190 1800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 42 error (2) 0 wit inspect .018 4.8
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 120   370 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 46 error (2) 0 wit inspect .031 4.8
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 110   390 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .023 4.8
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 110   270 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .023 4.8
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c true 2 wit inspect 16   130 160 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 20     550  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 8.3 110 120 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .022 4.8
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 110   160 1500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .023 4.8
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 110   470 1200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 97   170 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .020 4.9
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c unknown 0 wit inspect 19   150 220 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .023 4.9
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 21   170 280 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .021 4.8
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 120   830 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .024 4.8
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (1) 0 wit inspect 13   120 150 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 45 error (2) 0 wit inspect .023 4.8
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 13   130 190 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 true 2 wit inspect 6.3   260  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 13   130 190 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 true 2 wit inspect 33     790  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.9 92 100 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 4.3   240   unknown 0 wit inspect 2.7  180 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 6.5 92 88 true -32 wit inspect 3.9  250 false(unreach-call) 1 wit inspect 4.9   220   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.2 98 87 false(unreach-call) 1 wit inspect 11    350 timeout 0 wit inspect 97     6600   unknown 0 wit inspect 4.7  220 false(unreach-call) 1 wit inspect .70   24    - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 9.4 420 130 false(unreach-call) 1 wit inspect 45    1500 out of memory 0 wit inspect 59     7000   unknown 0 wit inspect 10    500 false(unreach-call) 1 wit inspect 1.2    76    - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 35   4000 370 timeout 0 wit inspect 96    2500 out of memory 0 wit inspect 75     7000   timeout 0 wit inspect 97    2500 false(unreach-call) 1 wit inspect 8.8    680    - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 0 wit inspect 11   1200 130 timeout 0 wit inspect 98    5500 timeout 0 wit inspect 96     6100   timeout 0 wit inspect 98    5500 out of memory 0 wit inspect 78      7000    - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect 8.7 110 120 false(unreach-call) 1 wit inspect 7.0  350 timeout 0 wit inspect 96     5700   unknown 0 wit inspect 4.3  220 false(unreach-call) 1 wit inspect .64   24    - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 11   420 150 false(unreach-call) 1 wit inspect 22    1300 timeout 0 wit inspect 97     7000   unknown 0 wit inspect 11    350 false(unreach-call) 1 wit inspect 1.3    76    - wit inspect - wit inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 35   4000 320 timeout 0 wit inspect 94    7000 timeout 0 wit inspect 93     7000   timeout 0 wit inspect 96    2400 false(unreach-call) 1 wit inspect 8.5    680    - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 0 wit inspect 12   1200 160 timeout 0 wit inspect 98    5500 timeout 0 wit inspect 98     6200   timeout 0 wit inspect 98    5500 out of memory 0 wit inspect 77      7000    - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.5 92 130 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 5.1   250   unknown 0 wit inspect 3.8  190 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.5 92 110 false(unreach-call) 1 wit inspect 4.6  270 false(unreach-call) 1 wit inspect 15     430   unknown 0 wit inspect 2.9  190 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.5 92 110 false(unreach-call) 1 wit inspect 4.8  270 false(unreach-call) 1 wit inspect 20     920   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.5 92 120 false(unreach-call) 1 wit inspect 5.4  270 false(unreach-call) 1 wit inspect 47     1800   unknown 0 wit inspect 3.2  190 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 8.5 92 110 false(unreach-call) 1 wit inspect 7.0  300 timeout 0 wit inspect 98     3800   unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .60   20    - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.1 92 86 false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 24     890   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.2 92 94 false(unreach-call) 1 wit inspect 6.1  280 timeout 0 wit inspect 96     4500   unknown 0 wit inspect 3.5  220 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.8 92 140 false(unreach-call) 1 wit inspect 3.4  260 true -32 wit inspect 5.7   260   unknown 0 wit inspect 2.8  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.5 92 110 false(unreach-call) 1 wit inspect 3.3  270 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .59   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 7.5 92 90 false(unreach-call) 1 wit inspect 4.5  260 true -32 wit inspect 4.9   260   unknown 0 wit inspect 3.4  190 true -32 wit inspect .66   18    - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.2 92 96 false(unreach-call) 1 wit inspect 2.7  270 false(unreach-call) 1 wit inspect 4.4   390   unknown 0 wit inspect 2.2  210 false(unreach-call) 1 wit inspect .68   19    - wit inspect - wit inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.2 92 82 false(unreach-call) 1 wit inspect 5.1  270 false(unreach-call) 1 wit inspect 12     470   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.2 92 87 false(unreach-call) 1 wit inspect 4.5  280 false(unreach-call) 1 wit inspect 12     630   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.1 92 92 false(unreach-call) 1 wit inspect 6.8  280 false(unreach-call) 1 wit inspect 17     830   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.1 92 100 false(unreach-call) 1 wit inspect 4.5  260 false(unreach-call) 1 wit inspect 5.0   270   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 7.5 92 98 timeout 0 wit inspect 91    2400 true -32 wit inspect 5.0   260   unknown 0 wit inspect 2.8  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 7.7 92 97 false(unreach-call) 1 wit inspect 6.9  420 true -32 wit inspect 7.8   260   unknown 0 wit inspect 2.8  180 true -32 wit inspect .63   18    - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 7.5 92 95 false(unreach-call) 1 wit inspect 4.7  270 true -32 wit inspect 7.7   260   unknown 0 wit inspect 2.7  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 7.7 92 95 false(unreach-call) 1 wit inspect 15    670 true -32 wit inspect 5.0   260   unknown 0 wit inspect 2.7  170 true -32 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 7.6 92 97 false(unreach-call) 1 wit inspect 4.0  290 true -32 wit inspect 7.3   260   unknown 0 wit inspect 2.9  180 true -32 wit inspect .71   18    - wit inspect - wit inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 7.4 92 89 false(unreach-call) 1 wit inspect 4.2  260 true -32 wit inspect 5.4   260   unknown 0 wit inspect 2.9  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.6 95 95 false(unreach-call) 1 wit inspect 5.3  270 false(unreach-call) 1 wit inspect 9.7   370   unknown 0 wit inspect 3.3  230 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.6 92 110 false(unreach-call) 1 wit inspect 5.5  270 false(unreach-call) 1 wit inspect 12     460   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.6 92 110 false(unreach-call) 1 wit inspect 3.4  280 false(unreach-call) 1 wit inspect 15     590   unknown 0 wit inspect 3.4  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 7.6 92 95 false(unreach-call) 1 wit inspect 7.0  280 false(unreach-call) 1 wit inspect 14     880   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.6 92 120 false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .65   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.9 120 94 timeout 0 wit inspect 92    2300 timeout 0 wit inspect 97     6900   unknown 0 wit inspect 22    1500 false(unreach-call) 1 wit inspect .67   26    - wit inspect - wit inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c unknown 0 wit inspect 8.7 110 110 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .022 5.0
recursive-simple/afterrec_true-unreach-call_true-termination.c unknown 0 wit inspect 7.3 110 100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .021 4.8
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect 14   200 160 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.2  260 true 2 wit inspect 63     4500  
recursive-simple/fibo_15_true-unreach-call.c true 1 wit inspect 14   210 150 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 5.1  250 timeout 0 wit inspect 960     5400  
recursive-simple/fibo_20_true-unreach-call.c true 1 wit inspect 19   210 230 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 8.8  820 timeout 0 wit inspect 960     6100  
recursive-simple/fibo_25_true-unreach-call.c true 1 wit inspect 25   1200 330 - wit inspect - wit inspect - wit inspect - wit inspect out of java memory 0 wit inspect 730    5500 out of memory 0 wit inspect 130     7000  
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect 15   200 180 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.0  250 true 2 wit inspect 110     4500  
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect 15   200 210 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.3  250 timeout 0 wit inspect 960     5700  
recursive-simple/fibo_2calls_20_true-unreach-call.c true 1 wit inspect 29   220 360 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 9.5  820 timeout 0 wit inspect 960     5700  
recursive-simple/fibo_2calls_25_true-unreach-call.c true 1 wit inspect 17   1200 240 - wit inspect - wit inspect - wit inspect - wit inspect out of java memory 0 wit inspect 600    5500 out of memory 0 wit inspect 170     7000  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 14   170 170 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 11     370  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect 15   200 190 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 20     550  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect 15   200 200 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.5  250 true 2 wit inspect 21     510  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect 15   200 190 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.1  250 true 2 wit inspect 34     760  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect 15   200 190 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  260 true 2 wit inspect 61     1700  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect 14   200 160 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 14     540  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect 14   200 200 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 true 2 wit inspect 20     780  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 1 wit inspect 15   210 230 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 4.9
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 1 wit inspect 14   200 180 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .020 5.0
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 1 wit inspect 15   210 190 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .043 5.0
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 14   170 170 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 13     500  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 1 wit inspect 14   210 150 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .024 5.0
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 1 wit inspect 12   160 160 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .023 4.8
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 1 wit inspect 12   160 150 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 4.8
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 14   210 180 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 18     540  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 15   210 200 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.8  250 true 2 wit inspect 24     620  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 15   210 210 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 33     750  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect 17   220 240 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 38     830  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 12   170 160 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 13     440  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect 12   220 180 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 21     550  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect 13   220 170 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 true 2 wit inspect 24     690  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c unknown 0 wit inspect 110   340 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .023 4.9
recursive-simple/sum_25x0_true-unreach-call_true-termination.c unknown 0 wit inspect 110   420 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .021 4.9
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect 11   140 150 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 9.6   350  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 110   280 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .025 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 91 4500 30000 55000 44 -34 800   37000 44 -237 1300 80000 44 0 530 25000 44 -229 190   16000 52 2 1400   20000 52 44 4800 59000
    correct results 57 79 650 16000 8300 30 30 220   11000 19 19 240 10000 0 27 27 34   2000 1 2 3.9 250 22 44 630 22000
        correct true 22 44 320 4100 4100 0 0 0 0 1 2 3.9 250 22 44 630 22000
        correct false 35 35 330 12000 4100 30 30 220   11000 19 19 240 10000 0 27 27 34   2000 0 0
    correct-unconfimed results 15 12 230 7000 3000 0 0 0 0 0 0
        correct-unconfirmed true 12 12 200 4400 2600 0 0 0 0 0 0
        correct-unconfirmed false 3 0 30 2500 380 0 0 0 0 0 0
    incorrect results 0 2 -64 7.6 510 8 -256 49 2100 0 8 -256 5.0 150 0 0
        incorrect true 0 2 -64 7.6 510 8 -256 49 2100 0 8 -256 5.0 150 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 91 -34 -237 0 -229 2 44
Run set viap.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-viap.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-viap.sv-comp18-correctness-witness.ReachSafety-Recursive