Tool ULTIMATE Taipan 0.1.23-3204b741 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-12-02 17:23:13 CET 2017-12-03 07:22:17 CET 2017-12-03 07:45:29 CET 2017-12-03 07:47:53 CET 2017-12-03 07:50:34 CET 2017-12-03 06:47:45 CET 2017-12-03 07:25:40 CET
Run set utaipan.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-Recursive
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/utaipan.2017-12-02_1723.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 7.5 380 54 false(unreach-call) 1 wit inspect 7.8  420 false(unreach-call) 1 wit inspect 5.6   310   unknown 0 wit inspect 3.0  210 true -32 wit inspect .57   19    - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 6.0 290 49 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 4.6   250   unknown 0 wit inspect 2.8  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 5.8 300 48 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.0   260   unknown 0 wit inspect 2.9  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 4.2 250 32 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 23   810 200 false(unreach-call) 1 wit inspect 45    1200 false(unreach-call) 1 wit inspect 17     590   unknown 0 wit inspect 4.3  220 true -32 wit inspect .62   18    - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 44   1600 370 timeout 0 wit inspect 92    2700 timeout 0 wit inspect 98     4000   unknown 0 wit inspect 30    1800 true -32 wit inspect .59   20    - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 4.1 240 32 false(unreach-call) 1 wit inspect 3.1  270 false(unreach-call) 1 wit inspect 4.7   230   unknown 0 wit inspect 2.7  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 910   13000 6200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .048 4.8
recursive/Ackermann03_true-unreach-call_true-no-overflow.c true 2 wit inspect 120   4900 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 26     750  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c true 2 wit inspect 100   4900 960 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4  250 true 2 wit inspect 20     690  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 8.5 480 75 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 8.3   320  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1500 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .017 4.8
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1600 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .043 4.8
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c true 2 wit inspect 26   870 210 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.9  250 true 2 wit inspect 14     540  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 480   11000 5000 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 31     3000  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 140   4600 1900 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 38     3300  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.4 420 61 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 8.5   280  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 910   14000 3900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 wit inspect 900   6000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .018 4.8
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.6 390 63 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 8.5   350  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   6900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .048 4.9
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   12000 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .047 4.9
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 4.9 290 40 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 6.2   270  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .045 4.8
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.7 290 41 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.5   240   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.3 240 33 true -32 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 7.1   330   unknown 0 wit inspect 2.6  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c timeout 0 wit inspect 910   13000 7600 error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .031 4.9 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0037 .33 - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c timeout 0 wit inspect 910   13000 6900 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .037 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0045 .30 - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c timeout 0 wit inspect 910   13000 7000 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0046 .26 - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c timeout 0 wit inspect 910   13000 6600 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .83 50 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c timeout 0 wit inspect 910   12000 7600 error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .83 52 error (invalid witness file) 0 wit inspect .0040 .28 - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c timeout 0 wit inspect 910   14000 6200 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0042 .26 - wit inspect - wit inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 0 wit inspect 910   13000 6700 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0029 .35 - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 0 wit inspect 910   13000 7300 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .040 4.9 error (invalid witness file) 0 wit inspect .86 51 error (invalid witness file) 0 wit inspect .0038 .28 - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 6.3 300 56 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.6   250   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 17   610 140 false(unreach-call) 1 wit inspect 6.3  340 false(unreach-call) 1 wit inspect 5.6   320   unknown 0 wit inspect 3.6  220 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 19   700 170 false(unreach-call) 1 wit inspect 9.9  470 false(unreach-call) 1 wit inspect 25     820   unknown 0 wit inspect 5.1  260 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 27   840 230 false(unreach-call) 1 wit inspect 22    880 false(unreach-call) 1 wit inspect 53     2500   unknown 0 wit inspect 8.3  340 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 110   3600 990 timeout 0 wit inspect 91    2900 timeout 0 wit inspect 98     4800   unknown 0 wit inspect 50    2500 false(unreach-call) 1 wit inspect .62   20    - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   610 98 false(unreach-call) 1 wit inspect 7.9  430 false(unreach-call) 1 wit inspect 18     660   unknown 0 wit inspect 4.4  220 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 25   970 210 false(unreach-call) 1 wit inspect 34    1700 false(unreach-call) 1 wit inspect 54     2000   unknown 0 wit inspect 14    500 false(unreach-call) 1 wit inspect .61   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 5.8 280 50 false(unreach-call) 1 wit inspect 3.4  270 false(unreach-call) 1 wit inspect 4.9   250   unknown 0 wit inspect 2.8  190 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 10   530 78 false(unreach-call) 1 wit inspect 3.4  270 false(unreach-call) 1 wit inspect 4.9   250   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   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 6.9 350 63 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 4.5   250   unknown 0 wit inspect 2.0  190 true -32 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 26   820 280 false(unreach-call) 1 wit inspect 3.7  270 true -32 wit inspect 4.4   220   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 69   1300 870 false(unreach-call) 1 wit inspect 4.0  270 true -32 wit inspect 4.9   230   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 180   1500 2200 false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 4.6   230   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 410   1500 6300 false(unreach-call) 1 wit inspect 4.6  270 true -32 wit inspect 4.6   240   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.7 570 89 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 4.6   230   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900   850 9900 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0044 .26 - wit inspect - wit inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900   900 11000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .039 4.8 error (invalid witness file) 0 wit inspect .87 51 error (invalid witness file) 0 wit inspect .0042 .31 - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 20   610 180 false(unreach-call) 1 wit inspect 3.8  270 true -32 wit inspect 4.3   220   unknown 0 wit inspect 2.8  190 true -32 wit inspect .57   19    - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900   830 12000 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0047 .26 - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 320   860 3700 false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 4.3   240   unknown 0 wit inspect 3.1  210 true -32 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.5 380 63 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 4.8   240   unknown 0 wit inspect 2.7  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 30   900 290 false(unreach-call) 1 wit inspect 3.4  260 true -32 wit inspect 4.5   250   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 80   1300 870 false(unreach-call) 1 wit inspect 4.0  270 true -32 wit inspect 4.6   250   unknown 0 wit inspect 3.1  220 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 210   1500 2500 false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 4.7   240   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 440   1400 6100 false(unreach-call) 1 wit inspect 4.9  280 true -32 wit inspect 4.6   250   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 6.4 310 57 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 4.8   260   unknown 0 wit inspect 2.9  200 false(unreach-call) 1 wit inspect .56   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 4.2 240 34 false(unreach-call) 1 wit inspect 3.1  270 false(unreach-call) 1 wit inspect 4.6   230   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect 4.6 280 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 4.8   250  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 4.7 280 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 4.9   260  
recursive-simple/fibo_10_true-unreach-call_true-termination.c timeout 0 wit inspect 910   13000 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .018 4.9
recursive-simple/fibo_15_true-unreach-call.c timeout 0 wit inspect 910   13000 7800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .048 4.8
recursive-simple/fibo_20_true-unreach-call.c timeout 0 wit inspect 910   13000 8000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8
recursive-simple/fibo_25_true-unreach-call.c timeout 0 wit inspect 910   13000 6500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 44 error (2) 0 wit inspect .018 4.8
recursive-simple/fibo_2calls_10_true-unreach-call.c timeout 0 wit inspect 900   13000 7800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .025 4.8
recursive-simple/fibo_2calls_15_true-unreach-call.c timeout 0 wit inspect 910   13000 7200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 5.0
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 wit inspect 900   13000 6300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .020 5.0
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 wit inspect 910   13000 6800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 8.6 450 80 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.6   370  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect 23   730 190 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 16     520  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect 24   770 230 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 20     600  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect 45   1100 450 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 24     760  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect 140   4600 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.5  270 true 2 wit inspect 43     1700  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect 18   660 170 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 13     560  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect 37   1200 310 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 18     800  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 9.3 470 79 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 9.6   420  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 11   550 85 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 11     490  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 10   540 97 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 11     490  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 13   670 130 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.0  250 true 2 wit inspect 11     490  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 6.4 300 49 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 8.6   350  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 7.5 370 62 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 4.4   260  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 7.8 370 71 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 6.2   260  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 28   900 270 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 14     540  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 73   1500 940 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 20     630  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 180   1300 2600 - 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 true 2 wit inspect 420   1500 5200 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 36     830  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 11   590 97 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 9.4   430  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect 29   900 300 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 19     560  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect 98   1500 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 22     690  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect 230   1400 2800 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  240 true 2 wit inspect 30     760  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect 480   1500 6200 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 47     890  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect 8.9 540 75 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 8.1   350  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 17   410 190 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 10     310  
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 104 29000 350000 290000 44 -68 410   18000 44 -299 490 22000 44 0 200 12000 44 -330 20   620 52 6 120   9700 52 72 620 25000
    correct results 68 104 5000 78000 59000 28 28 210   11000 21 21 250 11000 0 22 22 13   410 3 6 9.3 750 36 72 620 25000
        correct true 36 72 2800 53000 33000 0 0 0 0 3 6 9.3 750 36 72 620 25000
        correct false 32 32 2100 25000 26000 28 28 210   11000 21 21 250 11000 0 22 22 13   410 0 0
    correct-unconfimed results 1 0 44 1600 370 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 1 0 44 1600 370 0 0 0 0 0 0
    incorrect results 0 3 -96 8.9 770 10 -320 45 2400 0 11 -352 6.5 200 0 0
        incorrect true 0 3 -96 8.9 770 10 -320 45 2400 0 11 -352 6.5 200 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 104 -68 -299 0 -330 6 72
Run set utaipan.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-Recursive