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