Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 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* [apollon005; apollon043; apollon077; apollon078; apollon087; apollon118] [apollon061; apollon077; apollon078; apollon086; apollon134] [apollon038; apollon077; apollon078; apollon083] [apollon077; apollon078; apollon161] 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: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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 22:41:19 CET 2017-12-02 21:10:50 CET 2017-12-02 22:39:24 CET 2017-12-02 22:51:52 CET 2017-12-02 23:01:21 CET 2017-12-02 19:44:15 CET 2017-12-02 21:36:25 CET
Run set symbiotic.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Loops
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.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 .19 12 1.8 false(unreach-call) 1 wit inspect 3.2  270 true -32 wit inspect 4.9   250   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/bubble_sort_false-unreach-call.i false(unreach-call) 1 wit inspect .26 12 2.7 unknown 0 wit inspect 4.7  270 error (7) 0 wit inspect 5.5   210   unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16 11 1.9 false(unreach-call) 1 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 3.6   250   unknown 0 wit inspect 2.8  190 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 .97 15 13   timeout 0 wit inspect 92    1000 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.0  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16 11 1.6 false(unreach-call) 1 wit inspect 4.2  260 true -32 wit inspect 4.0   250   unknown 0 wit inspect 2.0  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i unknown 0 wit inspect .19 11 1.9 error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .026 4.8 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i unknown 0 wit inspect .22 12 2.2 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i unknown 0 wit inspect .19 12 2.3 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 1 wit inspect .16 11 1.7 false(unreach-call) 1 wit inspect 7.0  520 timeout 0 wit inspect 97     4500   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    1700 9700   error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0010 .29 - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i timeout (timeout) 0 wit inspect 900    1800 11000   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .65 51 error (invalid witness file) 0 wit inspect .0035 .26 - wit inspect - wit inspect
loops/nec11_false-unreach-call_false-termination.i error (1) 0 wit inspect .12 11 1.0 error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .66 51 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .17 11 2.4 false(unreach-call) 1 wit inspect 4.4  260 true -32 wit inspect 4.5   230   unknown 0 wit inspect 2.8  210 error (2) 0 wit inspect .60   18    - wit inspect - wit inspect
loops/s3_false-unreach-call.i unknown 0 wit inspect .47 12 4.6 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .20 12 2.4 false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 3.3   220   unknown 0 wit inspect 2.9  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .20 11 1.9 false(unreach-call) 1 wit inspect 5.6  270 true -32 wit inspect 3.9   270   unknown 0 wit inspect 2.8  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .17 11 2.3 false(unreach-call) 1 wit inspect 3.9  260 true -32 wit inspect 3.4   270   unknown 0 wit inspect 2.0  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .19 11 2.0 false(unreach-call) 1 wit inspect 6.8  290 true -32 wit inspect 5.4   260   unknown 0 wit inspect 1.9  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .17 11 1.8 false(unreach-call) 1 wit inspect 4.6  270 true -32 wit inspect 4.6   230   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16 11 1.7 false(unreach-call) 1 wit inspect 3.1  260 true -32 wit inspect 3.4   250   unknown 0 wit inspect 1.9  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
loops/sum_array_false-unreach-call.i unknown 0 wit inspect .21 12 2.0 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16 11 1.4 false(unreach-call) 1 wit inspect 3.3  260 true -32 wit inspect 4.5   230   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .17 11 1.5 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 3.5   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .15 11 1.5 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 3.5   250   unknown 0 wit inspect 2.7  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .19 11 1.8 false(unreach-call) 1 wit inspect 3.3  260 true -32 wit inspect 4.5   220   unknown 0 wit inspect 2.0  210 true -32 wit inspect .59   18    - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16 11 1.7 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 2.8  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .19 12 2.2 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16 11 1.7 false(unreach-call) 1 wit inspect 3.3  250 true -32 wit inspect 3.0   230   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .20 12 2.3 false(unreach-call) 1 wit inspect 2.7  260 true -32 wit inspect 3.7   250   unknown 0 wit inspect 3.0  210 error (2) 0 wit inspect .57   18    - wit inspect - wit inspect
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect .18 12 2.2 false(unreach-call) 1 wit inspect 5.0  300 true -32 wit inspect 5.3   240   unknown 0 wit inspect 2.0  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16 11 1.8 false(unreach-call) 1 wit inspect 2.0  260 true -32 wit inspect 5.1   250   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect .18 12 2.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  270 true 2 wit inspect 7.2   280  
loops/bubble_sort_true-unreach-call_true-termination.i true 2 wit inspect .15 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 5.0   230  
loops/count_up_down_true-unreach-call_true-termination.i true 2 wit inspect .17 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4900 true 2 wit inspect 27     330  
loops/eureka_01_true-unreach-call.i true 1 wit inspect .17 11 1.9 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 timeout 0 wit inspect 960     1400  
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect .17 11 2.0 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 56     830  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 900    15000 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .022 4.9
loops/for_infinite_loop_2_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 900    15000 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9
loops/insertion_sort_true-unreach-call_true-termination.i unknown 0 wit inspect .20 12 2.1 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 4.8
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .18 11 2.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    520 true 2 wit inspect 160     720  
loops/linear_sea.ch_true-unreach-call.i unknown 0 wit inspect .18 12 1.9 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .018 4.8
loops/lu.cmp_true-unreach-call.i true 1 wit inspect .16 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 timeout 0 wit inspect 960     4100  
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect .20 12 2.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 10     370  
loops/n.c11_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 900    77 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .023 4.8
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .17 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 6.9   350  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .18 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 9.9   350  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect .17 11 2.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  280 true 2 wit inspect 10     370  
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect .15 11 2.1 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 9.1   380  
loops/sum03_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 900    15000 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .022 4.8
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect .14 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  280 true 2 wit inspect 12     420  
loops/sum_array_true-unreach-call.i unknown 0 wit inspect .20 12 2.0 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 4.9
loops/terminator_02_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    3100 9100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.8
loops/terminator_03_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    69 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 5.0
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect .26 12 3.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 34    1100 true 2 wit inspect 5.4   260  
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect .14 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 5.0   250  
loops/trex03_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    2400 9000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect .18 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 5.4   250  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect .14 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 11     310  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect .65 12 6.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6  300 true 2 wit inspect 7.3   270  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect .14 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 5.4   260  
loops/vogal_true-unreach-call.i true 2 wit inspect .19 11 2.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 35    960 true 2 wit inspect 230     1100  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 900    15000 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 46 error (2) 0 wit inspect .018 4.9
loops/while_infinite_loop_2_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 900    15000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .020 4.8
loops/while_infinite_loop_3_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 900    15000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .020 4.9
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .18 11 1.7 timeout 0 wit inspect 97    930 true -32 wit inspect 5.0   240   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .17 12 1.9 timeout 0 wit inspect 97    1200 true -32 wit inspect 3.8   280   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 wit inspect 2.2  13 31   timeout 0 wit inspect 94    1000 true -32 wit inspect 4.8   250   unknown 0 wit inspect 2.6  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect .16 11 1.5 false(unreach-call) 1 wit inspect 7.7  630 true -32 wit inspect 4.9   260   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect .15 11 1.8 false(unreach-call) 1 wit inspect 5.9  290 true -32 wit inspect 3.2   220   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .14 11 1.6 timeout 0 wit inspect 92    1900 true -32 wit inspect 4.9   260   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .94   18    - wit inspect - wit inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .15 11 1.7 false(unreach-call) 1 wit inspect 2.3  270 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i false(unreach-call) 1 wit inspect .14 11 1.6 timeout 0 wit inspect 91    1900 true -32 wit inspect 3.5   270   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect 3.3    18    - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i out of memory 0 wit inspect 220    15000 3300   error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect .18 11 1.7 false(unreach-call) 1 wit inspect 3.1  260 true -32 wit inspect 3.1   240   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call1.i false(unreach-call) 1 wit inspect .14 11 1.7 timeout 0 wit inspect 92    1900 true -32 wit inspect 3.4   260   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .17 11 1.8 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 3.4   260   unknown 0 wit inspect 2.9  190 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .16 11 1.5 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 3.3   250   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call4.i false(unreach-call) 1 wit inspect .14 11 1.5 timeout 0 wit inspect 91    1700 true -32 wit inspect 5.2   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .15 11 1.6 false(unreach-call) 1 wit inspect 2.8  260 true -32 wit inspect 3.3   260   unknown 0 wit inspect 1.9  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .15 11 1.6 false(unreach-call) 1 wit inspect 3.7  260 true -32 wit inspect 5.0   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect .17 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  270 true 2 wit inspect 10     280  
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect .17 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 timeout 0 wit inspect 960     3600  
loop-acceleration/array_true-unreach-call3_true-termination.i true 2 wit inspect 7.9  15 93   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 9.5   310  
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 7.1  15 84   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 out of memory 0 wit inspect 86     7000  
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect .17 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 7.9   270  
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect .15 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 15    480 timeout 0 wit inspect 960     560  
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect .19 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  310 true 2 wit inspect 62     690  
loop-acceleration/functions_true-unreach-call1_true-termination.i true 1 wit inspect .17 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 500    7000 timeout 0 wit inspect 960     690  
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect .16 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 770    5600 true 2 wit inspect 5.4   250  
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect .17 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 true 2 wit inspect 23     380  
loop-acceleration/overflow_true-unreach-call1.i true 1 wit inspect .16 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 610    7000 timeout 0 wit inspect 960     630  
loop-acceleration/phases_true-unreach-call1.i true 1 wit inspect 200    7800 3400   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 timeout 0 wit inspect 960     640  
loop-acceleration/phases_true-unreach-call2_false-termination.i timeout (timeout) 0 wit inspect 900    11000 9100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .018 5.0
loop-acceleration/simple_true-unreach-call1.i true 1 wit inspect .15 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 timeout 0 wit inspect 960     570  
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect .14 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 3.8   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i true 1 wit inspect .16 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    7000 timeout 0 wit inspect 960     530  
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect .14 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 7.0   260  
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect .16 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  270 true 2 wit inspect 61     440  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect .17 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 7.2   280  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 1 wit inspect .24 24 3.0 false(unreach-call) 1 wit inspect 2.4  270 false(unreach-call) 1 wit inspect 3.3   250   unknown 0 wit inspect 2.8  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i true 1 wit inspect .19 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 timeout 0 wit inspect 960     700  
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i true 1 wit inspect 280    58 4000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    810 timeout 0 wit inspect 960     740  
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i true 1 wit inspect .24 13 3.1 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 810    7000 timeout 0 wit inspect 960     750  
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i timeout (timeout) 0 wit inspect 900    260 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .024 4.8
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true 2 wit inspect 240    15000 2900   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  270 true 2 wit inspect 5.4   260  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i true 2 wit inspect 240    15000 3700   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  270 true 2 wit inspect 5.1   260  
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .19 12 1.9 false(unreach-call) 1 wit inspect 2.9  260 true -32 wit inspect 5.1   260   unknown 0 wit inspect 2.9  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    1400 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .025 5.0
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    1100 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 45 error (2) 0 wit inspect .018 4.8
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 900    1500 7300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 5.0
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    3300 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 5.0
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    3600 9000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 5.0
loop-invgen/down_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    420 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .026 4.8
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    1400 8600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .018 4.9
loop-invgen/half_2_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    1700 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .023 5.0
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    1200 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 5.0
loop-invgen/id_build_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    1700 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .021 4.8
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect .16 12 1.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  280 true 2 wit inspect 9.1   350  
loop-invgen/nest-if3_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    38 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .023 5.0
loop-invgen/nested6_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    3500 9100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .019 4.9
loop-invgen/nested9_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    520 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .026 4.9
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .019 4.8
loop-invgen/seq_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    1500 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.8
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    300 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .020 4.8
loop-invgen/up_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    1800 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 46 error (2) 0 wit inspect .020 4.9
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 wit inspect 6.4  14 91   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 7.2   280  
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout (timeout) 0 wit inspect 900    21 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .020 4.9
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .16 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  270 true 2 wit inspect 8.4   300  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 wit inspect .15 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.2   320  
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect .16 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  260 true 2 wit inspect 8.2   270  
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 7.5  160 100   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 5.4   260  
loop-lit/ddlm2013_true-unreach-call.i timeout (timeout) 0 wit inspect 900    76 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .022 4.9
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect .15 11 1.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 41    490 true 2 wit inspect 120     1300  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout (timeout) 0 wit inspect 900    1600 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 46 error (2) 0 wit inspect .019 4.9
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect .16 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 49    910 true 2 wit inspect 94     1600  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i timeout (timeout) 0 wit inspect 900    39 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.9
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 wit inspect .17 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.8   280  
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect .15 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 true 2 wit inspect 9.8   280  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true 2 wit inspect .18 12 1.7 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 8.4   300  
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i unknown 0 wit inspect 140    270 1700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .19 11 1.8 timeout 0 wit inspect 92    2200 false(unreach-call) 1 wit inspect 3.4   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect .16 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  270 true 2 wit inspect 6.6   260  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect 2.9  180 46   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit