Tool 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:29:20 CET 2017-12-01 08:07:14 CET 2017-12-01 08:15:38 CET 2017-12-01 08:19:10 CET 2017-12-01 04:11:27 CET 2017-12-01 07:35:08 CET
Run set cpa-seq.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Loops
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.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/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.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/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-seq.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 3.4 270 32 1 3.8  260 1 5.7   260   0 3.0  180 1 .59   18    - -
loops/bubble_sort_false-unreach-call.i 1 4.9 310 43 -32 4.8  280 0 10     210   0 3.7  210 1 .74   18    - -
loops/count_up_down_false-unreach-call_true-termination.i 1 2.5 250 21 1 3.5  250 1 6.8   320   0 2.9  210 1 .60   18    - -
loops/eureka_01_false-unreach-call_true-termination.i 0 900   4400 11000 0 .56 43 0 .023 4.8 0 .98 49 0 .0045 .26 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i 1 3.6 270 33 1 3.5  260 1 5.5   260   0 3.7  210 -32 .73   19    - -
loops/insertion_sort_false-unreach-call_true-termination.i 1 51   2300 430 -32 3.5  270 1 16     520   0 3.2  210 -32 .63   19    - -
loops/invert_string_false-unreach-call_true-termination.i 1 210   2100 2900 -32 3.5  270 1 11     430   0 3.0  210 -32 .61   19    - -
loops/linear_search_false-unreach-call.i 1 13   540 99 1 4.2  280 1 14     520   0 3.7  210 0 .59   19    - -
loops/ludcmp_false-unreach-call.i 1 6.8 530 65 1 8.7  520 0 97     4500   0 3.3  210 0 .60   19    - -
loops/matrix_false-unreach-call_true-termination.i 1 3.7 280 31 1 3.4  270 1 7.4   330   0 2.8  180 1 .60   19    - -
loops/n.c24_false-unreach-call.i 0 900   5000 9200 0 .50 41 0 .017 4.9 0 .82 47 0 .0013 .32 - -
loops/nec11_false-unreach-call_false-termination.i 1 2.6 260 22 1 3.2  260 1 4.8   250   0 3.0  180 1 .59   18    - -
loops/nec20_false-unreach-call_true-termination.i 1 2.8 260 23 1 3.6  260 1 6.9   320   0 2.9  180 1 .76   18    - -
loops/s3_false-unreach-call.i 1 44   2500 430 -32 6.1  280 1 71     660   0 6.0  270 0 .81   20    - -
loops/string_false-unreach-call_true-termination.i 1 3.3 270 28 1 3.9  270 1 27     430   0 3.1  210 -32 .61   19    - -
loops/sum01_bug02_false-unreach-call_true-termination.i 1 4.1 280 42 1 3.5  260 1 10     280   0 3.4  210 1 .60   19    - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 1 3.7 280 36 1 3.2  260 1 6.8   260   0 3.3  180 -32 .63   19    - -
loops/sum01_false-unreach-call_true-termination.i 1 5.0 280 45 1 3.8  270 1 8.1   600   0 3.0  210 -32 .60   19    - -
loops/sum03_false-unreach-call_true-termination.i 1 3.6 270 29 1 4.8  290 0 84     7000   0 3.4  210 1 .71   19    - -
loops/sum04_false-unreach-call_true-termination.i 1 3.0 260 25 1 3.4  260 1 6.9   320   0 3.1  190 1 .58   18    - -
loops/sum_array_false-unreach-call.i 1 3.8 280 33 1 3.5  270 1 5.9   270   0 3.1  210 1 .62   19    - -
loops/terminator_01_false-unreach-call_true-termination.i 1 2.5 250 26 1 3.1  260 1 6.0   260   0 2.7  180 1 .58   18    - -
loops/terminator_02_false-unreach-call_true-termination.i 1 2.6 260 21 1 3.1  260 1 5.0   260   0 2.9  210 1 .59   18    - -
loops/terminator_03_false-unreach-call_true-termination.i 1 3.3 270 28 1 3.3  260 1 6.0   260   0 3.0  210 1 .60   18    - -
loops/trex01_false-unreach-call_true-termination.i 1 2.6 250 20 1 3.3  260 1 7.7   270   0 3.0  210 1 .71   18    - -
loops/trex02_false-unreach-call_true-termination.i 1 2.6 280 24 1 3.0  260 1 6.1   250   0 2.7  180 -32 .58   18    - -
loops/trex03_false-unreach-call_true-termination.i 1 3.2 270 32 1 3.4  260 1 5.1   260   0 3.9  210 1 .59   18    - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i 1 2.7 280 22 1 3.2  260 1 9.1   320   0 3.1  210 1 .78   18    - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i 1 4.2 280 37 1 4.1  270 1 20     510   0 3.0  210 0 .59   19    - -
loops/vogal_false-unreach-call.i 1 52   510 620 1 4.4  300 0 97     910   0 3.7  220 1 .67   20    - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 1 2.6 260 22 0 96    2700 1 5.3   230   0 96    2700 1 .57   18    - -
loops/array_true-unreach-call_true-termination.i 2 3.5 270 32 - - - - 2 4.7  270 2 8.0   280  
loops/bubble_sort_true-unreach-call_true-termination.i 2 93   470 1200 - - - - 2 4.0  280 2 4.9   230  
loops/count_up_down_true-unreach-call_true-termination.i 0 900   7000 9200 - - - - 0 .55 42 0 .019 4.9
loops/eureka_01_true-unreach-call.i 1 3.9 260 36 - - - - 0 900    5500 0 680     7000  
loops/eureka_05_true-unreach-call_true-termination.i 2 2.9 250 24 - - - - 0 900    4700 2 100     1000  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 2 93   2200 910 - - - - 2 3.7  260 2 6.0   260  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 2 93   2300 1000 - - - - 2 4.4  260 2 4.9   260  
loops/insertion_sort_true-unreach-call_true-termination.i 0 900   4600 6500 - - - - 0 .68 42 0 .019 4.9
loops/invert_string_true-unreach-call_true-termination.i 2 35   810 310 - - - - 2 27    560 2 540     660  
loops/linear_sea.ch_true-unreach-call.i 0 910   9100 8700 - - - - 0 .56 43 0 .019 5.0
loops/lu.cmp_true-unreach-call.i 1 3.3 260 30 - - - - 0 900    6500 0 960     4300  
loops/matrix_true-unreach-call_true-termination.i 2 3.9 280 32 - - - - 2 5.3  270 2 9.6   370  
loops/n.c11_true-unreach-call_false-termination.i 2 2.5 250 26 - - - - 0 790    7000 2 9.3   340  
loops/n.c40_true-unreach-call_true-termination.i 2 5.2 280 54 - - - - 2 2.5  260 2 7.6   350  
loops/nec40_true-unreach-call_true-termination.i 2 4.1 280 38 - - - - 2 4.1  290 2 8.6   340  
loops/string_true-unreach-call_true-termination.i 2 3.5 260 30 - - - - 2 9.0  360 -16 13     450  
loops/sum01_true-unreach-call_true-termination.i 2 260   3200 3000 - - - - 0 420    7000 2 9.4   390  
loops/sum03_true-unreach-call_false-termination.i 2 180   2300 2100 - - - - 2 4.8  270 2 5.4   250  
loops/sum04_true-unreach-call_true-termination.i 2 2.3 250 23 - - - - 2 5.0  280 2 15     540  
loops/sum_array_true-unreach-call.i 0 900   4500 6400 - - - - 0 .56 44 0 .019 4.9
loops/terminator_02_true-unreach-call_true-termination.i 2 3.4 260 27 - - - - 2 4.0  270 2 7.1   250  
loops/terminator_03_true-unreach-call_true-termination.i 2 3.3 260 30 - - - - 2 5.0  270 2 6.5   260  
loops/trex01_true-unreach-call_true-termination.i 2 16   590 160 - - - - 2 28    1100 2 6.0   270  
loops/trex02_true-unreach-call_true-termination.i 2 3.1 270 27 - - - - 2 3.7  260 2 5.2   250  
loops/trex03_true-unreach-call_true-termination.i 2 3.4 270 29 - - - - 2 4.4  290 2 5.9   260  
loops/trex04_true-unreach-call_false-termination.i 2 3.3 270 28 - - - - 2 5.0  270 2 5.5   260  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i 2 3.5 280 31 - - - - 0 370    7000 2 8.2   300  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i 2 150   1300 1700 - - - - 2 9.0  370 2 6.9   270  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i 2 4.0 270 40 - - - - 2 4.2  270 2 5.4   260  
loops/vogal_true-unreach-call.i 2 250   1900 2800 - - - - 2 100    1300 -16 27     620  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 2 2.3 240 20 - - - - 0 530    5200 2 4.9   260  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 2 2.4 240 22 - - - - 0 610    5200 2 6.0   260  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 2 2.4 250 21 - - - - 0 910    5200 2 5.9   250  
loop-acceleration/array_false-unreach-call1_true-termination.i 1 140   2100 1700 0 97    1100 0 96     5300   0 12    390 1 1.1    39    - -
loop-acceleration/array_false-unreach-call2_true-termination.i 0 900   8700 12000 0 .54 43 0 .018 4.8 0 .86 48 0 .0016 .26 - -
loop-acceleration/array_false-unreach-call3_true-termination.i 0 900   7500 10000 0 .54 44 0 .021 5.0 0 .85 49 0 .0011 .33 - -
loop-acceleration/const_false-unreach-call1.i 1 74   1200 840 1 19    1000 0 96     6100   0 21    670 1 1.9    54    - -
loop-acceleration/diamond_false-unreach-call1.i 1 45   1100 580 1 5.6  280 0 80     7000   0 3.7  220 1 .72   20    - -
loop-acceleration/functions_false-unreach-call1_true-termination.i 0 900   8100 10000 0 .58 44 0 .019 4.9 0 .83 47 0 .0016 .28 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i 1 2.5 260 20 1 4.0  260 1 5.7   250   0 3.6  190 1 .61   18    - -
loop-acceleration/nested_false-unreach-call1.i 0 900   5200 10000 0 .65 41 0 .019 4.8 0 1.0  49 0 .0012 .26 - -
loop-acceleration/phases_false-unreach-call1.i 0 900   5700 9500 0 .52 41 0 .019 5.0 0 .87 49 0 .0014 .26 - -
loop-acceleration/phases_false-unreach-call2_false-termination.i 1 2.5 250 25 1 3.7  260 1 5.0   250   0 2.9  180 1 .70   18    - -
loop-acceleration/simple_false-unreach-call1.i 0 910   7300 10000 0 .54 41 0 .023 4.9 0 .96 50 0 .0017 .26 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i 1 2.5 250 21 1 3.1  260 1 5.0   250   0 2.9  180 1 .79   18    - -
loop-acceleration/simple_false-unreach-call3_true-termination.i 1 2.6 250 22 1 3.5  280 1 4.8   250   0 3.4  210 1 .58   18    - -
loop-acceleration/simple_false-unreach-call4.i 0 900   7000 9800 0 .57 43 0 .019 4.8 0 .86 47 0 .0015 .27 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i 1 2.7 250 24 1 3.7  260 1 8.5   330   0 3.0  210 1 .57   19    - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i 1 2.8 260 25 1 3.5  260 1 8.4   340   0 3.1  210 1 .60   19    - -
loop-acceleration/array_true-unreach-call1_true-termination.i 2 92   460 1200 - - - - 2 9.8  570 0 12     320  
loop-acceleration/array_true-unreach-call2_true-termination.i 0 900   8600 11000 - - - - 0 .53 43 0 .019 4.9
loop-acceleration/array_true-unreach-call3_true-termination.i 2 10   660 89 - - - - 2 12    750 0 10     320  
loop-acceleration/array_true-unreach-call4_true-termination.i 1 11   470 86 - - - - 0 910    6300 0 8.7   220  
loop-acceleration/const_true-unreach-call1.i 2 5.2 280 46 - - - - 2 4.5  260 -16 5.2   260  
loop-acceleration/diamond_true-unreach-call1_true-termination.i 2 160   1900 2100 - - - - 2 13    480 0 960     680  
loop-acceleration/diamond_true-unreach-call2.i 2 5.8 310 51 - - - - 2 6.9  310 2 65     690  
loop-acceleration/functions_true-unreach-call1_true-termination.i 0 900   8000 9400 - - - - 0 .64 43 0 .019 4.8
loop-acceleration/multivar_true-unreach-call1_true-termination.i 2 2.9 260 27 - - - - 2 760    6200 2 6.5   250  
loop-acceleration/nested_true-unreach-call1.i 2 350   3600 5200 - - - - 2 5.5  270 2 26     550  
loop-acceleration/overflow_true-unreach-call1.i 0 900   6800 9200 - - - - 0 .68 43 0 .021 4.9
loop-acceleration/phases_true-unreach-call1.i 0 900   6400 9200 - - - - 0 .61 41 0 .019 4.9
loop-acceleration/phases_true-unreach-call2_false-termination.i 2 3.1 260 26 - - - - 0 900    410 2 6.6   260  
loop-acceleration/simple_true-unreach-call1.i 0 910   7300 9000 - - - - 0 .62 42 0 .019 4.9
loop-acceleration/simple_true-unreach-call2_true-termination.i 2 3.1 260 23 - - - - 2 3.8  260 2 6.0   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i 0 900   6600 8900 - - - - 0 .58 41 0 .019 4.8
loop-acceleration/simple_true-unreach-call4.i 2 150   1300 1800 - - - - 2 3.5  260 2 6.3   260  
loop-acceleration/underapprox_true-unreach-call1_true-termination.i 2 2.4 240 21 - - - - 2 5.3  350 2 15     520  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i 2 2.4 250 21 - - - - 2 4.4  270 2 14     490  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i 1 2.9 260 26 1 3.6  270 1 5.9   240   0 2.8  180 -32 .61   18    - -
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i 0 900   3700 9400 - - - - 0 .55 42 0 .019 4.8
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i 0 900   3400 9900 - - - - 0 .56 44 0 .020 5.0
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i 0 900   5800 8100 - - - - 0 .53 41 0 .019 4.8
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i 2 7.7 490 88 - - - - 0 900    1800 2 62     460  
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i 2 350   2700 4200 - - - - 2 4.4  270 -16 5.9   260  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i 2 150   2300 1700 - - - - 2 3.9  270 2 5.5   260  
loop-invgen/id_trans_false-unreach-call_true-termination.i 1 3.4 270 29 1 3.9  260 1 6.9   260   0 2.8  190 1 .71   19    - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 0 900   3200 9400 - - - - 0 .67 41 0 .019 4.9
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i 0 910   10000 9300 - - - - 0 .65 43 0 .025 4.8
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 2 8.4 340 95 - - - - 0 900    4400 2 12     490  
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 2 4.7 280 38 - - - - 0 900    2500 2 14     510  
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 2 210   2500 2500 - - - - 2 6.0  290 2 10     430  
loop-invgen/down_true-unreach-call_true-termination.i 0 910   12000 9300 - - - - 0 .64 43 0 .020 4.9
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 0 900   11000 8800 - - - - 0 .59 42 0 .019 4.9
loop-invgen/half_2_true-unreach-call_true-termination.i 0 900   7700 8800 - - - - 0 .66 44 0 .019 4.9
loop-invgen/heapsort_true-unreach-call_true-termination.i 0 900   5100 9200 - - - - 0 .72 43 0 .019 4.9
loop-invgen/id_build_true-unreach-call_true-termination.i 2 200   1800 2700 - - - - 2 5.0  280 -16 10     330  
loop-invgen/large_const_true-unreach-call_true-termination.i 2 3.8 270 35 - - - - 2 4.5  270 2 9.6   340  
loop-invgen/nest-if3_true-unreach-call_true-termination.i 0 900   5000 11000 - - - - 0 .53 45 0 .020 4.9
loop-invgen/nested6_true-unreach-call_true-termination.i 0 910   8900 9400 - - - - 0 .41 44 0 .024 5.0
loop-invgen/nested9_true-unreach-call_true-termination.i 0 900   6100 9200 - - - - 0 .65 41 0 .019 4.8
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 0 900   9700 8700 - - - - 0 .62 41 0 .020 4.9
loop-invgen/seq_true-unreach-call_true-termination.i 0 900   11000 10000 - - - - 0 .56 41 0 .018 4.9
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i 0 900   10000 9200 - - - - 0 .58 44 0 .018 5.0
loop-invgen/up_true-unreach-call_true-termination.i 0 810   15000 7200 - - - - 0 .55 41 0 .019 5.0
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 1 8.2 460 70 - - - - 0 390    7000 0 11     300  
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i 0 900   2000 9700 - - - - 0 .51 41 0 .023 4.9
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i 2 2.5 250 22 - - - - 2 5.9  280 2 10     440  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i 0 910   7100 9100 - - - - 0 .65 44 0 .020 4.8
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i 2 4.1 270 35 - - - - 2 8.0  410 0 960     1900  
loop-lit/css2003_true-unreach-call_true-termination.c.i 2 3.4 270 34 - - - - 2 4.3  270 2 6.6   260  
loop-lit/ddlm2013_true-unreach-call.i 0 900   7000 12000 - - - - 0 .66 41 0 .019 4.9
loop-lit/gj2007_true-unreach-call_true-termination.c.i 2 3.3 260 30 - - - - 2 160    3200 -16 5.6   250  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 0 900   4500 9500 - - - - 0 .53 41 0 .019 4.9
loop-lit/gr2006_true-unreach-call_true-termination.c.i 2 3.7 260 29 - - - - 2 55    1000 -16 6.0   260  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i 1 570   2600 7300 - - - - 0 900    2400 0 960     2200  
loop-lit/hhk2008_true-unreach-call_true-termination.c.i 0 910   7900 9600 - - - - 0 .71 43 0 .019 4.9
loop-lit/jm2006_true-unreach-call_true-termination.c.i 2 3.4 270 29 - - - - 0 900    5800 2 9.8   290  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i 0 900   6900 9900 - - - - 0 .55 45 0 .021 4.9
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 0 900   4300 8400 - - - - 0 .69 44 0 .019 4.9
loop-lit/gcnr2008_false-unreach-call_false-termination.i 1 2.6 250 22 1 3.3  260 1 5.6   250   0 2.8  180 1 .83   18    - -
loop-new/count_by_1_true-unreach-call_true-termination.i 2 350   3100 4200 - - - - 2 3.8  270 -16 5.3   260  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i 2 350   3600 3800 - - - - 2 4.5  270 -16 7.3   260  
loop-new/count_by_2_true-unreach-call_true-termination.i 0 900   6700 8400 - - - - 0 .72 43 0 .023 4.8
loop-new/count_by_k_true-unreach-call_true-termination.i 0 900   3500 9600 - - - - 0 .53 43 0 .020 4.9
loop-new/count_by_nondet_true-unreach-call_true-termination.i 0 900   3300 9300 - - - - 0 .54 43 0 .021 4.9
loop-new/gauss_sum_true-unreach-call_true-termination.i 1 240   2500 2700 - - - - 0 700    7000 0 960     1000  
loop-new/half_true-unreach-call_true-termination.i 0 900   6200 9500 - - - - 0 .65 43 0 .020 4.9
loop-new/nested_true-unreach-call_true-termination.i 0 900   5100 9400 - - - - 0 .67 43 0 .020 4.8
loop-industry-pattern/aiob_1_true-unreach-call.c 2 30   680 260 - - - - 2 39    590 0 960     1900  
loop-industry-pattern/aiob_2_true-unreach-call.c 2 29   700 270 - - - - 2 38    610 0 960     2000  
loop-industry-pattern/aiob_3_true-unreach-call.c 2 28   700 260 - - - - 2 39    590 0 960     1900  
loop-industry-pattern/aiob_4_true-unreach-call.c 2 29   700 320 - - - - 2 37    480 0 960     2000  
loop-industry-pattern/mod3_true-unreach-call.c 2 20   290 240 - - - - 2 7.2  300 2 18     270  
loop-industry-pattern/nested_true-unreach-call.c 0 900   5200 9600 - - - - 0 .55 41 0 .021 4.9
loop-industry-pattern/ofuf_1_true-unreach-call.c 2 63   2500 550 - - - - 0 3.5  270 2 29     610  
loop-industry-pattern/ofuf_2_true-unreach-call.c 2 59   2500 540 - - - - 0 4.7  260 2 25     580  
loop-industry-pattern/ofuf_3_true-unreach-call.c 2 60   2400 550 - - - - 0 4.4  280 2 23     580  
loop-industry-pattern/ofuf_4_true-unreach-call.c 2 59   2500 550 - - - - 0 4.1  250 2 22     580  
loop-industry-pattern/ofuf_5_true-unreach-call.c 2 58   2400 550 - - - - 0 5.3  260 2 24     590  
loops/heavy_true-unreach-call.c 1 93   2200 1300 - - - - 0 790    7000 0 180     7000  
loops/compact_false-unreach-call.c 0 900   6200 8400 0 .66 44 0 .021 4.8 0 .77 48 0 .0013 .27 - -
loops/heavy_false-unreach-call.c 0 900   3100 9700 0 .54 41 0 .020 5.0 0 1.0  49 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 178 51000 430000 540000 52 -93 370 16000 52 34 900 42000 52 0 260 12000 52 -227 28   820 111 96 16000 130000 111 -48 11000 55000
    correct results 106 171 4900 85000 57000 35 35 150 10000 34 34 340 11000 0 29 29 21   590 48 96 1500 27000 48 96 1200 18000
        correct true 65 130 4100 64000 48000 0 0 0 0 48 96 1500 27000 48 96 1200 18000
        correct false 41 41 740 21000 8600 35 35 150 10000 34 34 340 11000 0 29 29 21   590 0 0
    correct-unconfimed results 7 7 930 8800 12000 0 0 0 0 0 0
        correct-unconfirmed true 7 7 930 8800 12000 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 4 -128 18 1100 0 0 8 -256 5.0 150 0 9 -144 86 3000
        incorrect true 0 4 -128 18 1100 0 0 8 -256 5.0 150 0 0
        incorrect false 0 0 0 0 0 0 9 -144 86 3000
score (163 tasks, max score: 274) 178 -93 34 0 -227 96 -48
Run set cpa-seq.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Loops