Tool VeriAbs CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon020; apollon077; apollon078; apollon084; apollon149; apollon164] apollon* [apollon037; apollon065; apollon077; apollon078; apollon155; apollon159] 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 18:04:04 CET 2017-12-03 04:46:33 CET 2017-12-03 06:08:30 CET 2017-12-03 06:21:09 CET 2017-12-03 06:27:12 CET 2017-12-03 03:55:53 CET 2017-12-03 04:55:47 CET
Run set veriabs.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Loops
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/veriabs.2017-12-02_1804.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 1.8 150 17 -32 4.8  260 1 3.4   260   0 2.0  210 1 .67   18    - -
loops/bubble_sort_false-unreach-call.i 0 330   700 2500 0 .40 44 0 .020 4.9 0 .67 49 0 .0011 .32 - -
loops/count_up_down_false-unreach-call_true-termination.i 1 11   280 79 0 92    2000 1 4.8   250   0 2.9  210 1 .58   18    - -
loops/eureka_01_false-unreach-call_true-termination.i 0 480   370 6200 0 92    2000 0 98     3300   0 3.4  210 0 .64   19    - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i 1 14   280 100 1 3.6  260 1 5.4   260   0 3.0  210 1 .58   18    - -
loops/insertion_sort_false-unreach-call_true-termination.i 1 570   3300 6400 0 92    2000 1 10     410   0 2.3  210 1 .65   19    - -
loops/invert_string_false-unreach-call_true-termination.i 1 34   340 270 0 92    2000 1 5.7   260   0 3.0  210 1 .62   19    - -
loops/linear_search_false-unreach-call.i 0 18   280 150 0 2.4  170 1 15     540   0 1.9  180 0 .57   19    - -
loops/ludcmp_false-unreach-call.i 0 270   1300 3500 -32 8.6  320 0 97     4500   0 3.7  270 0 3.7    19    - -
loops/matrix_false-unreach-call_true-termination.i 1 470   3200 4600 0 91    1900 1 4.0   270   0 2.8  210 0 .60   18    - -
loops/n.c24_false-unreach-call.i 0 900   3700 6100 0 .55 41 0 .020 4.8 0 .66 50 0 .0014 .26 - -
loops/nec11_false-unreach-call_false-termination.i 1 18   280 120 -32 2.2  260 1 5.3   250   0 2.6  210 1 .58   18    - -
loops/nec20_false-unreach-call_true-termination.i 1 23   290 190 1 3.9  260 1 3.6   260   0 3.0  210 0 .67   18    - -
loops/s3_false-unreach-call.i 0 630   1800 7600 0 .39 43 0 .020 4.9 0 .84 49 0 .0037 .26 - -
loops/string_false-unreach-call_true-termination.i 1 36   320 250 -32 3.1  290 1 12     300   0 3.2  210 -32 .64   19    - -
loops/sum01_bug02_false-unreach-call_true-termination.i 1 19   330 130 0 92    2000 1 7.3   280   0 2.1  210 1 .62   19    - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 1 17   290 130 0 92    2000 1 7.4   280   0 2.2  210 -32 .59   19    - -
loops/sum01_false-unreach-call_true-termination.i 1 19   340 140 0 92    2000 1 9.6   570   0 3.0  210 -32 .60   19    - -
loops/sum03_false-unreach-call_true-termination.i 1 19   460 140 -32 4.2  270 1 69     6600   0 3.1  210 1 .70   19    - -
loops/sum04_false-unreach-call_true-termination.i 1 17   310 140 -32 3.6  260 1 6.7   330   0 2.3  210 1 .60   19    - -
loops/sum_array_false-unreach-call.i 0 2.0 160 17 0 2.8  170 1 7.9   310   0 1.8  170 0 .56   19    - -
loops/terminator_01_false-unreach-call_true-termination.i 1 11   280 77 -32 2.1  260 1 5.3   260   0 2.7  210 1 .60   18    - -
loops/terminator_02_false-unreach-call_true-termination.i 1 15   280 110 -32 3.1  260 1 5.0   250   0 2.0  210 1 .58   18    - -
loops/terminator_03_false-unreach-call_true-termination.i 1 11   280 86 1 2.3  290 1 6.1   260   0 2.0  210 1 .61   18    - -
loops/trex01_false-unreach-call_true-termination.i 1 16   280 130 -32 2.8  260 1 5.7   260   0 2.1  210 -32 .63   18    - -
loops/trex02_false-unreach-call_true-termination.i 1 15   280 120 1 3.2  260 1 5.2   260   0 2.1  210 1 .61   18    - -
loops/trex03_false-unreach-call_true-termination.i 1 15   280 140 -32 3.5  260 1 4.9   260   0 3.0  210 1 .61   18    - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i 1 19   300 130 1 3.6  260 1 8.8   320   0 2.9  210 1 .57   18    - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i 1 27   290 220 1 3.4  260 1 9.9   540   0 3.0  210 0 .63   19    - -
loops/vogal_false-unreach-call.i 1 30   470 210 -32 6.4  420 0 96     840   0 2.4  210 1 .68   20    - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 1 14   280 100 0 96    2700 1 4.6   250   0 97    2700 1 .60   18    - -
loops/array_true-unreach-call_true-termination.i 2 1.7 150 15 - - - - 2 4.1  270 2 8.4   280  
loops/bubble_sort_true-unreach-call_true-termination.i 2 12   270 96 - - - - 2 3.5  280 2 5.1   240  
loops/count_up_down_true-unreach-call_true-termination.i 1 84   1300 700 - - - - 0 430    7000 0 960     700  
loops/eureka_01_true-unreach-call.i 1 63   720 590 - - - - 0 900    5900 0 210     7000  
loops/eureka_05_true-unreach-call_true-termination.i 2 66   900 640 - - - - 0 930    6700 2 100     1000  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 2 12   290 79 - - - - 2 4.6  270 2 5.8   260  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 2 11   280 78 - - - - 2 4.8  270 2 5.7   260  
loops/insertion_sort_true-unreach-call_true-termination.i 0 800   220 9100 - - - - 0 .54 43 0 .021 5.0
loops/invert_string_true-unreach-call_true-termination.i 2 36   530 310 - - - - 2 23    520 2 150     850  
loops/linear_sea.ch_true-unreach-call.i 1 92   1200 970 - - - - 0 720    7000 0 960     690  
loops/lu.cmp_true-unreach-call.i 1 250   1200 2700 - - - - 0 190    7000 0 960     4500  
loops/matrix_true-unreach-call_true-termination.i 2 21   290 140 - - - - 2 5.2  280 2 20     380  
loops/n.c11_true-unreach-call_false-termination.i 2 380   2500 2700 - - - - 0 910    6100 2 7.4   290  
loops/n.c40_true-unreach-call_true-termination.i 2 36   280 310 - - - - 2 4.8  260 2 7.2   340  
loops/nec40_true-unreach-call_true-termination.i 2 54   290 520 - - - - 2 3.6  260 2 7.0   350  
loops/string_true-unreach-call_true-termination.i 2 18   220 130 - - - - 2 5.1  280 2 9.7   370  
loops/sum01_true-unreach-call_true-termination.i 0 83   1200 670 - - - - 0 .60 45 0 3.6   190  
loops/sum03_true-unreach-call_false-termination.i 2 12   290 87 - - - - 2 5.3  270 2 5.8   260  
loops/sum04_true-unreach-call_true-termination.i 2 13   280 98 - - - - 2 4.0  270 2 9.3   380  
loops/sum_array_true-unreach-call.i 1 23   220 190 - - - - 0 900    2800 0 960     1600  
loops/terminator_02_true-unreach-call_true-termination.i 2 13   280 100 - - - - 2 6.5  280 2 8.1   330  
loops/terminator_03_true-unreach-call_true-termination.i 2 13   310 84 - - - - 2 5.0  270 2 5.9   260  
loops/trex01_true-unreach-call_true-termination.i 2 14   300 100 - - - - 2 7.9  280 2 9.0   330  
loops/trex02_true-unreach-call_true-termination.i 2 11   280 100 - - - - 2 3.6  270 2 5.3   250  
loops/trex03_true-unreach-call_true-termination.i 2 13   280 100 - - - - 2 5.6  270 2 6.2   270  
loops/trex04_true-unreach-call_false-termination.i 2 13   280 100 - - - - 2 5.6  280 2 6.0   260  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i 2 82   1200 710 - - - - 0 390    7000 2 10     300  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i 2 50   600 460 - - - - 2 8.7  400 2 30     590  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i 2 16   280 130 - - - - 2 5.1  270 2 18     310  
loops/vogal_true-unreach-call.i 2 77   800 610 - - - - 2 58    1000 2 370     1500  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 2 11   270 88 - - - - 0 590    5200 2 5.3   260  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 2 10   280 84 - - - - 0 610    5200 2 3.8   260  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 2 11   270 76 - - - - 0 910    5200 2 5.6   240  
loop-acceleration/array_false-unreach-call1_true-termination.i 1 250   3700 2800 0 91    790 -32 2.8   210   0 2.7  190 1 .58   18    - -
loop-acceleration/array_false-unreach-call2_true-termination.i 1 5.8 220 52 -32 8.8  440 0 87     7000   0 3.0  230 1 1.9    19    - -
loop-acceleration/array_false-unreach-call3_true-termination.i 0 490   3700 7100 -32 62    3200 0 48     7000   0 47    3100 0 96      60    - -
loop-acceleration/const_false-unreach-call1.i 1 240   3700 2700 1 17    750 -32 3.2   210   0 1.9  210 1 .57   18    - -
loop-acceleration/diamond_false-unreach-call1.i 1 86   1900 900 -32 5.0  280 0 64     7000   0 2.7  220 1 .60   20    - -
loop-acceleration/functions_false-unreach-call1_true-termination.i 0 86   220 880 0 .39 43 0 .046 4.8 0 .83 47 0 .0016 .26 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i 1 11   280 92 -32 2.2  260 1 5.2   250   0 2.8  210 1 .57   18    - -
loop-acceleration/nested_false-unreach-call1.i 0 300   7300 3500 0 .40 41 0 .020 4.9 0 .90 49 0 .0020 .29 - -
loop-acceleration/phases_false-unreach-call1.i 1 400   7200 4800 0 92    1900 -32 5.3   210   0 2.7  210 1 .87   18    - -
loop-acceleration/phases_false-unreach-call2_false-termination.i 1 18   290 150 -32 3.4  260 1 5.4   260   0 2.7  210 1 .58   18    - -
loop-acceleration/simple_false-unreach-call1.i 1 240   3700 2600 0 92    1800 -32 4.8   210   0 2.9  180 1 .81   18    - -
loop-acceleration/simple_false-unreach-call2_true-termination.i 1 11   280 82 1 2.2  260 1 5.2   250   0 1.9  210 1 .60   18    - -
loop-acceleration/simple_false-unreach-call3_true-termination.i 1 15   280 120 1 3.1  260 1 4.9   250   0 2.0  210 1 .66   18    - -
loop-acceleration/simple_false-unreach-call4.i 1 220   2100 3100 0 91    1700 -32 4.3   210   0 2.7  210 1 .81   18    - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i 1 15   290 110 1 3.2  260 1 5.9   350   0 3.1  210 1 .57   19    - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i 1 15   290 120 1 4.0  260 1 8.3   350   0 2.2  210 1 .71   19    - -
loop-acceleration/array_true-unreach-call1_true-termination.i 2 18   280 140 - - - - 2 4.0  270 2 8.6   370  
loop-acceleration/array_true-unreach-call2_true-termination.i 1 3.1 210 23 - - - - 0 900    2700 0 960     2900  
loop-acceleration/array_true-unreach-call3_true-termination.i 2 15   220 94 - - - - 2 4.1  280 2 8.4   330  
loop-acceleration/array_true-unreach-call4_true-termination.i 1 15   220 120 - - - - 0 900    3800 0 120     7000  
loop-acceleration/const_true-unreach-call1.i 2 12   280 88 - - - - 2 4.1  270 2 7.6   300  
loop-acceleration/diamond_true-unreach-call1_true-termination.i 2 37   740 310 - - - - 2 14    480 0 960     710  
loop-acceleration/diamond_true-unreach-call2.i 2 25   480 200 - - - - 2 8.2  310 2 80     690  
loop-acceleration/functions_true-unreach-call1_true-termination.i 1 79   1200 760 - - - - 0 900    6800 0 960     710  
loop-acceleration/multivar_true-unreach-call1_true-termination.i 2 12   270 98 - - - - 2 4.9  270 2 5.1   260  
loop-acceleration/nested_true-unreach-call1.i 2 11   270 97 - - - - 2 4.6  270 2 26     500  
loop-acceleration/overflow_true-unreach-call1.i 1 79   1200 730 - - - - 0 480    7000 0 960     620  
loop-acceleration/phases_true-unreach-call1.i 1 240   7200 2600 - - - - 0 500    7000 0 960     640  
loop-acceleration/phases_true-unreach-call2_false-termination.i 2 12   300 100 - - - - 2 5.4  340 2 6.2   260  
loop-acceleration/simple_true-unreach-call1.i 1 79   1200 800 - - - - 0 490    7000 0 960     580  
loop-acceleration/simple_true-unreach-call2_true-termination.i 2 12   280 91 - - - - 2 4.0  270 2 5.1   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i 1 80   1200 750 - - - - 0 750    7000 0 960     560  
loop-acceleration/simple_true-unreach-call4.i 2 12   270 99 - - - - 2 4.0  260 2 6.8   260  
loop-acceleration/underapprox_true-unreach-call1_true-termination.i 2 16   300 110 - - - - 2 5.3  290 2 49     490  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i 2 11   280 86 - - - - 2 4.4  270 2 7.6   290  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i 1 560   5400 8500 1 3.6  260 -32 4.2   210   0 2.0  210 -32 .58   18    - -
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i 1 15   220 89 - - - - 0 900    4200 0 960     660  
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i 1 16   220 96 - - - - 0 900    730 0 960     730  
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i 1 15   220 100 - - - - 0 910    6200 0 960     740  
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i 2 17   220 120 - - - - 0 900    1800 2 65     470  
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i 2 12   280 99 - - - - 2 4.9  270 2 6.9   270  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i 2 12   280 96 - - - - 2 5.4  270 2 7.7   270  
loop-invgen/id_trans_false-unreach-call_true-termination.i 1 16   280 120 -32 3.5  260 1 5.2   260   0 3.0  210 1 .63   19    - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 2 83   860 790 - - - - 0 900    2600 2 11     450  
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i 2 80   1300 790 - - - - 0 710    7000 2 8.9   380  
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 2 95   850 810 - - - - 0 900    4400 2 14     510  
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 0 900   9400 8400 - - - - 0 .70 42 0 .018 4.9
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 0 900   4600 7800 - - - - 0 .68 42 0 .020 4.9
loop-invgen/down_true-unreach-call_true-termination.i 1 89   1400 750 - - - - 0 900    4200 0 960     1300  
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 1 13   230 75 - - - - 0 540    7000 0 960     4600  
loop-invgen/half_2_true-unreach-call_true-termination.i 1 91   1100 650 - - - - 0 880    7000 0 960     4700  
loop-invgen/heapsort_true-unreach-call_true-termination.i 2 140   890 1300 - - - - 0 900    2800 2 67     570  
loop-invgen/id_build_true-unreach-call_true-termination.i 2 13   290 96 - - - - 2 5.5  280 2 5.7   340  
loop-invgen/large_const_true-unreach-call_true-termination.i 2 20   290 140 - - - - 2 6.2  310 -16 5.5   270  
loop-invgen/nest-if3_true-unreach-call_true-termination.i 2 84   800 790 - - - - 0 900    3300 2 11     390  
loop-invgen/nested6_true-unreach-call_true-termination.i 0 900   8000 5900 - - - - 0 .54 42 0 .020 4.9
loop-invgen/nested9_true-unreach-call_true-termination.i 2 90   860 890 - - - - 0 900    4200 2 10     450  
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 1 760   3900 6500 - - - - 0 650    7000 -16 5.5   260  
loop-invgen/seq_true-unreach-call_true-termination.i 1 98   1000 870 - - - - 0 690    7000 0 960     2200  
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i 1 93   1300 800 - - - - 0 900    3600 0 960     4600  
loop-invgen/up_true-unreach-call_true-termination.i 1 88   1400 740 - - - - 0 900    5200 0 960     1300  
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 2 7.9 220 58 - - - - 0 310    7000 2 6.7   270  
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i 2 120   720 1300 - - - - 0 900    650 2 9.3   440  
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i 2 13   280 97 - - - - 2 5.7  270 2 7.9   310  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i 2 81   1400 700 - - - - 0 370    7000 2 5.9   340  
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i 2 8.8 230 61 - - - - 2 5.4  270 2 6.8   260  
loop-lit/css2003_true-unreach-call_true-termination.c.i 2 9.3 210 70 - - - - 2 3.7  270 2 5.9   270  
loop-lit/ddlm2013_true-unreach-call.i 0 560   2200 5600 - - - - 0 .59 42 0 .021 4.9
loop-lit/gj2007_true-unreach-call_true-termination.c.i 2 19   440 130 - - - - 2 6.0  290 2 28     690  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 2 86   1100 770 - - - - 0 900    2500 2 9.3   360  
loop-lit/gr2006_true-unreach-call_true-termination.c.i 2 30   610 190 - - - - 2 6.7  300 2 37     860  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i 2 160   800 1900 - - - - 0 900    1300 2 7.5   320  
loop-lit/hhk2008_true-unreach-call_true-termination.c.i 2 82   1300 720 - - - - 0 410    7000 2 8.6   330  
loop-lit/jm2006_true-unreach-call_true-termination.c.i 1 82   1300 650 - - - - 0 900    6100 0 960     2900  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i 2 82   1300 740 - - - - 0 910    3600 2 9.0   330  
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 1 100   620 1200 - - - - 0 780    7000 0 960     1400  
loop-lit/gcnr2008_false-unreach-call_false-termination.i 1 16   280 120 0 92    2200 1 4.8   250   0 2.9  210 1 .59   18    - -
loop-new/count_by_1_true-unreach-call_true-termination.i 2 11   290 85 - - - - 2 3.7  290 2 6.2   260  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i 2 14   280 120 - - - - 2 4.1  270 2 7.0   270  
loop-new/count_by_2_true-unreach-call_true-termination.i 1 79   1200 700 - - - - 0 480    7000 0 960     4800  
loop-new/count_by_k_true-unreach-call_true-termination.i 1 78   1100 710 - - - - 0 900    2200 0 960     3200  
loop-new/count_by_nondet_true-unreach-call_true-termination.i 0 900   850 7500 - - - - 0 .54 42 0 .019 4.9
loop-new/gauss_sum_true-unreach-call_true-termination.i 1 79   230 940 - - - - 0 910    6500 0 960     980  
loop-new/half_true-unreach-call_true-termination.i 0 590   3500 6300 - - - - 0 .51 43 0 .019 4.8
loop-new/nested_true-unreach-call_true-termination.i 0 900   3900 5600 - - - - 0 .70 43 0 .018 4.9
loop-industry-pattern/aiob_1_true-unreach-call.c 2 46   690 380 - - - - 2 62    800 2 160     1800  
loop-industry-pattern/aiob_2_true-unreach-call.c 2 43   680 410 - - - - 2 56    820 2 180     1900  
loop-industry-pattern/aiob_3_true-unreach-call.c 2 45   680 340 - - - - 2 63    830 2 180     1800  
loop-industry-pattern/aiob_4_true-unreach-call.c 2 43   690 360 - - - - 2 50    800 -16 8.9   590  
loop-industry-pattern/mod3_true-unreach-call.c 2 17   330 160 - - - - 2 7.7  340 2 15     280  
loop-industry-pattern/nested_true-unreach-call.c 2 89   880 850 - - - - 0 900    6900 2 17     570  
loop-industry-pattern/ofuf_1_true-unreach-call.c 2 26   350 230 - - - - 0 4.4  270 2 11     330  
loop-industry-pattern/ofuf_2_true-unreach-call.c 2 27   330 240 - - - - 0 3.5  250 2 7.6   330  
loop-industry-pattern/ofuf_3_true-unreach-call.c 2 26   350 240 - - - - 0 4.2  260 2 5.7   330  
loop-industry-pattern/ofuf_4_true-unreach-call.c 2 27   340 220 - - - - 0 3.3  250 2 9.6   340  
loop-industry-pattern/ofuf_5_true-unreach-call.c 2 26   340 210 - - - - 0 3.7  260 2 9.9   340  
loops/heavy_true-unreach-call.c 1 23   770 190 - - - - 0 900    7000 0 170     7000  
loops/compact_false-unreach-call.c 0 140   450 1600 0 91    2600 0 97     5100   0 27    1900 0 96      110    - -
loops/heavy_false-unreach-call.c 0 900   12000 7900 0 .40 43 0 .019 4.9 0 .88 47 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 216 20000 180000 200000 52 -532 1600 42000 52 -159 890 52000 52 0 290 17000 52 -128 220   980 111 96 38000 270000 111 94 27000 100000
    correct results 114 188 6500 81000 66000 12 12 53 3600 33 33 280 16000 0 32 32 22   590 48 96 540 17000 71 142 2000 32000
        correct true 74 148 3000 38000 26000 0 0 0 0 48 96 540 17000 71 142 2000 32000
        correct false 40 40 3500 43000 40000 12 12 53 3600 33 33 280 16000 0 32 32 22   590 0 0
    correct-unconfimed results 34 28 4200 39000 44000 0 0 0 0 0 0
        correct-unconfirmed true 28 28 2800 33000 26000 0 0 0 0 0 0
        correct-unconfirmed false 6 0 1400 6200 18000 0 0 0 0 0 0
    incorrect results 0 17 -544 130 7700 6 -192 25 1300 0 5 -160 3.0 93 0 3 -48 20 1100
        incorrect true 0 17 -544 130 7700 6 -192 25 1300 0 5 -160 3.0 93 0 0
        incorrect false 0 0 0 0 0 0 3 -48 20 1100
score (163 tasks, max score: 274) 216 -532 -159 0 -128 96 94
Run set veriabs.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Loops