Tool Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 19:46:39 CET 2017-12-01 22:34:51 CET 2017-12-01 23:03:48 CET 2017-12-01 23:06:19 CET 2017-12-01 23:09:14 CET 2017-12-01 22:04:37 CET 2017-12-01 22:38:34 CET
Run set map2check.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Loops
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
loops/array_false-unreach-call_true-termination.i true -32 wit inspect .43  12 4.7  unknown 0 wit inspect 4.7  270 false(unreach-call) 1 wit inspect 5.4   270   unknown 0 wit inspect .98 52 error (1) 0 wit inspect .091  9.1  - wit inspect - wit inspect
loops/bubble_sort_false-unreach-call.i unknown 0 wit inspect .39  12 4.2  error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .35  11 3.7  timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 4.9   250   unknown 0 wit inspect 3.5  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) 1 wit inspect 2.6   13 33    true -32 wit inspect 4.2  260 true -32 wit inspect 5.3   240   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i true -32 wit inspect .52  12 5.3  unknown 0 wit inspect 5.3  270 false(unreach-call) 1 wit inspect 8.1   290   unknown 0 wit inspect .92 51 error (1) 0 wit inspect .079  9.1  - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i true -32 wit inspect .37  11 3.9  unknown 0 wit inspect 52    580 timeout 0 wit inspect 97     870   unknown 0 wit inspect .92 52 error (1) 0 wit inspect .066  9.0  - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i unknown 0 wit inspect .38  12 4.0  error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i true -32 wit inspect .37  11 4.8  unknown 0 wit inspect 10    340 timeout 0 wit inspect 96     710   unknown 0 wit inspect .98 51 error (1) 0 wit inspect .066  9.0  - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 1 wit inspect .39  11 4.8  true -32 wit inspect 3.0  270 timeout 0 wit inspect 97     4500   unknown 0 wit inspect 3.6  190 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i unknown 0 wit inspect 900     410 9000    error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i unknown 0 wit inspect 900     1500 10000    error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
loops/nec11_false-unreach-call_false-termination.i unknown 0 wit inspect .31  11 2.9  error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
loops/nec20_false-unreach-call_true-termination.i unknown 0 wit inspect .30  11 4.0  error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
loops/s3_false-unreach-call.i unknown 0 wit inspect .096 13 .70 error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i true -32 wit inspect 1.2   12 15    unknown 0 wit inspect 51    1100 false(unreach-call) 1 wit inspect 19     370   unknown 0 wit inspect 1.0  50 error (1) 0 wit inspect .073  9.0  - wit inspect - wit inspect
loops/sum01_bug02_false-unreach-call_true-termination.i true -32 wit inspect .70  12 8.8  unknown 0 wit inspect 5.9  280 false(unreach-call) 1 wit inspect 12     500   unknown 0 wit inspect 1.2  51 error (1) 0 wit inspect .064  9.0  - wit inspect - wit inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .60  12 6.6  timeout 0 wit inspect 92    2100 true -32 wit inspect 7.1   270   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i true -32 wit inspect .82  12 11    unknown 0 wit inspect 6.9  280 false(unreach-call) 1 wit inspect 11     500   unknown 0 wit inspect .95 49 error (1) 0 wit inspect .076  9.0  - wit inspect - wit inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .33  11 3.8  true -32 wit inspect 2.4  260 true -32 wit inspect 6.1   260   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .33  11 3.6  true -32 wit inspect 3.9  250 true -32 wit inspect 6.3   260   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
loops/sum_array_false-unreach-call.i true -32 wit inspect .38  15 4.3  unknown 0 wit inspect 8.3  320 false(unreach-call) 1 wit inspect 6.9   260   unknown 0 wit inspect 1.0  50 error (1) 0 wit inspect .067  9.0  - wit inspect - wit inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .34  11 4.0  false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.3   250   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .43  12 6.1  false(unreach-call) 1 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 3.4   260   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .56  13 6.7  false(unreach-call) 1 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 5.7   260   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i unknown 0 wit inspect .30  11 3.5  error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .40  12 5.1  false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 5.4   250   unknown 0 wit inspect 3.5  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/trex03_false-unreach-call_true-termination.i unknown 0 wit inspect .30  11 3.6  error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .95 50 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .34  11 3.9  true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 8.8   300   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i unknown 0 wit inspect .31  11 3.8  error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0011 .36 - wit inspect - wit inspect
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect 1.8   12 22    true -32 wit inspect 6.6  410 true -32 wit inspect 3.5   220   unknown 0 wit inspect 4.0  210 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .32  11 4.0  true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 4.9   230   unknown 0 wit inspect 2.9  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect .45  12 4.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  280 true 2 wit inspect 7.5   280  
loops/bubble_sort_true-unreach-call_true-termination.i true 2 wit inspect .36  11 3.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 4.9   240  
loops/count_up_down_true-unreach-call_true-termination.i unknown 0 wit inspect 900     1200 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.8
loops/eureka_01_true-unreach-call.i true 1 wit inspect .37  11 4.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5400 timeout 0 wit inspect 960     1400  
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect .34  11 4.3  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6500 true 2 wit inspect 53     830  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i unknown 0 wit inspect 890     12 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .018 4.9
loops/for_infinite_loop_2_true-unreach-call_false-termination.i unknown 0 wit inspect 900     11 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .025 4.8
loops/insertion_sort_true-unreach-call_true-termination.i true 1 wit inspect .38  12 4.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 timeout 0 wit inspect 960     3100  
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .39  11 5.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 20    520 true 2 wit inspect 190     780  
loops/linear_sea.ch_true-unreach-call.i true 1 wit inspect .38  11 5.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 710    7000 timeout 0 wit inspect 960     720  
loops/lu.cmp_true-unreach-call.i true 1 wit inspect .44  11 5.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5300 timeout 0 wit inspect 960     4000  
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect .47  12 5.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 11     380  
loops/n.c11_true-unreach-call_false-termination.i unknown 0 wit inspect .27  11 3.2  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .026 4.8
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .37  12 3.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  270 true 2 wit inspect 6.7   340  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .35  12 4.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  270 true 2 wit inspect 7.2   350  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 18     13 210    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  280 true 2 wit inspect 12     380  
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 74     64 900    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 570    7000 true 2 wit inspect 12     390  
loops/sum03_true-unreach-call_false-termination.i unknown 0 wit inspect 890     11 14000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .026 4.8
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect .30  11 4.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  270 true 2 wit inspect 12     430  
loops/sum_array_true-unreach-call.i unknown 0 wit inspect .036 13 .39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .018 4.9
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect .61  12 6.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  270 true 2 wit inspect 7.0   260  
loops/terminator_03_true-unreach-call_true-termination.i unknown 0 wit inspect 900     66 14000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.8
loops/trex01_true-unreach-call_true-termination.i unknown 0 wit inspect .28  11 3.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .025 4.8
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect .34  12 4.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 4.1   260  
loops/trex03_true-unreach-call_true-termination.i unknown 0 wit inspect .31  11 3.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.9
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect .39  12 4.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 6.0   270  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect .31  11 3.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 7.9   290  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 700     79 8600    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  360 true 2 wit inspect 6.9   270  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 3.0   12 39    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 6.1   270  
loops/vogal_true-unreach-call.i true 2 wit inspect 13     13 150    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 46    1100 true 2 wit inspect 290     1100  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i unknown 0 wit inspect 890     11 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.9
loops/while_infinite_loop_2_true-unreach-call_false-termination.i unknown 0 wit inspect 890     11 15000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .025 4.8
loops/while_infinite_loop_3_true-unreach-call_false-termination.i unknown 0 wit inspect 900     11 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.9
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .34  11 3.9  true -32 wit inspect 47    320 true -32 wit inspect 10     410   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .36  11 5.4  true -32 wit inspect 17    430 true -32 wit inspect 9.2   430   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call3_true-termination.i unknown 0 wit inspect 890     53 11000    error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect .34  11 4.7  true -32 wit inspect 9.6  400 true -32 wit inspect 11     450   unknown 0 wit inspect 3.1  180 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 .36  11 4.2  true -32 wit inspect 2.5  270 true -32 wit inspect 6.0   260   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i unknown 0 wit inspect 890     11 13000    error (invalid witness file) 0 wit inspect .46 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect 1.2  50 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 .34  11 3.9  true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 6.6   250   unknown 0 wit inspect 3.0  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i unknown 0 wit inspect 890     11 13000    error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i unknown 0 wit inspect 890     11 14000    error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .88 47 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect .40  11 4.7  true -32 wit inspect 4.1  250 false(unreach-call) 1 wit inspect 4.9   250   unknown 0 wit inspect 3.1  180 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call1.i unknown 0 wit inspect 900     11 12000    error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .30  11 3.5  true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 5.1   250   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .79   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .30  11 4.0  timeout 0 wit inspect 92    1900 false(unreach-call) 1 wit inspect 4.6   250   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call4.i unknown 0 wit inspect 890     11 11000    error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .33  11 4.0  true -32 wit inspect 3.7  250 false(unreach-call) 1 wit inspect 7.8   310   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .32  11 3.9  true -32 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 8.4   310   unknown 0 wit inspect 3.6  180 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect .37  11 4.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.6  270 true 2 wit inspect 7.1   280  
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect .39  11 4.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 timeout 0 wit inspect 960     3400  
loop-acceleration/array_true-unreach-call3_true-termination.i unknown 0 wit inspect 890     53 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 45 error (2) 0 wit inspect .025 4.9
loop-acceleration/array_true-unreach-call4_true-termination.i unknown 0 wit inspect 890     71 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 44 error (2) 0 wit inspect .025 4.9
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect .33  11 4.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 8.9   260  
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect .38  11 4.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    480 timeout 0 wit inspect 960     550  
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect .44  11 5.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3  310 true 2 wit inspect 64     680  
loop-acceleration/functions_true-unreach-call1_true-termination.i unknown 0 wit inspect 890     11 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .026 4.8
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 67     64 860    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 820    5800 true 2 wit inspect 5.8   260  
loop-acceleration/nested_true-unreach-call1.i unknown 0 wit inspect 890     11 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .020 4.9
loop-acceleration/overflow_true-unreach-call1.i unknown 0 wit inspect 890     11 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .024 4.8
loop-acceleration/phases_true-unreach-call1.i unknown 0 wit inspect 890     11 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .021 4.8
loop-acceleration/phases_true-unreach-call2_false-termination.i unknown 0 wit inspect 890     12 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .026 4.8
loop-acceleration/simple_true-unreach-call1.i unknown 0 wit inspect 890     11 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 45 error (2) 0 wit inspect .023 4.9
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect .30  11 3.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 7.0   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i unknown 0 wit inspect 900     1100 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .025 4.8
loop-acceleration/simple_true-unreach-call4.i unknown 0 wit inspect 890     11 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .025 4.9
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect .33  11 3.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  280 true 2 wit inspect 63     440  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect .30  11 3.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  270 true 2 wit inspect 7.1   270  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 1 wit inspect .38  19 4.6  true -32 wit inspect 4.1  260 false(unreach-call) 1 wit inspect 3.2   250   unknown 0 wit inspect 3.1  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i true 1 wit inspect .47  11 6.3  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 timeout 0 wit inspect 960     710  
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i unknown 0 wit inspect 900     75 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i true 1 wit inspect 1.6   11 21    - 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 1.2   160 14    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 true 2 wit inspect 80     460  
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i unknown 0 wit inspect 890     11 14000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .021 4.9
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i unknown 0 wit inspect 890     11 14000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .025 4.8
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .58  12 7.8  false(unreach-call) 1 wit inspect 3.9  270 true -32 wit inspect 5.3   260   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i unknown 0 wit inspect 900     660 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .021 4.9
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i unknown 0 wit inspect 900     910 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .025 4.9
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i unknown 0 wit inspect 900     170 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.8
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i unknown 0 wit inspect 890     130 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .022 4.9
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i unknown 0 wit inspect 900     320 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 4.9
loop-invgen/down_true-unreach-call_true-termination.i unknown 0 wit inspect 890     400 8200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .021 4.8
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i unknown 0 wit inspect 900     190 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .025 4.9
loop-invgen/half_2_true-unreach-call_true-termination.i unknown 0 wit inspect 900     840 8200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .024 4.8
loop-invgen/heapsort_true-unreach-call_true-termination.i unknown 0 wit inspect 900     900 8800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .023 4.8
loop-invgen/id_build_true-unreach-call_true-termination.i unknown 0 wit inspect 900     680 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.8
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect .89  12 11    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  290 true 2 wit inspect 9.2   350  
loop-invgen/nest-if3_true-unreach-call_true-termination.i unknown 0 wit inspect 890     460 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .024 4.8
loop-invgen/nested6_true-unreach-call_true-termination.i unknown 0 wit inspect 900     700 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 4.9
loop-invgen/nested9_true-unreach-call_true-termination.i unknown 0 wit inspect 890     67 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .033 4.9
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i unknown 0 wit inspect 890     40 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .047 4.9
loop-invgen/seq_true-unreach-call_true-termination.i unknown 0 wit inspect 900     200 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .022 4.8
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i unknown 0 wit inspect 890     98 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .026 5.0
loop-invgen/up_true-unreach-call_true-termination.i unknown 0 wit inspect 900     420 8900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .024 4.8
loop-lit/afnp2014_true-unreach-call_true-termination.c.i unknown 0 wit inspect 890     29 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .025 5.0
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i unknown 0 wit inspect 900     580 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .027 4.8
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .35  11 3.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 true 2 wit inspect 10     310  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i unknown 0 wit inspect 900     330 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .025 4.9
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect .33  11 4.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 8.4   260  
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 150     12 1900    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 true 2 wit inspect 6.3   270  
loop-lit/ddlm2013_true-unreach-call.i unknown 0 wit inspect 890     30 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.9
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect .34  11 3.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 40    580 true 2 wit inspect 91     1200  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i unknown 0 wit inspect 900     1000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .024 4.9
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect .34  11 3.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 46    1000 true 2 wit inspect 120     1600  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i unknown 0 wit inspect 900     40 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 5.0
loop-lit/hhk2008_true-unreach-call_true-termination.c.i unknown 0 wit inspect 900     330 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .025 4.8
loop-lit/jm2006_true-unreach-call_true-termination.c.i unknown 0 wit inspect 900     680 9600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.8
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i unknown 0 wit inspect 900     650 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .023 4.9
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i true 1 wit inspect .43  12 4.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 760    7000 timeout 0 wit inspect 960     710  
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .39  12 4.4  false(unreach-call) 1 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 4.7   250   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect 17     11 220    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.4  260 true 2 wit inspect 6.9   260  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect 92     11 1400    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 7.5   270  
loop-new/count_by_2_true-unreach-call_true-termination.i true 1 wit