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 false(unreach-call) 1 wit inspect 1.8 150 17 true -32 wit inspect 4.8  260 false(unreach-call) 1 wit inspect 3.4   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
loops/bubble_sort_false-unreach-call.i unknown 0 wit inspect 330   700 2500 error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 11   280 79 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 480   370 6200 timeout 0 wit inspect 92    2000 timeout 0 wit inspect 98     3300   unknown 0 wit inspect 3.4  210 error (2) 0 wit inspect .64   19    - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 14   280 100 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 570   3300 6400 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 10     410   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 34   340 270 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 5.7   260   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i false(unreach-call) 0 wit inspect 18   280 150 error (invalid witness file) 0 wit inspect 2.4  170 false(unreach-call) 1 wit inspect 15     540   error (invalid witness file) 0 wit inspect 1.9  180 error (1) 0 wit inspect .57   19    - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 0 wit inspect 270   1300 3500 true -32 wit inspect 8.6  320 timeout 0 wit inspect 97     4500   unknown 0 wit inspect 3.7  270 error (2) 0 wit inspect 3.7    19    - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 470   3200 4600 timeout 0 wit inspect 91    1900 false(unreach-call) 1 wit inspect 4.0   270   unknown 0 wit inspect 2.8  210 error (2) 0 wit inspect .60   18    - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i timeout 0 wit inspect 900   3700 6100 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 18   280 120 true -32 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 5.3   250   unknown 0 wit inspect 2.6  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 23   290 190 false(unreach-call) 1 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 3.6   260   unknown 0 wit inspect 3.0  210 error (2) 0 wit inspect .67   18    - wit inspect - wit inspect
loops/s3_false-unreach-call.i unknown 0 wit inspect 630   1800 7600 error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 36   320 250 true -32 wit inspect 3.1  290 false(unreach-call) 1 wit inspect 12     300   unknown 0 wit inspect 3.2  210 true -32 wit inspect .64   19    - wit inspect - wit inspect
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 19   330 130 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 7.3   280   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 17   290 130 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 7.4   280   unknown 0 wit inspect 2.2  210 true -32 wit inspect .59   19    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 19   340 140 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 9.6   570   unknown 0 wit inspect 3.0  210 true -32 wit inspect .60   19    - wit inspect - wit inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 19   460 140 true -32 wit inspect 4.2  270 false(unreach-call) 1 wit inspect 69     6600   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .70   19    - wit inspect - wit inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 17   310 140 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 6.7   330   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
loops/sum_array_false-unreach-call.i false(unreach-call) 0 wit inspect 2.0 160 17 error (invalid witness file) 0 wit inspect 2.8  170 false(unreach-call) 1 wit inspect 7.9   310   error (invalid witness file) 0 wit inspect 1.8  170 error (1) 0 wit inspect .56   19    - wit inspect - wit inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 11   280 77 true -32 wit inspect 2.1  260 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 15   280 110 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.0   250   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 11   280 86 false(unreach-call) 1 wit inspect 2.3  290 false(unreach-call) 1 wit inspect 6.1   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16   280 130 true -32 wit inspect 2.8  260 false(unreach-call) 1 wit inspect 5.7   260   unknown 0 wit inspect 2.1  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 15   280 120 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 15   280 140 true -32 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 19   300 130 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 8.8   320   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 27   290 220 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 9.9   540   unknown 0 wit inspect 3.0  210 error (2) 0 wit inspect .63   19    - wit inspect - wit inspect
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect 30   470 210 true -32 wit inspect 6.4  420 timeout 0 wit inspect 96     840   unknown 0 wit inspect 2.4  210 false(unreach-call) 1 wit inspect .68   20    - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 14   280 100 timeout 0 wit inspect 96    2700 false(unreach-call) 1 wit inspect 4.6   250   timeout 0 wit inspect 97    2700 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 1.7 150 15 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 8.4   280  
loops/bubble_sort_true-unreach-call_true-termination.i true 2 wit inspect 12   270 96 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  280 true 2 wit inspect 5.1   240  
loops/count_up_down_true-unreach-call_true-termination.i true 1 wit inspect 84   1300 700 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    7000 timeout 0 wit inspect 960     700  
loops/eureka_01_true-unreach-call.i true 1 wit inspect 63   720 590 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5900 out of memory 0 wit inspect 210     7000  
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect 66   900 640 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    6700 true 2 wit inspect 100     1000  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 12   290 79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  270 true 2 wit inspect 5.8   260  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 11   280 78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 true 2 wit inspect 5.7   260  
loops/insertion_sort_true-unreach-call_true-termination.i unknown 0 wit inspect 800   220 9100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 5.0
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect 36   530 310 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    520 true 2 wit inspect 150     850  
loops/linear_sea.ch_true-unreach-call.i true 1 wit inspect 92   1200 970 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    7000 timeout 0 wit inspect 960     690  
loops/lu.cmp_true-unreach-call.i true 1 wit inspect 250   1200 2700 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 190    7000 timeout 0 wit inspect 960     4500  
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 21   290 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  280 true 2 wit inspect 20     380  
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect 380   2500 2700 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 true 2 wit inspect 7.4   290  
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 36   280 310 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  260 true 2 wit inspect 7.2   340  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 54   290 520 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 7.0   350  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 18   220 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  280 true 2 wit inspect 9.7   370  
loops/sum01_true-unreach-call_true-termination.i witness invalid (true) 0 wit inspect 83   1200 670 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 45 error (invalid witness file) 0 wit inspect 3.6   190  
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect 12   290 87 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  270 true 2 wit inspect 5.8   260  
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 13   280 98 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 9.3   380  
loops/sum_array_true-unreach-call.i true 1 wit inspect 23   220 190 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 timeout 0 wit inspect 960     1600  
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 13   280 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  280 true 2 wit inspect 8.1   330  
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect 13   310 84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 true 2 wit inspect 5.9   260  
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 14   300 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  280 true 2 wit inspect 9.0   330  
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 11   280 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  270 true 2 wit inspect 5.3   250  
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect 13   280 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  270 true 2 wit inspect 6.2   270  
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect 13   280 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  280 true 2 wit inspect 6.0   260  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect 82   1200 710 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 10     300  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 50   600 460 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.7  400 true 2 wit inspect 30     590  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 16   280 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  270 true 2 wit inspect 18     310  
loops/vogal_true-unreach-call.i true 2 wit inspect 77   800 610 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 58    1000 true 2 wit inspect 370     1500  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 11   270 88 - wit inspect - wit inspect - wit inspect - wit inspect out of java memory 0 wit inspect 590    5200 true 2 wit inspect 5.3   260  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 10   280 84 - wit inspect - wit inspect - wit inspect - wit inspect out of java memory 0 wit inspect 610    5200 true 2 wit inspect 3.8   260  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect 11   270 76 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5200 true 2 wit inspect 5.6   240  
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 250   3700 2800 timeout 0 wit inspect 91    790 true -32 wit inspect 2.8   210   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 5.8 220 52 true -32 wit inspect 8.8  440 out of memory 0 wit inspect 87     7000   unknown 0 wit inspect 3.0  230 false(unreach-call) 1 wit inspect 1.9    19    - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 wit inspect 490   3700 7100 true -32 wit inspect 62    3200 out of memory 0 wit inspect 48     7000   unknown 0 wit inspect 47    3100 timeout 0 wit inspect 96      60    - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect 240   3700 2700 false(unreach-call) 1 wit inspect 17    750 true -32 wit inspect 3.2   210   unknown 0 wit inspect 1.9  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 86   1900 900 true -32 wit inspect 5.0  280 out of memory 0 wit inspect 64     7000   unknown 0 wit inspect 2.7  220 false(unreach-call) 1 wit inspect .60   20    - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i unknown 0 wit inspect 86   220 880 error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .046 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 11   280 92 true -32 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 5.2   250   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i unknown 0 wit inspect 300   7300 3500 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0020 .29 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i false(unreach-call) 1 wit inspect 400   7200 4800 timeout 0 wit inspect 92    1900 true -32 wit inspect 5.3   210   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .87   18    - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect 18   290 150 true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call1.i false(unreach-call) 1 wit inspect 240   3700 2600 timeout 0 wit inspect 92    1800 true -32 wit inspect 4.8   210   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .81   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 11   280 82 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 5.2   250   unknown 0 wit inspect 1.9  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect 15   280 120 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.9   250   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call4.i false(unreach-call) 1 wit inspect 220   2100 3100 timeout 0 wit inspect 91    1700 true -32 wit inspect 4.3   210   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .81   18    - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 15   290 110 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.9   350   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .57   19    - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 15   290 120 false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 8.3   350   unknown 0 wit inspect 2.2  210 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 18   280 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 8.6   370  
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect 3.1 210 23 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 timeout 0 wit inspect 960     2900  
loop-acceleration/array_true-unreach-call3_true-termination.i true 2 wit inspect 15   220 94 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  280 true 2 wit inspect 8.4   330  
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 15   220 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 out of memory 0 wit inspect 120     7000  
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 12   280 88 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 7.6   300  
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 37   740 310 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    480 timeout 0 wit inspect 960     710  
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect 25   480 200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.2  310 true 2 wit inspect 80     690  
loop-acceleration/functions_true-unreach-call1_true-termination.i true 1 wit inspect 79   1200 760 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6800 timeout 0 wit inspect 960     710  
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 12   270 98 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  270 true 2 wit inspect 5.1   260  
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect 11   270 97 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  270 true 2 wit inspect 26     500  
loop-acceleration/overflow_true-unreach-call1.i true 1 wit inspect 79   1200 730 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    7000 timeout 0 wit inspect 960     620  
loop-acceleration/phases_true-unreach-call1.i true 1 wit inspect 240   7200 2600 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 500    7000 timeout 0 wit inspect 960     640  
loop-acceleration/phases_true-unreach-call2_false-termination.i true 2 wit inspect 12   300 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  340 true 2 wit inspect 6.2   260  
loop-acceleration/simple_true-unreach-call1.i true 1 wit inspect 79   1200 800 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 490    7000 timeout 0 wit inspect 960     580  
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 12   280 91 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 5.1   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i true 1 wit inspect 80   1200 750 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    7000 timeout 0 wit inspect 960     560  
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect 12   270 99 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 6.8   260  
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 16   300 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  290 true 2 wit inspect 49     490  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 11   280 86 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 7.6   290  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 1 wit inspect 560   5400 8500 false(unreach-call) 1 wit inspect 3.6  260 true -32 wit inspect 4.2   210   unknown 0 wit inspect 2.0  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i true 1 wit inspect 15   220 89 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 timeout 0 wit inspect 960     660  
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i true 1 wit inspect 16   220 96 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    730 timeout 0 wit inspect 960     730  
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i true 1 wit inspect 15   220 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6200 timeout 0 wit inspect 960     740  
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i true 2 wit inspect 17   220 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 true 2 wit inspect 65     470  
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true 2 wit inspect 12   280 99 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  270 true 2 wit inspect 6.9   270  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i true 2 wit inspect 12   280 96 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  270 true 2 wit inspect 7.7   270  
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16   280 120 true -32 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .63   19    - wit inspect - wit inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i true 2 wit inspect 83   860 790 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 true 2 wit inspect 11     450  
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect 80   1300 790 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 710    7000 true 2 wit inspect 8.9   380  
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 2 wit inspect 95   850 810 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 true 2 wit inspect 14     510  
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 0 wit inspect 900   9400 8400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .018 4.9
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4600 7800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .020 4.9
loop-invgen/down_true-unreach-call_true-termination.i true 1 wit inspect 89   1400 750 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 timeout 0 wit inspect 960     1300  
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i true 1 wit inspect 13   230 75 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 540    7000 timeout 0 wit inspect 960     4600  
loop-invgen/half_2_true-unreach-call_true-termination.i true 1 wit inspect 91   1100 650 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 880    7000 timeout 0 wit inspect 960     4700  
loop-invgen/heapsort_true-unreach-call_true-termination.i true 2 wit inspect 140   890 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 true 2 wit inspect 67     570  
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 13   290 96 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  280 true 2 wit inspect 5.7   340  
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 20   290 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2  310 false(unreach-call) -16 wit inspect 5.5   270  
loop-invgen/nest-if3_true-unreach-call_true-termination.i true 2 wit inspect 84   800 790 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3300 true 2 wit inspect 11     390  
loop-invgen/nested6_true-unreach-call_true-termination.i error 0 wit inspect 900   8000 5900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .020 4.9
loop-invgen/nested9_true-unreach-call_true-termination.i true 2 wit inspect 90   860 890 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 true 2 wit inspect 10     450  
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i true 1 wit inspect 760   3900 6500 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 650    7000 false(unreach-call) -16 wit inspect 5.5   260  
loop-invgen/seq_true-unreach-call_true-termination.i true 1 wit inspect 98   1000 870 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 timeout 0 wit inspect 960     2200  
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i true 1 wit inspect 93   1300 800 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 timeout 0 wit inspect 960     4600  
loop-invgen/up_true-unreach-call_true-termination.i true 1 wit inspect 88   1400 740 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 timeout 0 wit inspect 960     1300  
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 wit inspect 7.9 220 58 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 6.7   270  
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i true 2 wit inspect 120   720 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    650 true 2 wit inspect 9.3   440  
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect 13   280 97 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  270 true 2 wit inspect 7.9   310  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 81   1400 700 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 5.9   340  
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect 8.8 230 61 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  270 true 2 wit inspect 6.8   260  
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 9.3 210 70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  270 true 2 wit inspect 5.9   270  
loop-lit/ddlm2013_true-unreach-call.i unknown 0 wit inspect 560   2200 5600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .021 4.9
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect 19   440 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  290 true 2 wit inspect 28     690  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i true 2 wit inspect 86   1100 770 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 true 2 wit inspect 9.3   360  
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect 30   610 190 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7  300 true 2 wit inspect 37     860  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i true 2 wit inspect 160   800 1900 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1300 true 2 wit inspect 7.5   320  
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 wit inspect 82   1300 720 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 8.6   330  
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 1 wit inspect 82   1300 650 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 timeout 0 wit inspect 960     2900  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 82   1300 740 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    3600 true 2 wit inspect 9.0   330  
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i true 1 wit inspect 100   620 1200 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 780    7000 timeout 0 wit inspect 960     1400  
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 16   280 120 timeout 0 wit inspect 92    2200 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect 11   290 85 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  290