Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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* [apollon073; apollon077; apollon078; apollon119; apollon130] apollon* [apollon077; apollon078; apollon091; apollon114] 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 12:59:33 CET 2017-12-02 09:20:19 CET 2017-12-02 10:53:45 CET 2017-12-02 11:06:16 CET 2017-12-02 11:21:21 CET 2017-12-02 06:57:43 CET 2017-12-02 09:56:59 CET
Run set esbmc-kind.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Loops
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.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 .22  28 2.1  true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 3.1  220 false(unreach-call) 1 wit inspect .57   19    - wit inspect - wit inspect
loops/bubble_sort_false-unreach-call.i false(unreach-call) 1 wit inspect 7.3   230 79    unknown 0 wit inspect 3.4  280 error (7) 0 wit inspect 9.1   210   unknown 0 wit inspect 2.8  240 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .20  28 2.0  false(unreach-call) 1 wit inspect 3.3  270 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   19    - wit inspect - wit inspect
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect .79  29 8.0  true -32 wit inspect 4.3  260 true -32 wit inspect 5.0   240   unknown 0 wit inspect 2.1  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .21  28 2.0  false(unreach-call) 1 wit inspect 3.3  260 true -32 wit inspect 5.6   270   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect .77  28 8.5  true -32 wit inspect 2.5  260 true -32 wit inspect 14     600   unknown 0 wit inspect 2.1  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .64  28 5.5  true -32 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 6.8   270   unknown 0 wit inspect 2.9  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i false(unreach-call) 0 wit inspect .53  28 5.9  true -32 wit inspect 2.7  270 true -32 wit inspect 5.4   260   unknown 0 wit inspect 2.0  210 error (2) 0 wit inspect .57   18    - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 1 wit inspect .18  31 2.2  false(unreach-call) 1 wit inspect 6.8  520 timeout 0 wit inspect 97     4500   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .36  28 3.0  true -32 wit inspect 3.9  260 true -32 wit inspect 4.5   220   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i out of memory 0 wit inspect 440     15000 4400    error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0011 .27 - wit inspect - wit inspect
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .11  28 1.3  false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 3.3   260   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .57   19    - wit inspect - wit inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .20  28 2.3  false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 2.9  210 error (2) 0 wit inspect .58   18    - wit inspect - wit inspect
loops/s3_false-unreach-call.i false(unreach-call) 1 wit inspect 18     740 210    false(unreach-call) 1 wit inspect 4.8  280 true -32 wit inspect 5.4   320   unknown 0 wit inspect 3.6  280 error (2) 0 wit inspect .75   19    - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect .61  28 7.5  true -32 wit inspect 3.6  260 true -32 wit inspect 5.2   260   unknown 0 wit inspect 2.1  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .15  28 2.3  false(unreach-call) 1 wit inspect 5.2  270 true -32 wit inspect 7.1   280   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .20  28 1.9  false(unreach-call) 1 wit inspect 4.1  260 true -32 wit inspect 5.2   270   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .20  28 2.1  false(unreach-call) 1 wit inspect 5.2  270 true -32 wit inspect 4.8   270   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .14  28 1.1  false(unreach-call) 1 wit inspect 2.4  260 true -32 wit inspect 5.6   260   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .12  28 1.2  false(unreach-call) 1 wit inspect 2.2  260 true -32 wit inspect 4.8   250   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect .28  28 2.7  true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 3.9   260   unknown 0 wit inspect 2.0  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .13  28 1.4  false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 3.7   260   unknown 0 wit inspect 2.9  210 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 .18  28 2.4  false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.9   250   unknown 0 wit inspect 2.0  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 .14  28 1.8  false(unreach-call) 1 wit inspect 2.3  260 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .25  28 2.5  false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 3.5   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  28 1.5  false(unreach-call) 1 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .43  28 2.9  false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 4.8   260   unknown 0 wit inspect 2.1  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 .21  28 2.1  false(unreach-call) 1 wit inspect 4.0  260 true -32 wit inspect 6.4   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect .26  28 3.0  timeout 0 wit inspect 92    1900 true -32 wit inspect 5.1   240   unknown 0 wit inspect 3.0  210 error (2) 0 wit inspect .58   18    - wit inspect - wit inspect
loops/vogal_false-unreach-call.i false(unreach-call) 0 wit inspect .95  36 8.9  true -32 wit inspect 2.4  260 true -32 wit inspect 7.1   270   unknown 0 wit inspect 2.3  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .11  28 .87 false(unreach-call) 1 wit inspect 2.0  250 true -32 wit inspect 4.6   250   unknown 0 wit inspect 2.6  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 .095 26 .95 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  270 true 2 wit inspect 7.7   280  
loops/bubble_sort_true-unreach-call_true-termination.i true 2 wit inspect .13  27 1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 5.0   240  
loops/count_up_down_true-unreach-call_true-termination.i timeout 0 wit inspect 900     1400 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .021 4.9
loops/eureka_01_true-unreach-call.i true 1 wit inspect .33  28 5.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5900 timeout 0 wit inspect 960     1100  
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect .12  26 .80 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6700 true 2 wit inspect 53     820  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect .075 26 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 5.5   250  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i timeout 0 wit inspect 900     11000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .024 4.9
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     140 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .020 4.9
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .12  26 .94 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    520 true 2 wit inspect 180     770  
loops/linear_sea.ch_true-unreach-call.i timeout 0 wit inspect 900     980 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9
loops/lu.cmp_true-unreach-call.i true 1 wit inspect .23  29 2.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5800 timeout 0 wit inspect 960     3900  
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect .12  26 .81 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  280 true 2 wit inspect 10     370  
loops/n.c11_true-unreach-call_false-termination.i timeout 0 wit inspect 900     2500 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .018 4.9
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .10  26 .74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 true 2 wit inspect 7.1   340  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .10  26 .68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 true 2 wit inspect 7.9   340  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect .11  26 .75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  280 true 2 wit inspect 9.5   370  
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 380     830 4400    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 11     380  
loops/sum03_true-unreach-call_false-termination.i timeout 0 wit inspect 900     10000 9600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .024 4.8
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect .081 26 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  260 true 2 wit inspect 9.8   420  
loops/sum_array_true-unreach-call.i timeout 0 wit inspect 900     310 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.8
loops/terminator_02_true-unreach-call_true-termination.i timeout 0 wit inspect 900     78 14000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .024 5.0
loops/terminator_03_true-unreach-call_true-termination.i timeout 0 wit inspect 900     85 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 4.8
loops/trex01_true-unreach-call_true-termination.i timeout 0 wit inspect 900     910 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .019 5.0
loops/trex02_true-unreach-call_true-termination.i timeout 0 wit inspect 900     460 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9
loops/trex03_true-unreach-call_true-termination.i timeout 0 wit inspect 900     370 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.9
loops/trex04_true-unreach-call_false-termination.i timeout 0 wit inspect 900     110 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .024 5.0
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect .11  26 .76 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 7.9   310  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect .087 27 .86 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.1  360 true 2 wit inspect 7.5   260  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect .075 26 .80 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  270 true 2 wit inspect 5.2   260  
loops/vogal_true-unreach-call.i true 2 wit inspect .17  26 1.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 53    970 true 2 wit inspect 200     1100  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i timeout 0 wit inspect 900     14000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .038 4.9
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect .077 26 .79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 5.0   250  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i timeout 0 wit inspect 900     12000 12000    - 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
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 72     270 620    true -32 wit inspect 6.1  350 timeout 0 wit inspect 97     5000   unknown 0 wit inspect 6.6  370 false(unreach-call) 1 wit inspect .90   23    - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 300     990 2900    timeout 0 wit inspect 92    1000 timeout 0 wit inspect 98     6400   unknown 0 wit inspect 17    700 false(unreach-call) 1 wit inspect 1.7    38    - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 wit inspect 70     390 650    true -32 wit inspect 12    500 timeout 0 wit inspect 96     5000   unknown 0 wit inspect 6.4  350 true -32 wit inspect .91   23    - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect 11     140 140    false(unreach-call) 1 wit inspect 7.6  630 true -32 wit inspect 5.2   260   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 2.8   28 23    true -32 wit inspect 3.4  250 out of memory 0 wit inspect 60     7000   unknown 0 wit inspect 2.4  210 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i out of memory 0 wit inspect 800     15000 10000    error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .70 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .22  28 1.3  false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 3.4   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900     9600 11000    error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .67 50 error (invalid witness file) 0 wit inspect .0026 .29 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i timeout 0 wit inspect 900     7600 10000    error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0011 .30 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect .11  28 1.6  false(unreach-call) 1 wit inspect 2.3  280 false(unreach-call) 1 wit inspect 4.5   260   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 timeout 0 wit inspect 900     11000 9400    error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 51 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .15  28 1.3  false(unreach-call) 1 wit inspect 2.7  260 false(unreach-call) 1 wit inspect 4.7   250   unknown 0 wit inspect 2.7  210 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 .080 28 .81 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 4.7   250   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call4.i timeout 0 wit inspect 900     11000 11000    error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .087 28 .85 false(unreach-call) 1 wit inspect 2.2  260 true -32 wit inspect 3.7   260   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .083 28 .87 false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 3.9   260   unknown 0 wit inspect 1.9  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 15     150 200    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  270 true 2 wit inspect 6.8   280  
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect 89     510 1100    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 timeout 0 wit inspect 960     3300  
loop-acceleration/array_true-unreach-call3_true-termination.i true 2 wit inspect 17     280 200    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 true 2 wit inspect 11     320  
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 19     350 270    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 out of memory 0 wit inspect 130     7000  
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect .074 26 .88 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 7.0   270  
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 1.8   31 27    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    480 timeout 0 wit inspect 960     650  
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect .19  26 1.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1  310 true 2 wit inspect 69     690  
loop-acceleration/functions_true-unreach-call1_true-termination.i out of memory 0 wit inspect 810     15000 9000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 5.0
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 440     840 5200    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 670    6100 true 2 wit inspect 6.0   260  
loop-acceleration/nested_true-unreach-call1.i timeout 0 wit inspect 900     9400 9500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.8
loop-acceleration/overflow_true-unreach-call1.i timeout 0 wit inspect 900     11000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .018 4.8
loop-acceleration/phases_true-unreach-call1.i timeout 0 wit inspect 900     7500 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .018 4.8
loop-acceleration/phases_true-unreach-call2_false-termination.i timeout 0 wit inspect 900     440 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .018 4.8
loop-acceleration/simple_true-unreach-call1.i timeout 0 wit inspect 900     11000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 5.0
loop-acceleration/simple_true-unreach-call2_true-termination.i timeout 0 wit inspect 900     250 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .024 4.8
loop-acceleration/simple_true-unreach-call3_true-termination.i timeout 0 wit inspect 900     1500 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.8
loop-acceleration/simple_true-unreach-call4.i timeout 0 wit inspect 900     11000 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .019 4.9
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect .13  26 .95 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  280 true 2 wit inspect 81     440  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect .11  26 .74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  260 true 2 wit inspect 7.2   270  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 1 wit inspect .15  28 1.3  false(unreach-call) 1 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 4.7   240   unknown 0 wit inspect 2.0  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 16     160 220    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     600  
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 .66 41 error (2) 0 wit inspect .019 4.9
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i timeout 0 wit inspect 900     6600 9600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .024 4.8
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i timeout 0 wit inspect 900     240 13000    - 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-crafted/simple_vardep_true-unreach-call1_true-termination.i true 2 wit inspect .88  29 12    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 5.5   260  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i true 2 wit inspect .075 26 .94 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  270 true 2 wit inspect 5.4   260  
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .26  28 1.8  false(unreach-call) 1 wit inspect 3.3  260 true -32 wit inspect 5.5   270   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout 0 wit inspect 900     91 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 5.0
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect .11  26 1.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 12     350  
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i timeout 0 wit inspect 900     400 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .025 4.8
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 0 wit inspect 900     81 8700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .018 4.9
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i timeout 0 wit inspect 900     150 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .023 4.8
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 wit inspect 900     510 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .023 4.9
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 0 wit inspect 900     1000 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.9
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900     470 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .024 4.8
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     620 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .018 5.0
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect .17  26 1.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 true 2 wit inspect 6.4   270  
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect .083 26 .78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  280 true 2 wit inspect 11     350  
loop-invgen/nest-if3_true-unreach-call_true-termination.i timeout 0 wit inspect 900     320 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9
loop-invgen/nested6_true-unreach-call_true-termination.i timeout 0 wit inspect 900     700 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .023 4.8
loop-invgen/nested9_true-unreach-call_true-termination.i timeout 0 wit inspect 900     4300 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.8
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i timeout 0 wit inspect 900     910 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.9
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900     270 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .49 41 error (2) 0 wit inspect .023 4.9
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i out of memory 0 wit inspect 300     15000 3000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .025 4.8
loop-invgen/up_true-unreach-call_true-termination.i timeout 0 wit inspect 900     720 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .018 4.8
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 wit inspect 680     1300 8200    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 7.8   260  
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     140 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .11  26 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 true 2 wit inspect 9.8   310  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     340 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect .29  27 3.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 true 2 wit inspect 8.1   270  
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect .16  26 1.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  270 true 2 wit inspect 7.6   260  
loop-lit/ddlm2013_true-unreach-call.i timeout 0 wit inspect 900     1400 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .021 5.0
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect .28  26 2.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 43    580 true 2 wit inspect 120     1100  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     870 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.9
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect .30  26 4.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 45    1000 true 2 wit inspect 97     1800  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     92 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.8
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     330 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.9
loop-lit/jm2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     1000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .019 4.9
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     1300 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .024 4.8
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     200 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.8
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .11  28 .97 timeout 0 wit inspect 92    2200 false(unreach-call) 1 wit inspect 3.3   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loop-new/count_by_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900     12000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .023 5.0
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect .078 26 .74 - wit inspect - wit inspect - wit inspect - wit inspect