Tool Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 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] 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-01 19:46:39 CET 2017-12-01 22:34:51 CET 2017-12-01 23:03:48 CET 2017-12-01 23:06:19 CET 2017-12-01 23:09:14 CET 2017-12-01 22:04:37 CET 2017-12-01 22:38:34 CET
Run set map2check.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Loops
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.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/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.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/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/map2check.2017-12-01_1946.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 -32 .43  12 4.7  0 4.7  270 1 5.4   270   0 .98 52 0 .091  9.1  - -
loops/bubble_sort_false-unreach-call.i 0 .39  12 4.2  0 .59 42 0 .020 4.8 0 .87 50 0 .0013 .28 - -
loops/count_up_down_false-unreach-call_true-termination.i 1 .35  11 3.7  0 92    2000 1 4.9   250   0 3.5  210 1 .58   18    - -
loops/eureka_01_false-unreach-call_true-termination.i 1 2.6   13 33    -32 4.2  260 -32 5.3   240   0 2.9  210 1 .67   18    - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i -32 .52  12 5.3  0 5.3  270 1 8.1   290   0 .92 51 0 .079  9.1  - -
loops/insertion_sort_false-unreach-call_true-termination.i -32 .37  11 3.9  0 52    580 0 97     870   0 .92 52 0 .066  9.0  - -
loops/invert_string_false-unreach-call_true-termination.i 0 .38  12 4.0  0 .55 41 0 .018 5.0 0 1.1  49 0 .0015 .28 - -
loops/linear_search_false-unreach-call.i -32 .37  11 4.8  0 10    340 0 96     710   0 .98 51 0 .066  9.0  - -
loops/ludcmp_false-unreach-call.i 1 .39  11 4.8  -32 3.0  270 0 97     4500   0 3.6  190 1 .65   18    - -
loops/matrix_false-unreach-call_true-termination.i 0 900     410 9000    0 .62 43 0 .023 4.9 0 .85 49 0 .0012 .34 - -
loops/n.c24_false-unreach-call.i 0 900     1500 10000    0 .70 43 0 .019 4.9 0 1.0  49 0 .0017 .29 - -
loops/nec11_false-unreach-call_false-termination.i 0 .31  11 2.9  0 .72 44 0 .018 4.8 0 1.1  49 0 .0014 .26 - -
loops/nec20_false-unreach-call_true-termination.i 0 .30  11 4.0  0 .41 43 0 .019 5.0 0 .86 47 0 .0016 .27 - -
loops/s3_false-unreach-call.i 0 .096 13 .70 0 .71 44 0 .019 4.9 0 .83 49 0 .0015 .26 - -
loops/string_false-unreach-call_true-termination.i -32 1.2   12 15    0 51    1100 1 19     370   0 1.0  50 0 .073  9.0  - -
loops/sum01_bug02_false-unreach-call_true-termination.i -32 .70  12 8.8  0 5.9  280 1 12     500   0 1.2  51 0 .064  9.0  - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 1 .60  12 6.6  0 92    2100 -32 7.1   270   0 3.3  210 1 .61   18    - -
loops/sum01_false-unreach-call_true-termination.i -32 .82  12 11    0 6.9  280 1 11     500   0 .95 49 0 .076  9.0  - -
loops/sum03_false-unreach-call_true-termination.i 1 .33  11 3.8  -32 2.4  260 -32 6.1   260   0 3.7  210 1 .71   18    - -
loops/sum04_false-unreach-call_true-termination.i 1 .33  11 3.6  -32 3.9  250 -32 6.3   260   0 2.9  180 1 .64   18    - -
loops/sum_array_false-unreach-call.i -32 .38  15 4.3  0 8.3  320 1 6.9   260   0 1.0  50 0 .067  9.0  - -
loops/terminator_01_false-unreach-call_true-termination.i 1 .34  11 4.0  1 3.0  260 1 5.3   250   0 3.5  210 1 .65   18    - -
loops/terminator_02_false-unreach-call_true-termination.i 1 .43  12 6.1  1 3.9  260 1 3.4   260   0 3.8  210 1 .64   18    - -
loops/terminator_03_false-unreach-call_true-termination.i 1 .56  13 6.7  1 3.9  260 1 5.7   260   0 3.6  210 1 .76   18    - -
loops/trex01_false-unreach-call_true-termination.i 0 .30  11 3.5  0 .72 43 0 .019 4.8 0 .87 49 0 .0015 .27 - -
loops/trex02_false-unreach-call_true-termination.i 1 .40  12 5.1  1 3.6  260 1 5.4   250   0 3.5  190 1 .59   18    - -
loops/trex03_false-unreach-call_true-termination.i 0 .30  11 3.6  0 .57 42 0 .018 4.8 0 .95 50 0 .0014 .26 - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i 1 .34  11 3.9  -32 3.7  260 1 8.8   300   0 2.8  210 1 .66   18    - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i 0 .31  11 3.8  0 .68 44 0 .022 5.0 0 .86 50 0 .0011 .36 - -
loops/vogal_false-unreach-call.i 1 1.8   12 22    -32 6.6  410 -32 3.5   220   0 4.0  210 1 .64   19    - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 1 .32  11 4.0  -32 3.3  260 1 4.9   230   0 2.9  190 1 .58   18    - -
loops/array_true-unreach-call_true-termination.i 2 .45  12 4.9  - - - - 2 5.2  280 2 7.5   280  
loops/bubble_sort_true-unreach-call_true-termination.i 2 .36  11 3.9  - - - - 2 3.6  260 2 4.9   240  
loops/count_up_down_true-unreach-call_true-termination.i 0 900     1200 12000    - - - - 0 .56 43 0 .020 4.8
loops/eureka_01_true-unreach-call.i 1 .37  11 4.4  - - - - 0 900    5400 0 960     1400  
loops/eureka_05_true-unreach-call_true-termination.i 2 .34  11 4.3  - - - - 0 900    6500 2 53     830  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 0 890     12 12000    - - - - 0 .62 44 0 .018 4.9
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 0 900     11 13000    - - - - 0 .57 43 0 .025 4.8
loops/insertion_sort_true-unreach-call_true-termination.i 1 .38  12 4.5  - - - - 0 900    2900 0 960     3100  
loops/invert_string_true-unreach-call_true-termination.i 2 .39  11 5.0  - - - - 2 20    520 2 190     780  
loops/linear_sea.ch_true-unreach-call.i 1 .38  11 5.1  - - - - 0 710    7000 0 960     720  
loops/lu.cmp_true-unreach-call.i 1 .44  11 5.0  - - - - 0 900    5300 0 960     4000  
loops/matrix_true-unreach-call_true-termination.i 2 .47  12 5.1  - - - - 2 4.1  270 2 11     380  
loops/n.c11_true-unreach-call_false-termination.i 0 .27  11 3.2  - - - - 0 .67 43 0 .026 4.8
loops/n.c40_true-unreach-call_true-termination.i 2 .37  12 3.6  - - - - 2 3.7  270 2 6.7   340  
loops/nec40_true-unreach-call_true-termination.i 2 .35  12 4.5  - - - - 2 4.5  270 2 7.2   350  
loops/string_true-unreach-call_true-termination.i 2 18     13 210    - - - - 2 5.6  280 2 12     380  
loops/sum01_true-unreach-call_true-termination.i 2 74     64 900    - - - - 0 570    7000 2 12     390  
loops/sum03_true-unreach-call_false-termination.i 0 890     11 14000    - - - - 0 .55 41 0 .026 4.8
loops/sum04_true-unreach-call_true-termination.i 2 .30  11 4.2  - - - - 2 2.9  270 2 12     430  
loops/sum_array_true-unreach-call.i 0 .036 13 .39 - - - - 0 .43 43 0 .018 4.9
loops/terminator_02_true-unreach-call_true-termination.i 2 .61  12 6.2  - - - - 2 3.0  270 2 7.0   260  
loops/terminator_03_true-unreach-call_true-termination.i 0 900     66 14000    - - - - 0 .56 44 0 .018 4.8
loops/trex01_true-unreach-call_true-termination.i 0 .28  11 3.4  - - - - 0 .53 43 0 .025 4.8
loops/trex02_true-unreach-call_true-termination.i 2 .34  12 4.4  - - - - 2 3.6  260 2 4.1   260  
loops/trex03_true-unreach-call_true-termination.i 0 .31  11 3.3  - - - - 0 .52 41 0 .021 4.9
loops/trex04_true-unreach-call_false-termination.i 2 .39  12 4.3  - - - - 2 4.0  270 2 6.0   270  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i 2 .31  11 3.8  - - - - 0 410    7000 2 7.9   290  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i 2 700     79 8600    - - - - 2 6.8  360 2 6.9   270  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i 2 3.0   12 39    - - - - 2 4.0  270 2 6.1   270  
loops/vogal_true-unreach-call.i 2 13     13 150    - - - - 2 46    1100 2 290     1100  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 0 890     11 11000    - - - - 0 .56 44 0 .018 4.9
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 0 890     11 15000    - - - - 0 .54 41 0 .025 4.8
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 0 900     11 12000    - - - - 0 .54 41 0 .019 4.9
loop-acceleration/array_false-unreach-call1_true-termination.i 1 .34  11 3.9  -32 47    320 -32 10     410   0 3.0  180 1 .63   18    - -
loop-acceleration/array_false-unreach-call2_true-termination.i 1 .36  11 5.4  -32 17    430 -32 9.2   430   0 2.9  180 1 .66   18    - -
loop-acceleration/array_false-unreach-call3_true-termination.i 0 890     53 11000    0 .66 44 0 .019 4.9 0 1.1  49 0 .0014 .26 - -
loop-acceleration/const_false-unreach-call1.i 1 .34  11 4.7  -32 9.6  400 -32 11     450   0 3.1  180 1 .57   18    - -
loop-acceleration/diamond_false-unreach-call1.i 1 .36  11 4.2  -32 2.5  270 -32 6.0   260   0 3.8  210 1 .68   18    - -
loop-acceleration/functions_false-unreach-call1_true-termination.i 0 890     11 13000    0 .46 43 0 .019 5.0 0 1.2  50 0 .0016 .26 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i 1 .34  11 3.9  -32 3.2  260 1 6.6   250   0 3.0  190 1 .58   18    - -
loop-acceleration/nested_false-unreach-call1.i 0 890     11 13000    0 .71 44 0 .022 4.8 0 1.1  49 0 .0015 .27 - -
loop-acceleration/phases_false-unreach-call1.i 0 890     11 14000    0 .58 41 0 .022 4.8 0 .88 47 0 .0017 .27 - -
loop-acceleration/phases_false-unreach-call2_false-termination.i 1 .40  11 4.7  -32 4.1  250 1 4.9   250   0 3.1  180 1 .77   18    - -
loop-acceleration/simple_false-unreach-call1.i 0 900     11 12000    0 .68 43 0 .019 4.9 0 .86 50 0 .0015 .26 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i 1 .30  11 3.5  -32 3.6  260 1 5.1   250   0 2.8  180 1 .79   18    - -
loop-acceleration/simple_false-unreach-call3_true-termination.i 1 .30  11 4.0  0 92    1900 1 4.6   250   0 2.9  180 1 .74   18    - -
loop-acceleration/simple_false-unreach-call4.i 0 890     11 11000    0 .61 43 0 .019 5.0 0 .87 50 0 .0018 .29 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i 1 .33  11 4.0  -32 3.7  250 1 7.8   310   0 2.7  180 1 .59   18    - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i 1 .32  11 3.9  -32 4.0  260 1 8.4   310   0 3.6  180 1 .73   18    - -
loop-acceleration/array_true-unreach-call1_true-termination.i 2 .37  11 4.1  - - - - 2 2.6  270 2 7.1   280  
loop-acceleration/array_true-unreach-call2_true-termination.i 1 .39  11 4.6  - - - - 0 900    2800 0 960     3400  
loop-acceleration/array_true-unreach-call3_true-termination.i 0 890     53 11000    - - - - 0 .71 45 0 .025 4.9
loop-acceleration/array_true-unreach-call4_true-termination.i 0 890     71 12000    - - - - 0 .75 44 0 .025 4.9
loop-acceleration/const_true-unreach-call1.i 2 .33  11 4.2  - - - - 2 4.1  270 2 8.9   260  
loop-acceleration/diamond_true-unreach-call1_true-termination.i 2 .38  11 4.5  - - - - 2 14    480 0 960     550  
loop-acceleration/diamond_true-unreach-call2.i 2 .44  11 5.3  - - - - 2 7.3  310 2 64     680  
loop-acceleration/functions_true-unreach-call1_true-termination.i 0 890     11 12000    - - - - 0 .53 43 0 .026 4.8
loop-acceleration/multivar_true-unreach-call1_true-termination.i 2 67     64 860    - - - - 2 820    5800 2 5.8   260  
loop-acceleration/nested_true-unreach-call1.i 0 890     11 12000    - - - - 0 .67 43 0 .020 4.9
loop-acceleration/overflow_true-unreach-call1.i 0 890     11 12000    - - - - 0 .57 41 0 .024 4.8
loop-acceleration/phases_true-unreach-call1.i 0 890     11 12000    - - - - 0 .40 44 0 .021 4.8
loop-acceleration/phases_true-unreach-call2_false-termination.i 0 890     12 11000    - - - - 0 .53 43 0 .026 4.8
loop-acceleration/simple_true-unreach-call1.i 0 890     11 12000    - - - - 0 .64 45 0 .023 4.9
loop-acceleration/simple_true-unreach-call2_true-termination.i 2 .30  11 3.9  - - - - 2 3.7  260 2 7.0   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i 0 900     1100 11000    - - - - 0 .65 43 0 .025 4.8
loop-acceleration/simple_true-unreach-call4.i 0 890     11 12000    - - - - 0 .57 43 0 .025 4.9
loop-acceleration/underapprox_true-unreach-call1_true-termination.i 2 .33  11 3.5  - - - - 2 4.8  280 2 63     440  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i 2 .30  11 3.5  - - - - 2 3.5  270 2 7.1   270  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i 1 .38  19 4.6  -32 4.1  260 1 3.2   250   0 3.1  210 -32 .60   18    - -
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i 1 .47  11 6.3  - - - - 0 900    4200 0 960     710  
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i 0 900     75 10000    - - - - 0 .53 43 0 .019 4.9
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i 1 1.6   11 21    - - - - 0 910    6200 0 960     740  
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i 2 1.2   160 14    - - - - 0 900    1800 2 80     460  
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i 0 890     11 14000    - - - - 0 .67 43 0 .021 4.9
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i 0 890     11 14000    - - - - 0 .55 43 0 .025 4.8
loop-invgen/id_trans_false-unreach-call_true-termination.i 1 .58  12 7.8  1 3.9  270 -32 5.3   260   0 3.6  210 1 .65   18    - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 0 900     660 11000    - - - - 0 .70 43 0 .021 4.9
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i 0 900     910 11000    - - - - 0 .73 43 0 .025 4.9
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 0 900     170 11000    - - - - 0 .53 41 0 .020 4.8
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 0 890     130 13000    - - - - 0 .52 41 0 .022 4.9
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 0 900     320 10000    - - - - 0 .54 41 0 .023 4.9
loop-invgen/down_true-unreach-call_true-termination.i 0 890     400 8200    - - - - 0 .53 43 0 .021 4.8
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 0 900     190 12000    - - - - 0 .56 41 0 .025 4.9
loop-invgen/half_2_true-unreach-call_true-termination.i 0 900     840 8200    - - - - 0 .69 44 0 .024 4.8
loop-invgen/heapsort_true-unreach-call_true-termination.i 0 900     900 8800    - - - - 0 .54 45 0 .023 4.8
loop-invgen/id_build_true-unreach-call_true-termination.i 0 900     680 13000    - - - - 0 .66 44 0 .019 4.8
loop-invgen/large_const_true-unreach-call_true-termination.i 2 .89  12 11    - - - - 2 4.8  290 2 9.2   350  
loop-invgen/nest-if3_true-unreach-call_true-termination.i 0 890     460 11000    - - - - 0 .55 42 0 .024 4.8
loop-invgen/nested6_true-unreach-call_true-termination.i 0 900     700 10000    - - - - 0 .54 43 0 .024 4.9
loop-invgen/nested9_true-unreach-call_true-termination.i 0 890     67 11000    - - - - 0 .57 42 0 .033 4.9
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 0 890     40 11000    - - - - 0 .55 41 0 .047 4.9
loop-invgen/seq_true-unreach-call_true-termination.i 0 900     200 11000    - - - - 0 .60 43 0 .022 4.8
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i 0 890     98 11000    - - - - 0 .56 43 0 .026 5.0
loop-invgen/up_true-unreach-call_true-termination.i 0 900     420 8900    - - - - 0 .55 43 0 .024 4.8
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 0 890     29 12000    - - - - 0 .54 42 0 .025 5.0
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i 0 900     580 11000    - - - - 0 .71 43 0 .027 4.8
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i 2 .35  11 3.7  - - - - 2 3.8  270 2 10     310  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i 0 900     330 11000    - - - - 0 .59 43 0 .025 4.9
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i 2 .33  11 4.7  - - - - 2 4.4  270 2 8.4   260  
loop-lit/css2003_true-unreach-call_true-termination.c.i 2 150     12 1900    - - - - 2 4.8  270 2 6.3   270  
loop-lit/ddlm2013_true-unreach-call.i 0 890     30 13000    - - - - 0 .57 43 0 .018 4.9
loop-lit/gj2007_true-unreach-call_true-termination.c.i 2 .34  11 3.9  - - - - 2 40    580 2 91     1200  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 0 900     1000 12000    - - - - 0 .56 41 0 .024 4.9
loop-lit/gr2006_true-unreach-call_true-termination.c.i 2 .34  11 3.9  - - - - 2 46    1000 2 120     1600  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i 0 900     40 11000    - - - - 0 .52 43 0 .018 5.0
loop-lit/hhk2008_true-unreach-call_true-termination.c.i 0 900     330 11000    - - - - 0 .59 44 0 .025 4.8
loop-lit/jm2006_true-unreach-call_true-termination.c.i 0 900     680 9600    - - - - 0 .56 41 0 .019 4.8
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i 0 900     650 11000    - - - - 0 .64 43 0 .023 4.9
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 1 .43  12 4.8  - - - - 0 760    7000 0 960     710  
loop-lit/gcnr2008_false-unreach-call_false-termination.i 1 .39  12 4.4  1 3.9  260 1 4.7   250   0 3.2  210 1 .65   18    - -
loop-new/count_by_1_true-unreach-call_true-termination.i 2 17     11 220    - - - - 2 2.4  260 2 6.9   260  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i 2 92     11 1400    - - - - 2 3.6  260 2 7.5   270  
loop-new/count_by_2_true-unreach-call_true-termination.i 1 8.1   11 120    - - - - 0 480    7000 0 960     4600  
loop-new/count_by_k_true-unreach-call_true-termination.i 0 900     26 12000    - - - - 0 .49 43 0 .024 4.8
loop-new/count_by_nondet_true-unreach-call_true-termination.i 0 900     73 12000    - - - - 0 .52 43 0 .018 4.8
loop-new/gauss_sum_true-unreach-call_true-termination.i 1 78     65 900    - - - - 0 910    6300 0 960     950  
loop-new/half_true-unreach-call_true-termination.i 0 900     1600 9700    - - - - 0 .59 44 0 .025 4.9
loop-new/nested_true-unreach-call_true-termination.i 0 890     680 12000    - - - - 0 .55 43 0 .025 5.0
loop-industry-pattern/aiob_1_true-unreach-call.c 2 .40  12 4.6  - - - - 2 40    520 0 960     1800  
loop-industry-pattern/aiob_2_true-unreach-call.c 2 .38  11 4.5  - - - - 2 44    590 0 960     1800  
loop-industry-pattern/aiob_3_true-unreach-call.c 2 .37  12 4.2  - - - - 2 33    590 0 960     1900  
loop-industry-pattern/aiob_4_true-unreach-call.c 2 .40  12 4.4  - - - - 2 38    480 0 960     1700  
loop-industry-pattern/mod3_true-unreach-call.c 0 900     260 11000    - - - - 0 .55 43 0 .023 4.8
loop-industry-pattern/nested_true-unreach-call.c 0 900     11 12000    - - - - 0 .52 43 0 .020 4.9
loop-industry-pattern/ofuf_1_true-unreach-call.c 2 .41  12 5.2  - - - - 0 4.5  260 2 10     330  
loop-industry-pattern/ofuf_2_true-unreach-call.c 2 .44  12 5.0  - - - - 0 3.7  270 2 9.8   330  
loop-industry-pattern/ofuf_3_true-unreach-call.c 2 .42  12 4.8  - - - - 0 4.1  250 2 9.7   320  
loop-industry-pattern/ofuf_4_true-unreach-call.c 2 .42  12 4.8  - - - - 0 3.4  250 2 12     350  
loop-industry-pattern/ofuf_5_true-unreach-call.c 2 .42  12 4.7  - - - - 0 4.1  250 2 11     330  
loops/heavy_true-unreach-call.c 0 900     41 12000    - - - - 0 .59 45 0 .020 4.8
loops/compact_false-unreach-call.c 0 900     99 12000    0 .73 43 0 .019 4.9 0 .93 48 0 .0015 .26 - -
loops/heavy_false-unreach-call.c 0 890     39 12000    0 .70 43 0 .018 4.8 0 1.1  49 0 .0013 .28 - -
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 -134 59000   20000 760000 52 -538 580 17000 52 -299 510 15000 52 0 110 6400 52 -7 18    560 111 68 12000 98000 111 76 16000 45000
    correct results 69 112 1200   1100 15000 6 6 22 1600 21 21 150 6100 0 25 25 16    460 34 68 1200 18000 38 76 1200 16000
        correct true 43 86 1100   820 14000 0 0 0 0 34 68 1200 18000 38 76 1200 16000
        correct false 26 26 14   310 170 6 6 22 1600 21 21 150 6100 0 25 25 16    460 0 0
    correct-unconfimed results 10 10 90   170 1100 0 0 0 0 0 0
        correct-unconfirmed true 10 10 90   170 1100 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 8 -256 4.8 97 58 17 -544 130 4900 10 -320 70 3100 0 1 -32 .60 18 0 0
        incorrect true 8 -256 4.8 97 58 17 -544 130 4900 10 -320 70 3100 0 1 -32 .60 18 0 0
        incorrect false 0 0 0 0 0 0 0
score (163 tasks, max score: 274) -134 -538 -299 0 -7 68 76
Run set map2check.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Loops