Tool CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:29:20 CET 2017-12-01 08:07:14 CET 2017-12-01 08:15:38 CET 2017-12-01 08:19:10 CET 2017-12-01 04:11:27 CET 2017-12-01 07:35:08 CET
Run set cpa-seq.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Loops
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
loops/array_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.4 270 32 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 5.7   260   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/bubble_sort_false-unreach-call.i false(unreach-call) 1 wit inspect 4.9 310 43 true -32 wit inspect 4.8  280 error (7) 0 wit inspect 10     210   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.5 250 21 false(unreach-call) 1 wit inspect 3.5  250 false(unreach-call) 1 wit inspect 6.8   320   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/eureka_01_false-unreach-call_true-termination.i timeout 0 wit inspect 900   4400 11000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .98 49 error (invalid witness file) 0 wit inspect .0045 .26 - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.6 270 33 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.5   260   unknown 0 wit inspect 3.7  210 true -32 wit inspect .73   19    - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 51   2300 430 true -32 wit inspect 3.5  270 false(unreach-call) 1 wit inspect 16     520   unknown 0 wit inspect 3.2  210 true -32 wit inspect .63   19    - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 210   2100 2900 true -32 wit inspect 3.5  270 false(unreach-call) 1 wit inspect 11     430   unknown 0 wit inspect 3.0  210 true -32 wit inspect .61   19    - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i false(unreach-call) 1 wit inspect 13   540 99 false(unreach-call) 1 wit inspect 4.2  280 false(unreach-call) 1 wit inspect 14     520   unknown 0 wit inspect 3.7  210 error (2) 0 wit inspect .59   19    - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 1 wit inspect 6.8 530 65 false(unreach-call) 1 wit inspect 8.7  520 timeout 0 wit inspect 97     4500   unknown 0 wit inspect 3.3  210 error (2) 0 wit inspect .60   19    - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.7 280 31 false(unreach-call) 1 wit inspect 3.4  270 false(unreach-call) 1 wit inspect 7.4   330   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i timeout 0 wit inspect 900   5000 9200 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0013 .32 - wit inspect - wit inspect
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 2.6 260 22 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.8 260 23 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 6.9   320   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
loops/s3_false-unreach-call.i false(unreach-call) 1 wit inspect 44   2500 430 true -32 wit inspect 6.1  280 false(unreach-call) 1 wit inspect 71     660   unknown 0 wit inspect 6.0  270 error (2) 0 wit inspect .81   20    - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.3 270 28 false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 27     430   unknown 0 wit inspect 3.1  210 true -32 wit inspect .61   19    - wit inspect - wit inspect
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.1 280 42 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 10     280   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.7 280 36 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 6.8   260   unknown 0 wit inspect 3.3  180 true -32 wit inspect .63   19    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.0 280 45 false(unreach-call) 1 wit inspect 3.8  270 false(unreach-call) 1 wit inspect 8.1   600   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 3.6 270 29 false(unreach-call) 1 wit inspect 4.8  290 out of memory 0 wit inspect 84     7000   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.0 260 25 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 6.9   320   unknown 0 wit inspect 3.1  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect 3.8 280 33 false(unreach-call) 1 wit inspect 3.5  270 false(unreach-call) 1 wit inspect 5.9   270   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.5 250 26 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.0   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.6 260 21 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.0   260   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.3 270 28 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 6.0   260   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.6 250 20 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 7.7   270   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.6 280 24 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 6.1   250   unknown 0 wit inspect 2.7  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.2 270 32 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 3.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.7 280 22 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 9.1   320   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .78   18    - wit inspect - wit inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.2 280 37 false(unreach-call) 1 wit inspect 4.1  270 false(unreach-call) 1 wit inspect 20     510   unknown 0 wit inspect 3.0  210 error (2) 0 wit inspect .59   19    - wit inspect - wit inspect
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect 52   510 620 false(unreach-call) 1 wit inspect 4.4  300 timeout 0 wit inspect 97     910   unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .67   20    - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.6 260 22 timeout 0 wit inspect 96    2700 false(unreach-call) 1 wit inspect 5.3   230   timeout 0 wit inspect 96    2700 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 3.5 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  270 true 2 wit inspect 8.0   280  
loops/bubble_sort_true-unreach-call_true-termination.i true 2 wit inspect 93   470 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  280 true 2 wit inspect 4.9   230  
loops/count_up_down_true-unreach-call_true-termination.i timeout 0 wit inspect 900   7000 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.9
loops/eureka_01_true-unreach-call.i true 1 wit inspect 3.9 260 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 680     7000  
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect 2.9 250 24 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 100     1000  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 93   2200 910 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 6.0   260  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 93   2300 1000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  260 true 2 wit inspect 4.9   260  
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4600 6500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .019 4.9
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect 35   810 310 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27    560 true 2 wit inspect 540     660  
loops/linear_sea.ch_true-unreach-call.i timeout 0 wit inspect 910   9100 8700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 5.0
loops/lu.cmp_true-unreach-call.i true 1 wit inspect 3.3 260 30 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6500 timeout 0 wit inspect 960     4300  
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 3.9 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  270 true 2 wit inspect 9.6   370  
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect 2.5 250 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 790    7000 true 2 wit inspect 9.3   340  
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 5.2 280 54 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.5  260 true 2 wit inspect 7.6   350  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 4.1 280 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  290 true 2 wit inspect 8.6   340  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 3.5 260 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.0  360 false(unreach-call) -16 wit inspect 13     450  
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 260   3200 3000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 9.4   390  
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect 180   2300 2100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 true 2 wit inspect 5.4   250  
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 2.3 250 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  280 true 2 wit inspect 15     540  
loops/sum_array_true-unreach-call.i timeout 0 wit inspect 900   4500 6400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 3.4 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 7.1   250  
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect 3.3 260 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 true 2 wit inspect 6.5   260  
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 16   590 160 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 28    1100 true 2 wit inspect 6.0   270  
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 3.1 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 5.2   250  
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect 3.4 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  290 true 2 wit inspect 5.9   260  
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect 3.3 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 true 2 wit inspect 5.5   260  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect 3.5 280 31 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 8.2   300  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 150   1300 1700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.0  370 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 4.0 270 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  270 true 2 wit inspect 5.4   260  
loops/vogal_true-unreach-call.i true 2 wit inspect 250   1900 2800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 100    1300 false(unreach-call) -16 wit inspect 27     620  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 2.3 240 20 - wit inspect - wit inspect - wit inspect - wit inspect out of java memory 0 wit inspect 530    5200 true 2 wit inspect 4.9   260  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 2.4 240 22 - wit inspect - wit inspect - wit inspect - wit inspect out of java memory 0 wit inspect 610    5200 true 2 wit inspect 6.0   260  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect 2.4 250 21 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5200 true 2 wit inspect 5.9   250  
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 140   2100 1700 timeout 0 wit inspect 97    1100 timeout 0 wit inspect 96     5300   unknown 0 wit inspect 12    390 false(unreach-call) 1 wit inspect 1.1    39    - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call2_true-termination.i timeout 0 wit inspect 900   8700 12000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .86 48 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 0 wit inspect 900   7500 10000 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0011 .33 - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect 74   1200 840 false(unreach-call) 1 wit inspect 19    1000 timeout 0 wit inspect 96     6100   unknown 0 wit inspect 21    670 false(unreach-call) 1 wit inspect 1.9    54    - wit inspect - wit inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 45   1100 580 false(unreach-call) 1 wit inspect 5.6  280 out of memory 0 wit inspect 80     7000   unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .72   20    - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   8100 10000 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect - wit inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 2.5 260 20 false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 5.7   250   unknown 0 wit inspect 3.6  190 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900   5200 10000 error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i timeout 0 wit inspect 900   5700 9500 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect 2.5 250 25 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 5.0   250   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call1.i timeout 0 wit inspect 910   7300 10000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .96 50 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 2.5 250 21 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.0   250   unknown 0 wit inspect 2.9  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 2.6 250 22 false(unreach-call) 1 wit inspect 3.5  280 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call4.i timeout 0 wit inspect 900   7000 9800 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 2.7 250 24 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 8.5   330   unknown 0 wit inspect 3.0  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 2.8 260 25 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 8.4   340   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 92   460 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.8  570 error (7) 0 wit inspect 12     320  
loop-acceleration/array_true-unreach-call2_true-termination.i timeout 0 wit inspect 900   8600 11000 - 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-acceleration/array_true-unreach-call3_true-termination.i true 2 wit inspect 10   660 89 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    750 error (7) 0 wit inspect 10     320  
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 11   470 86 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6300 error (7) 0 wit inspect 8.7   220  
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 5.2 280 46 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 false(unreach-call) -16 wit inspect 5.2   260  
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 160   1900 2100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    480 timeout 0 wit inspect 960     680  
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect 5.8 310 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  310 true 2 wit inspect 65     690  
loop-acceleration/functions_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   8000 9400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.8
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 2.9 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 760    6200 true 2 wit inspect 6.5   250  
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect 350   3600 5200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  270 true 2 wit inspect 26     550  
loop-acceleration/overflow_true-unreach-call1.i timeout 0 wit inspect 900   6800 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .021 4.9
loop-acceleration/phases_true-unreach-call1.i timeout 0 wit inspect 900   6400 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 4.9
loop-acceleration/phases_true-unreach-call2_false-termination.i true 2 wit inspect 3.1 260 26 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    410 true 2 wit inspect 6.6   260  
loop-acceleration/simple_true-unreach-call1.i timeout 0 wit inspect 910   7300 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .019 4.9
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 3.1 260 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 6.0   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i timeout 0 wit inspect 900   6600 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 4.8
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect 150   1300 1800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 6.3   260  
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 2.4 240 21 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  350 true 2 wit inspect 15     520  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 2.4 250 21 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 14     490  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 1 wit inspect 2.9 260 26 false(unreach-call) 1 wit inspect 3.6  270 false(unreach-call) 1 wit inspect 5.9   240   unknown 0 wit inspect 2.8  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   3700 9400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.8
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i timeout 0 wit inspect 900   3400 9900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 5.0
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i timeout 0 wit inspect 900   5800 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i true 2 wit inspect 7.7 490 88 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 true 2 wit inspect 62     460  
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true 2 wit inspect 350   2700 4200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 false(unreach-call) -16 wit inspect 5.9   260  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i true 2 wit inspect 150   2300 1700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  270 true 2 wit inspect 5.5   260  
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.4 270 29 false(unreach-call) 1 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 6.9   260   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout 0 wit inspect 900   3200 9400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.9
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i timeout 0 wit inspect 910   10000 9300 - 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-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 2 wit inspect 8.4 340 95 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 true 2 wit inspect 12     490  
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i true 2 wit inspect 4.7 280 38 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 true 2 wit inspect 14     510  
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i true 2 wit inspect 210   2500 2500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  290 true 2 wit inspect 10     430  
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 wit inspect 910   12000 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .020 4.9
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 0 wit inspect 900   11000 8800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .019 4.9
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   7700 8800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.9
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5100 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 4.9
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 200   1800 2700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  280 false(unreach-call) -16 wit inspect 10     330  
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 3.8 270 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  270 true 2 wit inspect 9.6   340  
loop-invgen/nest-if3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5000 11000 - 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-invgen/nested6_true-unreach-call_true-termination.i timeout 0 wit inspect 910   8900 9400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .024 5.0
loop-invgen/nested9_true-unreach-call_true-termination.i timeout 0 wit inspect 900   6100 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.8
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i timeout 0 wit inspect 900   9700 8700 - 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/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900   11000 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.9
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i timeout 0 wit inspect 900   10000 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .018 5.0
loop-invgen/up_true-unreach-call_true-termination.i out of memory 0 wit inspect 810   15000 7200 - 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-lit/afnp2014_true-unreach-call_true-termination.c.i true 1 wit inspect 8.2 460 70 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 error (7) 0 wit inspect 11     300  
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   2000 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .023 4.9
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect 2.5 250 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  280 true 2 wit inspect 10     440  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 910   7100 9100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .020 4.8
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect 4.1 270 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.0  410 timeout 0 wit inspect 960     1900  
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 3.4 270 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  270 true 2 wit inspect 6.6   260  
loop-lit/ddlm2013_true-unreach-call.i timeout 0 wit inspect 900   7000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.9
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect 3.3 260 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 160    3200 false(unreach-call) -16 wit inspect 5.6   250  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   4500 9500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect 3.7 260 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 55    1000 false(unreach-call) -16 wit inspect 6.0   260  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i true 1 wit inspect 570   2600 7300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2400 timeout 0 wit inspect 960     2200  
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 910   7900 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 4.9
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect 3.4 270 29 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5800 true 2 wit inspect 9.8   290  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   6900 9900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .021 4.9
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   4300 8400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .019 4.9
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 2.6 250 22 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 5.6   250   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .83   18    - wit inspect - wit inspect
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect 350   3100 4200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 false(unreach-call) -16 wit inspect 5.3   260  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect 350   3600 3800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  270 false(unreach-call) -16 wit inspect 7.3   260  
loop-new/count_by_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   6700 8400 - wit