Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 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]
Date of execution 2017-11-30 16:01:31 CET 2017-12-01 08:31:47 CET 2017-12-01 08:56:50 CET 2017-12-01 08:59:39 CET 2017-12-01 09:01:39 CET 2017-12-01 08:10:33 CET 2017-12-01 08:38:18 CET
Run set depthk.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Loops
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.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/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.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/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/depthk.2017-11-30_1601.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) 0 wit inspect 1.1  75 19   true -32 wit inspect 3.2  260 true -32 wit inspect 4.6   230   unknown 0 wit inspect 3.0  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
loops/bubble_sort_false-unreach-call.i false(unreach-call) 0 wit inspect 3.0  240 36   true -32 wit inspect 4.9  270 error (7) 0 wit inspect 8.1   220   unknown 0 wit inspect 3.9  220 error (2) 0 wit inspect .85   19    - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .54 75 5.6 timeout 0 wit inspect 92    2000 true -32 wit inspect 5.4   210   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 2.9  190 34   timeout 0 wit inspect 92    1900 true -32 wit inspect 5.0   240   unknown 0 wit inspect 3.1  210 error (2) 0 wit inspect .59   19    - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.2  76 14   timeout 0 wit inspect 92    2300 true -32 wit inspect 4.8   230   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.6  130 54   timeout 0 wit inspect 92    2000 true -32 wit inspect 5.3   240   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 1.9  130 23   timeout 0 wit inspect 92    2000 true -32 wit inspect 4.8   230   unknown 0 wit inspect 3.1  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i false(unreach-call) 0 wit inspect 16    76 230   true -32 wit inspect 3.9  260 true -32 wit inspect 5.0   220   unknown 0 wit inspect 3.3  220 error (2) 0 wit inspect .59   19    - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 0 wit inspect 7.1  350 79   true -32 wit inspect 3.1  270 true -32 wit inspect 17     1500   unknown 0 wit inspect 3.5  220 error (2) 0 wit inspect .62   19    - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 480    180 6700   timeout 0 wit inspect 92    1900 true -32 wit inspect 4.8   230   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i unknown 0 wit inspect 900    1400 8300   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .88 51 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 .54 75 7.0 true -32 wit inspect 3.2  250 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 1.2  76 17   timeout 0 wit inspect 92    2100 true -32 wit inspect 4.8   230   unknown 0 wit inspect 3.0  180 error (2) 0 wit inspect .62   18    - wit inspect - wit inspect
loops/s3_false-unreach-call.i unknown 0 wit inspect 890    1600 11000   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .84 46 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 4.0  190 53   true -32 wit inspect 4.4  260 true -32 wit inspect 5.5   250   unknown 0 wit inspect 3.2  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 3.8  76 54   timeout 0 wit inspect 92    2100 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.8  75 34   timeout 0 wit inspect 92    2000 true -32 wit inspect 4.7   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.0  75 86   timeout 0 wit inspect 92    2000 true -32 wit inspect 5.1   230   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.8  75 76   true -32 wit inspect 3.6  260 true -32 wit inspect 5.0   240   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.7  75 58   true -32 wit inspect 3.2  260 true -32 wit inspect 3.1   210   unknown 0 wit inspect 3.2  210 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 1.4  160 17   timeout 0 wit inspect 91    2000 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .53 75 6.3 true -32 wit inspect 3.0  260 true -32 wit inspect 4.6   230   unknown 0 wit inspect 2.8  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 .40 75 4.4 true -32 wit inspect 3.0  250 true -32 wit inspect 3.1   230   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .55 75 6.5 true -32 wit inspect 3.0  250 true -32 wit inspect 4.5   220   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .62 160 8.7 true -32 wit inspect 2.8  280 true -32 wit inspect 4.8   230   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .41 75 5.0 true -32 wit inspect 2.9  250 true -32 wit inspect 4.3   220   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .40 75 5.1 true -32 wit inspect 3.3  260 true -32 wit inspect 4.6   230   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 1.4  75 19   true -32 wit inspect 3.3  260 true -32 wit inspect 5.1   220   unknown 0 wit inspect 3.0  180 error (2) 0 wit inspect .57   18    - wit inspect - wit inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 2.0  130 25   timeout 0 wit inspect 92    2000 true -32 wit inspect 5.0   240   unknown 0 wit inspect 3.1  220 error (2) 0 wit inspect .59   18    - wit inspect - wit inspect
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect 12    210 140   false(unreach-call) 1 wit inspect 14    610 true -32 wit inspect 3.9   300   unknown 0 wit inspect 5.8  280 true -32 wit inspect .70   19    - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .38 75 4.8 true -32 wit inspect 3.1  260 true -32 wit inspect 4.5   220   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 4.3  280 42   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  280 true 2 wit inspect 7.6   290  
loops/bubble_sort_true-unreach-call_true-termination.i unknown 0 wit inspect 900    450 12000   - 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
loops/count_up_down_true-unreach-call_true-termination.i unknown 0 wit inspect 69    75 900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .042 4.9
loops/eureka_01_true-unreach-call.i unknown 0 wit inspect 890    310 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .020 5.0
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect 6.2  260 61   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    6600 true 2 wit inspect 48     810  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i unknown 0 wit inspect 38    75 470   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .018 5.0
loops/for_infinite_loop_2_true-unreach-call_false-termination.i unknown 0 wit inspect 37    75 560   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .018 4.9
loops/insertion_sort_true-unreach-call_true-termination.i unknown 0 wit inspect 890    190 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .020 4.9
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect 17    460 230   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    520 true 2 wit inspect 140     760  
loops/linear_sea.ch_true-unreach-call.i unknown 0 wit inspect 120    76 1400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8
loops/lu.cmp_true-unreach-call.i true 1 wit inspect 9.2  350 97   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 timeout 0 wit inspect 960     3900  
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 15    370 160   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  270 true 2 wit inspect 10     370  
loops/n.c11_true-unreach-call_false-termination.i unknown 0 wit inspect 58    75 680   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.8
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 4.4  280 39   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 6.4   350  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 4.5  280 46   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  270 true 2 wit inspect 6.7   340  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 4.6  260 53   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  290 true 2 wit inspect 9.1   370  
loops/sum01_true-unreach-call_true-termination.i true 1 wit inspect 300    3600 2800   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 error (7) 0 wit inspect 14     440  
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect 180    2200 2300   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  270 true 2 wit inspect 5.4   250  
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 3.3  250 33   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 9.8   430  
loops/sum_array_true-unreach-call.i unknown 0 wit inspect 890    290 9000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.8
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 4.1  260 48   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  270 true 2 wit inspect 6.1   260  
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect 3.8  270 39   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 5.5   260  
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 160    2300 1900   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 26    1100 true 2 wit inspect 5.2   260  
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 3.7  260 32   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 5.3   250  
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect 4.0  270 36   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  280 true 2 wit inspect 5.8   250  
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect 4.6  280 45   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 5.3   260  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect 4.1  280 41   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 8.3   300  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 160    2300 1800   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    350 true 2 wit inspect 7.0   270  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 5.4  280 50   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  270 true 2 wit inspect 5.6   260  
loops/vogal_true-unreach-call.i true 2 wit inspect 330    2300 3800   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 46    1000 true 2 wit inspect 560     2200  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 3.2  260 33   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 true 2 wit inspect 5.2   260  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 3.0  250 26   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  280 true 2 wit inspect 4.9   260  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect 3.2  260 28   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 5.3   260  
loop-acceleration/array_false-unreach-call1_true-termination.i unknown 0 wit inspect 890    250 9700   error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .90 48 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call2_true-termination.i unknown 0 wit inspect 890    320 9500   error (invalid witness file) 0 wit inspect .54 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 .0012 .26 - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 0 wit inspect 900    8200 11000   timeout 0 wit inspect 91    2100 timeout 0 wit inspect 96     1100   unknown 0 wit inspect .96 51 error (1) 0 wit inspect .073  9.1  - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i unknown 0 wit inspect 54    75 670   error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 32    75 400   true -32 wit inspect 3.2  260 true -32 wit inspect 4.6   230   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i unknown 0 wit inspect 36    75 510   error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .85 48 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .52 75 6.4 true -32 wit inspect 2.9  250 true -32 wit inspect 4.6   210   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900    1400 9200   error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i unknown 0 wit inspect 180    75 2700   error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0013 .31 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect .53 75 7.0 true -32 wit inspect 3.3  260 true -32 wit inspect 3.0   220   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call1.i unknown 0 wit inspect 54    75 790   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .38 75 4.1 true -32 wit inspect 2.9  260 true -32 wit inspect 4.1   220   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .84   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .54 75 7.6 timeout 0 wit inspect 92    1900 true -32 wit inspect 4.2   210   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call4.i unknown 0 wit inspect 53    75 710   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 3.5  75 42   true -32 wit inspect 3.1  260 true -32 wit inspect 4.7   210   unknown 0 wit inspect 2.9  210 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 3.5  75 44   true -32 wit inspect 3.2  250 true -32 wit inspect 4.6   220   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 99    330 1400   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  270 true 2 wit inspect 6.7   290  
loop-acceleration/array_true-unreach-call2_true-termination.i unknown 0 wit inspect 900    230 9400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8
loop-acceleration/array_true-unreach-call3_true-termination.i true 2 wit inspect 15    1200 160   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  270 true 2 wit inspect 8.8   320  
loop-acceleration/array_true-unreach-call4_true-termination.i unknown 0 wit inspect 900    220 9200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 7.1  450 71   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  270 true 2 wit inspect 7.3   270  
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 280    2800 3200   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    480 timeout 0 wit inspect 960     680  
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect 9.3  290 98   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    310 true 2 wit inspect 61     690  
loop-acceleration/functions_true-unreach-call1_true-termination.i unknown 0 wit inspect 36    75 530   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 46 error (2) 0 wit inspect .019 4.8
loop-acceleration/multivar_true-unreach-call1_true-termination.i unknown 0 wit inspect 63    75 910   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.8
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect 360    3500 4100   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  270 true 2 wit inspect 27     500  
loop-acceleration/overflow_true-unreach-call1.i unknown 0 wit inspect 54    75 680   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
loop-acceleration/phases_true-unreach-call1.i unknown 0 wit inspect 130    75 1900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 46 error (2) 0 wit inspect .019 4.8
loop-acceleration/phases_true-unreach-call2_false-termination.i true 2 wit inspect 5.1  270 45   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    400 true 2 wit inspect 6.6   270  
loop-acceleration/simple_true-unreach-call1.i unknown 0 wit inspect 53    75 680   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .037 4.9
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 3.5  270 34   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 5.2   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i unknown 0 wit inspect 57    75 720   - 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-acceleration/simple_true-unreach-call4.i true 2 wit inspect 150    2200 1600   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  280 true 2 wit inspect 4.4   260  
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 5.8  260 65   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  280 true 2 wit inspect 68     440  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 3.3  250 32   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 6.6   270  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 0 wit inspect .54 75 7.8 true -32 wit inspect 3.6  260 true -32 wit inspect 6.1   290   unknown 0 wit inspect 2.9  190 true -32 wit inspect .60   18    - wit inspect - wit inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i unknown 0 wit inspect 890    150 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i unknown 0 wit inspect 900    170 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 5.0
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i unknown 0 wit inspect 890    170 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.8
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i unknown 0 wit inspect 890    100 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.9
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i unknown 0 wit inspect 38    75 470   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .032 4.8
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i true 2 wit inspect 160    2400 1700   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 5.3   260  
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .60 76 7.8 timeout 0 wit inspect 92    2100 true -32 wit inspect 4.6   230   unknown 0 wit inspect 2.9  190 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i unknown 0 wit inspect 900    77 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .020 4.9
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i unknown 0 wit inspect 54    75 760   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .018 5.0
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i unknown 0 wit inspect 890    110 9800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .020 4.9
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i unknown 0 wit inspect 890    100 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 45 error (2) 0 wit inspect .019 4.8
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i unknown 0 wit inspect 890    100 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-invgen/down_true-unreach-call_true-termination.i unknown 0 wit inspect 89    100 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .019 5.0
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i unknown 0 wit inspect 92    130 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.9
loop-invgen/half_2_true-unreach-call_true-termination.i unknown 0 wit inspect 170    110 2500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 4.9
loop-invgen/heapsort_true-unreach-call_true-termination.i unknown 0 wit inspect 890    710 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .79 44 error (2) 0 wit inspect .019 5.0
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 210    1100 2800   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  280 false(unreach-call) -16 wit inspect 5.2   260  
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 4.5  280 40   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  300 true 2 wit inspect 8.5   340  
loop-invgen/nest-if3_true-unreach-call_true-termination.i unknown 0 wit inspect 900    310 7600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9
loop-invgen/nested6_true-unreach-call_true-termination.i unknown 0 wit inspect 900    4000 8100   - 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-invgen/nested9_true-unreach-call_true-termination.i timeout 0 wit inspect 900    6100 8000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 true 2 wit inspect 11     460  
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i unknown 0 wit inspect 230    82 2700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900    9900 9400   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 670    7000 timeout 0 wit inspect 960     1700  
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i unknown 0 wit inspect 900    15000 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .020 4.8
loop-invgen/up_true-unreach-call_true-termination.i unknown 0 wit inspect 71    100 860   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.9
loop-lit/afnp2014_true-unreach-call_true-termination.c.i unknown 0 wit inspect 86    75 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.8
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900    2700 11000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    700 true 2 wit inspect 8.9   420  
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect 3.4  260 30   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  270 true 2 wit inspect 8.5   330  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900    8700 9000   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 8.2   320  
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect 4.6  270 47   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 6.4   260  
loop-lit/css2003_true-unreach-call_true-termination.c.i unknown 0 wit inspect 51    77 730   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .023 4.8
loop-lit/ddlm2013_true-unreach-call.i unknown 0 wit inspect 210    310 2300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .021 4.9
loop-lit/gj2007_true-unreach-call_true-termination.c.i unknown 0 wit inspect 37    76 550   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 40    500 true 2 wit inspect 96     1300  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i unknown 0 wit inspect 200    130 2800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .050 4.9
loop-lit/gr2006_true-unreach-call_true-termination.c.i unknown 0 wit inspect 170    120 1900   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 50    1000 true 2 wit inspect 92     1600  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i unknown 0 wit inspect 900    580 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.8
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900    8000 9000   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 7.6   280  
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect 4.0  270 42   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 true 2 wit inspect 7.8   280  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900    10000 8400   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 true 2 wit inspect 7.4   280  
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i unknown 0 wit inspect 890    100 13000   - 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
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 16    81 200   timeout 0 wit inspect 92    2100 true -32 wit inspect 4.5   230   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect 350    3100 4000   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 6.2   260  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i unknown 0 wit inspect 37    75 440   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.8
loop-new/count_by_2_true-unreach-call_true-termination.i unknown 0 wit inspect 57    75 730   - wit inspect - wit