Tool 2LS 0.6.0 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:32:03 CET 2017-12-01 08:01:50 CET 2017-12-01 08:11:41 CET 2017-12-01 08:15:34 CET 2017-12-01 04:23:32 CET 2017-12-01 07:36:49 CET
Run set 2ls.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Loops
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
loops/array_false-unreach-call_true-termination.i 1 .15  24 .97 1 3.1  260 1 5.0   260   0 3.6  190 1 .61   18    - -
loops/bubble_sort_false-unreach-call.i 0 .25  27 2.0  0 .52 41 0 .022 4.9 0 1.0  50 0 .0011 .29 - -
loops/count_up_down_false-unreach-call_true-termination.i 1 .11  22 .68 1 3.1  260 1 6.5   310   0 2.6  180 1 .67   18    - -
loops/eureka_01_false-unreach-call_true-termination.i 1 1.1   60 13    1 4.5  290 1 58     910   0 3.9  210 0 .62   19    - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i 1 .20  25 1.8  1 3.1  260 1 5.2   260   0 2.9  180 1 .67   18    - -
loops/insertion_sort_false-unreach-call_true-termination.i 1 450     7700 1500    -32 4.1  280 1 7.9   300   0 3.3  220 0 .65   19    - -
loops/invert_string_false-unreach-call_true-termination.i 1 .71  44 10    1 3.6  270 1 6.1   260   0 3.1  210 1 .85   19    - -
loops/linear_search_false-unreach-call.i 0 .076 22 .71 0 .57 42 0 .018 4.8 0 .82 49 0 .0010 .33 - -
loops/ludcmp_false-unreach-call.i 0 900     3900 6300    0 .52 43 0 .019 4.8 0 .85 47 0 .0013 .26 - -
loops/matrix_false-unreach-call_true-termination.i 1 160     2400 630    1 3.2  260 1 5.4   270   0 2.8  190 1 .63   18    - -
loops/n.c24_false-unreach-call.i 0 .20  25 1.3  0 .53 43 0 .021 4.8 0 .80 49 0 .0013 .26 - -
loops/nec11_false-unreach-call_false-termination.i 1 .11  23 .85 1 3.0  260 1 6.1   250   0 3.4  180 1 .70   18    - -
loops/nec20_false-unreach-call_true-termination.i 1 1.1   75 12    1 3.1  260 1 5.7   260   0 3.1  210 0 .82   18    - -
loops/s3_false-unreach-call.i 0 .73  170 9.3  0 .55 43 0 .018 5.0 0 1.2  49 0 .0016 .26 - -
loops/string_false-unreach-call_true-termination.i 1 .66  37 7.4  -32 3.7  260 1 13     320   0 3.5  210 1 .67   18    - -
loops/sum01_bug02_false-unreach-call_true-termination.i 1 .31  29 4.0  -32 3.5  260 1 6.7   270   0 3.1  210 1 .73   19    - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 1 .23  27 2.9  1 3.4  260 1 6.9   270   0 3.1  220 1 .58   18    - -
loops/sum01_false-unreach-call_true-termination.i 1 .28  29 2.7  1 4.0  270 1 8.3   270   0 3.2  210 1 .60   19    - -
loops/sum03_false-unreach-call_true-termination.i 1 .20  26 1.8  -32 3.7  260 1 14     490   0 3.1  220 1 .60   19    - -
loops/sum04_false-unreach-call_true-termination.i 1 .26  27 2.5  1 3.2  260 1 5.6   270   0 4.0  210 1 .77   18    - -
loops/sum_array_false-unreach-call.i 1 .33  41 3.4  0 2.4  170 1 5.2   260   0 2.5  170 1 .72   18    - -
loops/terminator_01_false-unreach-call_true-termination.i 1 .13  22 .73 1 3.1  250 1 5.2   260   0 2.7  180 1 .73   18    - -
loops/terminator_02_false-unreach-call_true-termination.i 1 .13  23 .83 1 3.1  270 1 5.3   280   0 3.6  180 1 .77   18    - -
loops/terminator_03_false-unreach-call_true-termination.i 1 .10  22 .85 1 3.2  260 1 4.9   260   0 3.4  190 1 .65   18    - -
loops/trex01_false-unreach-call_true-termination.i 1 .12  23 1.3  1 3.7  260 1 6.3   260   0 3.4  210 -32 .59   18    - -
loops/trex02_false-unreach-call_true-termination.i 1 .13  22 .83 1 3.1  250 1 5.2   250   0 3.4  210 1 .68   18    - -
loops/trex03_false-unreach-call_true-termination.i 1 .097 22 1.0  1 3.1  260 1 5.8   260   0 3.3  180 1 .59   18    - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i 0 .11  22 .61 0 .54 43 0 .023 4.8 0 .82 49 0 .0015 .27 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i 1 .71  40 7.4  0 92    2000 1 19     520   0 4.0  220 0 .61   18    - -
loops/vogal_false-unreach-call.i 1 2.3   140 27    -32 4.6  280 0 97     3300   0 7.1  330 1 .69   21    - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 1 .13  22 .88 -32 2.9  260 1 4.7   230   0 2.9  180 1 .60   19    - -
loops/array_true-unreach-call_true-termination.i 2 .14  24 1.1  - - - - 2 4.5  280 2 23     370  
loops/bubble_sort_true-unreach-call_true-termination.i 0 .11  22 .61 - - - - 0 .58 41 0 .018 5.0
loops/count_up_down_true-unreach-call_true-termination.i 0 900     1400 11000    - - - - 0 .61 45 0 .019 4.8
loops/eureka_01_true-unreach-call.i 1 16     840 140    - - - - 0 900    6300 0 960     1500  
loops/eureka_05_true-unreach-call_true-termination.i 2 .92  60 10    - - - - 0 910    6700 2 58     810  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 2 .090 22 .66 - - - - 2 4.4  260 2 5.4   260  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 2 .11  22 .71 - - - - 2 3.6  270 2 6.4   260  
loops/insertion_sort_true-unreach-call_true-termination.i 0 380     15000 1700    - - - - 0 .66 43 0 .018 4.9
loops/invert_string_true-unreach-call_true-termination.i 2 .40  35 5.2  - - - - 2 21    520 2 170     770  
loops/linear_sea.ch_true-unreach-call.i 0 900     5200 5300    - - - - 0 .53 43 0 .020 4.9
loops/lu.cmp_true-unreach-call.i 1 9.5   3700 100    - - - - 0 930    6300 0 960     4500  
loops/matrix_true-unreach-call_true-termination.i 2 .17  26 1.5  - - - - 2 4.7  280 2 33     510  
loops/n.c11_true-unreach-call_false-termination.i 0 900     1700 11000    - - - - 0 .60 43 0 .048 4.8
loops/n.c40_true-unreach-call_true-termination.i 2 .14  28 1.1  - - - - 2 4.7  270 2 6.7   350  
loops/nec40_true-unreach-call_true-termination.i 2 .12  27 .99 - - - - 2 3.9  260 2 7.7   340  
loops/string_true-unreach-call_true-termination.i 2 .13  23 .84 - - - - 2 5.2  280 2 9.6   370  
loops/sum01_true-unreach-call_true-termination.i 0 900     1600 11000    - - - - 0 .57 41 0 .019 4.9
loops/sum03_true-unreach-call_false-termination.i 2 .28  26 2.7  - - - - 2 4.2  270 2 5.2   260  
loops/sum04_true-unreach-call_true-termination.i 2 .21  26 2.4  - - - - 2 6.2  270 2 10     430  
loops/sum_array_true-unreach-call.i 0 900     13000 4500    - - - - 0 .71 42 0 .019 4.8
loops/terminator_02_true-unreach-call_true-termination.i 2 .11  23 .86 - - - - 2 5.2  270 2 6.1   260  
loops/terminator_03_true-unreach-call_true-termination.i 2 .11  22 .70 - - - - 2 4.6  270 2 6.0   260  
loops/trex01_true-unreach-call_true-termination.i 2 3.7   110 50    - - - - 2 30    840 2 5.8   260  
loops/trex02_true-unreach-call_true-termination.i 2 .12  22 .70 - - - - 2 3.7  270 2 5.0   250  
loops/trex03_true-unreach-call_true-termination.i 2 .11  23 .73 - - - - 2 4.0  270 2 5.1   260  
loops/trex04_true-unreach-call_false-termination.i 2 .10  23 .79 - - - - 2 5.0  290 2 5.2   260  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i 0 .088 22 .73 - - - - 0 .52 42 0 .042 5.0
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i 2 .14  25 .89 - - - - 2 9.4  300 2 7.3   270  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i 2 .092 23 .83 - - - - 2 4.3  270 2 5.5   260  
loops/vogal_true-unreach-call.i 2 1.4   66 19    - - - - 2 55    890 2 240     1200  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 2 .096 22 .86 - - - - 2 3.5  260 2 6.1   260  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 2 .088 22 .74 - - - - 2 3.7  260 2 5.4   260  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 2 .10  22 .58 - - - - 2 4.5  260 2 5.7   260  
loop-acceleration/array_false-unreach-call1_true-termination.i 0 380     15000 3200    0 .55 42 0 .033 4.8 0 .89 49 0 .0013 .29 - -
loop-acceleration/array_false-unreach-call2_true-termination.i 0 270     15000 1700    0 .57 42 0 .018 4.8 0 .84 49 0 .0017 .29 - -
loop-acceleration/array_false-unreach-call3_true-termination.i 0 660     15000 3500    0 .56 41 0 .019 4.8 0 .82 47 0 .0038 .34 - -
loop-acceleration/const_false-unreach-call1.i 0 900     1600 12000    0 .54 42 0 .018 5.0 0 .90 49 0 .0011 .26 - -
loop-acceleration/diamond_false-unreach-call1.i 1 .82  32 11    -32 3.6  260 0 94     7000   0 4.0  220 1 .59   19    - -
loop-acceleration/functions_false-unreach-call1_true-termination.i 0 900     1400 11000    0 .53 42 0 .021 4.9 0 .94 49 0 .0014 .28 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i 1 .091 22 .96 1 3.0  260 1 4.7   250   0 3.2  210 1 .71   18    - -
loop-acceleration/nested_false-unreach-call1.i 0 900     10000 9800    0 .52 41 0 .019 4.8 0 .79 49 0 .0014 .26 - -
loop-acceleration/phases_false-unreach-call1.i 0 900     1200 10000    0 .51 43 0 .019 5.0 0 .84 49 0 .0018 .28 - -
loop-acceleration/phases_false-unreach-call2_false-termination.i 1 .14  24 1.0  1 3.4  260 1 5.2   250   0 3.0  210 1 .61   18    - -
loop-acceleration/simple_false-unreach-call1.i 0 900     1400 10000    0 .55 45 0 .019 5.0 0 .85 47 0 .0013 .26 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i 1 .11  22 .75 1 3.2  260 1 5.5   250   0 3.1  210 1 .81   18    - -
loop-acceleration/simple_false-unreach-call3_true-termination.i 1 .11  22 .87 1 2.9  260 1 4.8   250   0 3.0  190 1 .58   18    - -
loop-acceleration/simple_false-unreach-call4.i 0 900     1300 9500    0 .58 42 0 .023 4.9 0 .86 49 0 .0013 .27 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i 1 .18  25 1.5  1 3.7  260 1 11     350   0 3.3  210 1 .58   18    - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i 1 .17  25 1.9  1 3.3  260 1 8.7   350   0 3.2  210 1 .63   18    - -
loop-acceleration/array_true-unreach-call1_true-termination.i 2 35     710 380    - - - - 2 5.1  270 2 7.3   300  
loop-acceleration/array_true-unreach-call2_true-termination.i 0 260     15000 1700    - - - - 0 .53 44 0 .020 4.8
loop-acceleration/array_true-unreach-call3_true-termination.i 2 4.1   170 40    - - - - 2 6.5  270 2 9.6   380  
loop-acceleration/array_true-unreach-call4_true-termination.i 0 630     15000 4300    - - - - 0 .54 43 0 .020 4.8
loop-acceleration/const_true-unreach-call1.i 2 .18  25 1.9  - - - - 2 4.2  260 2 7.0   270  
loop-acceleration/diamond_true-unreach-call1_true-termination.i 2 .81  31 9.0  - - - - 2 14    480 0 960     680  
loop-acceleration/diamond_true-unreach-call2.i 2 .17  28 1.5  - - - - 2 7.4  310 2 62     670  
loop-acceleration/functions_true-unreach-call1_true-termination.i 0 900     1400 12000    - - - - 0 .54 41 0 .019 4.8
loop-acceleration/multivar_true-unreach-call1_true-termination.i 0 900     1600 12000    - - - - 0 .60 42 0 .019 4.9
loop-acceleration/nested_true-unreach-call1.i 2 .18  25 1.5  - - - - 2 5.8  280 2 30     500  
loop-acceleration/overflow_true-unreach-call1.i 0 900     1300 11000    - - - - 0 .54 43 0 .022 4.9
loop-acceleration/phases_true-unreach-call1.i 0 900     1500 11000    - - - - 0 .56 42 0 .018 5.0
loop-acceleration/phases_true-unreach-call2_false-termination.i 2 .11  24 1.2  - - - - 0 900    410 2 7.5   260  
loop-acceleration/simple_true-unreach-call1.i 0 900     1400 12000    - - - - 0 .63 41 0 .017 4.8
loop-acceleration/simple_true-unreach-call2_true-termination.i 2 .082 22 .83 - - - - 2 4.1  260 2 4.2   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i 0 900     1200 10000    - - - - 0 .53 45 0 .020 4.9
loop-acceleration/simple_true-unreach-call4.i 2 .097 22 .85 - - - - 2 3.6  260 2 8.1   260  
loop-acceleration/underapprox_true-unreach-call1_true-termination.i 2 .16  25 1.6  - - - - 2 4.5  280 2 55     430  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i 2 .10  23 1.0  - - - - 2 4.6  260 2 7.8   290  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i 1 4.3   1400 45    -32 3.6  260 1 5.7   240   0 3.7  210 -32 .58   18    - -
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i 0 670     15000 4000    - - - - 0 .61 41 0 .023 4.9
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i 0 260     15000 2600    - - - - 0 .61 45 0 .019 4.9
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i 0 270     15000 2600    - - - - 0 .52 41 0 .019 4.9
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i 0 250     15000 1900    - - - - 0 .55 41 0 .019 5.0
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i 2 .67  30 8.5  - - - - 2 4.6  260 2 7.5   260  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i 0 900     370 11000    - - - - 0 .73 44 0 .019 4.8
loop-invgen/id_trans_false-unreach-call_true-termination.i 1 .12  23 .86 1 3.4  290 1 5.0   250   0 2.9  210 1 .58   18    - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 0 900     420 8900    - - - - 0 .62 41 0 .020 4.9
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i 2 .16  24 1.4  - - - - 0 650    7000 2 9.4   410  
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 2 2.1   46 27    - - - - 0 900    4400 2 14     500  
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 0 900     2100 10000    - - - - 0 .53 44 0 .018 4.8
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 2 .63  30 6.9  - - - - 2 7.7  300 2 10     430  
loop-invgen/down_true-unreach-call_true-termination.i 0 900     1600 8700    - - - - 0 .56 44 0 .019 5.0
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 0 900     3000 11000    - - - - 0 .66 42 0 .019 4.9
loop-invgen/half_2_true-unreach-call_true-termination.i 0 900     1900 11000    - - - - 0 .72 41 0 .020 4.9
loop-invgen/heapsort_true-unreach-call_true-termination.i 0 900     2000 5300    - - - - 0 .60 44 0 .017 4.8
loop-invgen/id_build_true-unreach-call_true-termination.i 2 .21  26 2.0  - - - - 2 5.4  280 -16 5.0   240  
loop-invgen/large_const_true-unreach-call_true-termination.i 2 .22  27 2.4  - - - - 2 4.9  280 -16 5.4   260  
loop-invgen/nest-if3_true-unreach-call_true-termination.i 2 .78  35 8.3  - - - - 0 900    3600 2 7.5   270  
loop-invgen/nested6_true-unreach-call_true-termination.i 0 900     2700 4400    - - - - 0 .58 41 0 .018 4.9
loop-invgen/nested9_true-unreach-call_true-termination.i 0 900     330 7900    - - - - 0 .54 44 0 .019 4.9
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 0 900     2100 11000    - - - - 0 .53 41 0 .018 5.0
loop-invgen/seq_true-unreach-call_true-termination.i 0 900     830 6700    - - - - 0 .58 43 0 .019 4.8
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i 0 .093 22 .61 - - - - 0 .55 44 0 .021 4.8
loop-invgen/up_true-unreach-call_true-termination.i 0 900     1900 9800    - - - - 0 .54 43 0 .018 5.0
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 0 900     2000 10000    - - - - 0 .54 42 0 .032 4.8
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i 0 900     280 12000    - - - - 0 .55 41 0 .048 4.8
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i 2 .19  25 1.6  - - - - 2 5.4  280 2 7.6   310  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i 0 900     1600 10000    - - - - 0 .66 43 0 .050 4.8
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i 0 900     5300 6700    - - - - 0 .49 43 0 .019 4.8
loop-lit/css2003_true-unreach-call_true-termination.c.i 0 900     340 8000    - - - - 0 .54 43 0 .034 4.8
loop-lit/ddlm2013_true-unreach-call.i 0 900     2000 11000    - - - - 0 .67 44 0 .024 4.8
loop-lit/gj2007_true-unreach-call_true-termination.c.i 2 5.5   89 69    - - - - 2 38    510 2 97     1300  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 0 900     1300 12000    - - - - 0 .61 42 0 .020 4.9
loop-lit/gr2006_true-unreach-call_true-termination.c.i 2 9.6   130 120    - - - - 2 46    910 2 120     1700  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i 0 900     800 9900    - - - - 0 .59 44 0 .018 4.8
loop-lit/hhk2008_true-unreach-call_true-termination.c.i 0 900     380 8800    - - - - 0 .54 43 0 .027 4.8
loop-lit/jm2006_true-unreach-call_true-termination.c.i 0 900     1400 9200    - - - - 0 .64 41 0 .024 4.8
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i 0 900     1600 12000    - - - - 0 .56 44 0 .023 4.9
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 0 .16  23 1.6  - - - - 0 .65 43 0 .020 4.8
loop-lit/gcnr2008_false-unreach-call_false-termination.i 1 .13  23 .90 0 92    2200 1 4.9   250   0 2.7  180 1 .74   18    - -
loop-new/count_by_1_true-unreach-call_true-termination.i 2 .14  24 1.1  - - - - 2 4.7  280 2 5.7   270  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i 2 .15  24 1.1  - - - - 2 4.0  270 2 8.0   280  
loop-new/count_by_2_true-unreach-call_true-termination.i 0 900     1200 11000    - - - - 0 .52 43 0 .019 4.9
loop-new/count_by_k_true-unreach-call_true-termination.i 0 900     1200 11000    - - - - 0 .70 44 0 .018 4.8
loop-new/count_by_nondet_true-unreach-call_true-termination.i 0 900     2000 11000    - - - - 0 .57 43 0 .023 4.9
loop-new/gauss_sum_true-unreach-call_true-termination.i 0 900     1600 14000    - - - - 0 .54 43 0 .024 4.8
loop-new/half_true-unreach-call_true-termination.i 0 900     1800 11000    - - - - 0 .70 44 0 .048 4.9
loop-new/nested_true-unreach-call_true-termination.i 0 900     2600 5600    - - - - 0 .66 43 0 .019 4.9
loop-industry-pattern/aiob_1_true-unreach-call.c 2 .37  32 3.5  - - - - 2 50    600 0 960     1900  
loop-industry-pattern/aiob_2_true-unreach-call.c 2 .41  32 3.6  - - - - 2 43    520 0 960     1800  
loop-industry-pattern/aiob_3_true-unreach-call.c 2 .38  32 3.2  - - - - 2 46    510 0 960     2000  
loop-industry-pattern/aiob_4_true-unreach-call.c 2 .38  32 3.4  - - - - 2 37    530 0 960     1800  
loop-industry-pattern/mod3_true-unreach-call.c 2 .65  30 7.6  - - - - 2 7.5  320 2 16     270  
loop-industry-pattern/nested_true-unreach-call.c 0 900     320 8800    - - - - 0 .70 41 0 .047 5.0
loop-industry-pattern/ofuf_1_true-unreach-call.c 0 .29  30 2.8  - - - - 0 .62 46 0 .024 4.9
loop-industry-pattern/ofuf_2_true-unreach-call.c 0 .32  30 3.2  - - - - 0 .68 42 0 .021 4.9
loop-industry-pattern/ofuf_3_true-unreach-call.c 0 .33  30 2.6  - - - - 0 .52 42 0 .025 4.9
loop-industry-pattern/ofuf_4_true-unreach-call.c 0 .32  30 3.0  - - - - 0 .54 43 0 .020 4.9
loop-industry-pattern/ofuf_5_true-unreach-call.c 0 .30  30 2.7  - - - - 0 .67 46 0 .025 4.9
loops/heavy_true-unreach-call.c 0 27     15000 370    - - - - 0 .51 45 0 .019 5.0
loops/compact_false-unreach-call.c 0 410     15000 3800    0 .54 43 0 .020 4.9 0 .90 49 0 .0015 .35 - -
loops/heavy_false-unreach-call.c 0 27     15000 380    0 .54 43 0 .019 4.9 0 1.1  50 0 .0013 .26 - -
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 163 139 48000 310000 500000 52 -232 300 13000 52 33 470 20000 52 0 130 8000 52 -35 23   650 111 92 6700 53000 111 56 7900 33000
    correct results 86 137 690 15000 3200 24 24 79 6300 33 33 280 9900 0 29 29 19   540 46 92 560 16000 44 88 1100 18000
        correct true 51 102 73 2500 820 0 0 0 0 46 92 560 16000 44 88 1100 18000
        correct false 35 35 620 13000 2300 24 24 79 6300 33 33 280 9900 0 29 29 19   540 0 0
    correct-unconfimed results 2 2 26 4600 240 0 0 0 0 0 0
        correct-unconfirmed true 2 2 26 4600 240 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 8 -256 30 2100 0 0 2 -64 1.2 37 0 2 -32 10 500
        incorrect true 0 8 -256 30 2100 0 0 2 -64 1.2 37 0 0
        incorrect false 0 0 0 0 0 0 2 -32 10 500
score (163 tasks, max score: 274) 139 -232 33 0 -35 92 56
Run set 2ls.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Loops