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* [apollon010; apollon035; apollon045; apollon077; apollon078; apollon138] [apollon007; apollon077; apollon078; apollon143] 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-12-01 08:49:27 CET 2017-12-01 22:53:44 CET 2017-12-01 23:38:04 CET 2017-12-01 23:47:42 CET 2017-12-01 23:55:24 CET 2017-12-01 22:20:30 CET 2017-12-01 23:01:53 CET
Run set esbmc-incr.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Loops
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-incr.2017-12-01_0849.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.2  true -32 wit inspect 3.4  250 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 2.9  190 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 5.5   140 61    unknown 0 wit inspect 4.9  280 error (7) 0 wit inspect 8.2   210   unknown 0 wit inspect 2.5  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .20  28 1.4  false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.3   240   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect .48  28 4.0  true -32 wit inspect 3.0  250 true -32 wit inspect 5.7   250   unknown 0 wit inspect 3.0  190 true -32 wit inspect .62   18    - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .36  28 3.7  false(unreach-call) 1 wit inspect 4.0  280 true -32 wit inspect 7.3   270   unknown 0 wit inspect 3.0  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.4   30 15    true -32 wit inspect 4.6  260 true -32 wit inspect 21     680   unknown 0 wit inspect 2.2  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .59  28 5.1  true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 7.1   270   unknown 0 wit inspect 2.1  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i false(unreach-call) 0 wit inspect .47  28 5.2  true -32 wit inspect 3.8  270 true -32 wit inspect 5.2   260   unknown 0 wit inspect 2.1  210 error (2) 0 wit inspect .60   18    - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 1 wit inspect .088 29 1.3  false(unreach-call) 1 wit inspect 8.2  520 timeout 0 wit inspect 97     4500   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .54  28 4.2  false(unreach-call) 1 wit inspect 3.7  260 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i out of memory 0 wit inspect 460     15000 3700    error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0031 .29 - wit inspect - wit inspect
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .16  28 1.1  false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 3.3   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .24  28 2.1  false(unreach-call) 1 wit inspect 3.4  270 false(unreach-call) 1 wit inspect 4.8   260   unknown 0 wit inspect 2.1  210 error (2) 0 wit inspect .58   18    - wit inspect - wit inspect
loops/s3_false-unreach-call.i false(unreach-call) 1 wit inspect 15     600 180    false(unreach-call) 1 wit inspect 7.4  280 true -32 wit inspect 5.5   330   unknown 0 wit inspect 5.2  280 error (2) 0 wit inspect .74   19    - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect .81  28 6.6  true -32 wit inspect 4.0  260 true -32 wit inspect 5.1   260   unknown 0 wit inspect 2.2  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 .16  28 1.7  false(unreach-call) 1 wit inspect 4.9  270 true -32 wit inspect 6.6   280   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16  28 1.5  false(unreach-call) 1 wit inspect 4.0  290 true -32 wit inspect 5.0   280   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .21  28 1.9  false(unreach-call) 1 wit inspect 7.1  270 true -32 wit inspect 5.0   280   unknown 0 wit inspect 2.0  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 .13  28 .86 false(unreach-call) 1 wit inspect 3.5  260 true -32 wit inspect 5.5   260   unknown 0 wit inspect 2.8  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 .78 false(unreach-call) 1 wit inspect 3.5  260 true -32 wit inspect 5.1   250   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect .30  28 2.9  true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 5.3   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 .16  28 1.2  false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 3.9   260   unknown 0 wit inspect 2.8  210 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 .22  28 1.5  false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .19  28 1.5  false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .21  28 1.4  false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 3.6   270   unknown 0 wit inspect 2.1  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .13  28 1.3  false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 4.6   260   unknown 0 wit inspect 2.7  180 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 .19  28 2.3  false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.7   250   unknown 0 wit inspect 2.8  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) 1 wit inspect .19  28 2.1  false(unreach-call) 1 wit inspect 3.3  260 true -32 wit inspect 5.8   260   unknown 0 wit inspect 2.9  190 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 .16  28 1.6  false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 5.1   230   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 .82  35 8.4  true -32 wit inspect 3.9  260 true -32 wit inspect 7.1   270   unknown 0 wit inspect 2.2  210 true -32 wit inspect .59   18    - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .075 28 .95 false(unreach-call) 1 wit inspect 3.0  260 true -32 wit inspect 4.7   260   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect .10  26 .82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 true 2 wit inspect 7.9   280  
loops/bubble_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     1600 7800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.9
loops/count_up_down_true-unreach-call_true-termination.i timeout 0 wit inspect 900     1400 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 5.0
loops/eureka_01_true-unreach-call.i true 1 wit inspect .15  27 1.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5900 timeout 0 wit inspect 960     1400  
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect .11  27 .77 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5700 true 2 wit inspect 58     820  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i timeout 0 wit inspect 900     11000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .024 5.0
loops/for_infinite_loop_2_true-unreach-call_false-termination.i timeout 0 wit inspect 900     11000 9500    - 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
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     130 11000    - 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/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .11  26 .69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    400 true 2 wit inspect 150     760  
loops/linear_sea.ch_true-unreach-call.i timeout 0 wit inspect 900     980 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .025 4.9
loops/lu.cmp_true-unreach-call.i true 1 wit inspect .12  27 1.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 timeout 0 wit inspect 960     4500  
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect .086 26 .85 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  300 true 2 wit inspect 11     390  
loops/n.c11_true-unreach-call_false-termination.i timeout 0 wit inspect 900     2500 12000    - 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
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .10  26 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  270 true 2 wit inspect 7.1   340  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .10  26 .63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 8.4   350  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect .25  27 2.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  280 true 2 wit inspect 11     370  
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 380     830 4300    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 8.9   370  
loops/sum03_true-unreach-call_false-termination.i timeout 0 wit inspect 900     10000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .024 4.8
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect .078 26 .90 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  270 true 2 wit inspect 9.8   420  
loops/sum_array_true-unreach-call.i timeout 0 wit inspect 900     250 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .024 4.8
loops/terminator_02_true-unreach-call_true-termination.i timeout 0 wit inspect 900     83 11000    - 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
loops/terminator_03_true-unreach-call_true-termination.i timeout 0 wit inspect 900     89 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .023 4.9
loops/trex01_true-unreach-call_true-termination.i timeout 0 wit inspect 900     900 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .020 5.0
loops/trex02_true-unreach-call_true-termination.i timeout 0 wit inspect 900     460 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 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 .52 42 error (2) 0 wit inspect .018 5.0
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 .72 43 error (2) 0 wit inspect .024 4.8
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect .095 26 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 9.9   290  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect .29  28 4.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.0  290 true 2 wit inspect 7.4   260  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect .088 26 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  280 true 2 wit inspect 5.1   270  
loops/vogal_true-unreach-call.i true 2 wit inspect .13  27 .93 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 54    1000 true 2 wit inspect 240     1200  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i timeout 0 wit inspect 900     14000 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .020 4.9
loops/while_infinite_loop_2_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 .63 41 error (2) 0 wit inspect .019 4.8
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 .68 43 error (2) 0 wit inspect .022 4.8
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 71     270 580    true -32 wit inspect 5.8  350 timeout 0 wit inspect 96     5000   unknown 0 wit inspect 9.1  370 false(unreach-call) 1 wit inspect .87   23    - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 310     990 2800    timeout 0 wit inspect 92    1000 timeout 0 wit inspect 97     6600   unknown 0 wit inspect 22    690 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 71     390 610    true -32 wit inspect 12    500 timeout 0 wit inspect 96     5000   unknown 0 wit inspect 10    380 true -32 wit inspect .89   23    - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect 11     150 120    false(unreach-call) 1 wit inspect 11    510 true -32 wit inspect 5.1   260   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 2.5   28 29    true -32 wit inspect 3.6  260 out of memory 0 wit inspect 68     7000   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i out of memory 0 wit inspect 820     15000 8900    error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .85 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 .20  28 1.6  false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 3.5   250   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900     9500 10000    error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i timeout 0 wit inspect 900     7600 9600    error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect .16  28 1.2  false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.6   250   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call1.i timeout 0 wit inspect 900     11000 12000    error (invalid witness file) 0 wit inspect .64 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 .0012 .27 - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .082 28 .81 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 4.8   240   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .79   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .12  28 .72 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 3.4   250   unknown 0 wit inspect 1.9  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 10000    error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0010 .27 - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .081 28 .88 false(unreach-call) 1 wit inspect 3.9  260 true -32 wit inspect 5.4   260   unknown 0 wit inspect 2.7  180 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 .080 28 .94 false(unreach-call) 1 wit inspect 3.9  260 true -32 wit inspect 5.1   260   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 15     150 190    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.6  270 true 2 wit inspect 8.9   280  
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect 88     510 930    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 timeout 0 wit inspect 960     3300  
loop-acceleration/array_true-unreach-call3_true-termination.i true 2 wit inspect 17     280 190    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  270 true 2 wit inspect 9.6   310  
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 19     350 220    - 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 11     130 140    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 8.3   270  
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 1.9   31 24    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    480 timeout 0 wit inspect 960     660  
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect .14  26 1.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.2  320 true 2 wit inspect 65     670  
loop-acceleration/functions_true-unreach-call1_true-termination.i out of memory 0 wit inspect 810     15000 9100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 5.0
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 450     840 6000    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 true 2 wit inspect 6.0   260  
loop-acceleration/nested_true-unreach-call1.i timeout 0 wit inspect 900     9300 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .017 4.9
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 .75 44 error (2) 0 wit inspect .018 5.0
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 .56 43 error (2) 0 wit inspect .025 4.9
loop-acceleration/phases_true-unreach-call2_false-termination.i timeout 0 wit inspect 900     390 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .019 4.8
loop-acceleration/simple_true-unreach-call1.i timeout 0 wit inspect 900     11000 9100    - 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/simple_true-unreach-call2_true-termination.i timeout 0 wit inspect 900     250 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.9
loop-acceleration/simple_true-unreach-call3_true-termination.i timeout 0 wit inspect 900     1500 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.8
loop-acceleration/simple_true-unreach-call4.i timeout 0 wit inspect 900     11000 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .021 4.9
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect .078 26 .72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  280 true 2 wit inspect 57     450  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect .11  26 .78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 8.8   270  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 1 wit inspect .16  28 1.3  false(unreach-call) 1 wit inspect 3.6  270 false(unreach-call) 1 wit inspect 4.8   240   unknown 0 wit inspect 2.8  210 true -32 wit inspect .58   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    4300 timeout 0 wit inspect 960     700  
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i timeout 0 wit inspect 900     3400 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .82 43 error (2) 0 wit inspect .020 4.9
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i timeout 0 wit inspect 900     6700 9600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .023 4.8
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i timeout 0 wit inspect 900     230 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .025 4.8
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i timeout 0 wit inspect 900     10000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .020 4.9
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i timeout 0 wit inspect 900     11000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .020 4.9
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .22  28 2.6  false(unreach-call) 1 wit inspect 3.9  260 true -32 wit inspect 3.6   260   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     85 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .024 4.8
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i timeout 0 wit inspect 900     790 11000    - 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-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i timeout 0 wit inspect 900     410 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .020 4.8
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 0 wit inspect 900     82 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .017 4.9
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i timeout 0 wit inspect 900     140 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .020 4.8
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 wit inspect 900     510 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .76 44 error (2) 0 wit inspect .019 4.8
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 .53 41 error (2) 0 wit inspect .019 4.9
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900     480 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
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout 0 wit inspect 900     560 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 45 error (2) 0 wit inspect .019 4.8
loop-invgen/id_build_true-unreach-call_true-termination.i timeout 0 wit inspect 900     1000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .020 4.9
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect .12  26 .79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  270 true 2 wit inspect 9.0   340  
loop-invgen/nest-if3_true-unreach-call_true-termination.i timeout 0 wit inspect 900     360 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .021 4.9
loop-invgen/nested6_true-unreach-call_true-termination.i timeout 0 wit inspect 900     730 9800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .025 4.8
loop-invgen/nested9_true-unreach-call_true-termination.i timeout 0 wit inspect 900     4300 10000    - 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/sendmail-close-angle_true-unreach-call_true-termination.i timeout 0 wit inspect 900     920 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 4.8
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900     280 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 4.9
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i out of memory 0 wit inspect 290     15000 3300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 45 error (2) 0 wit inspect .025 4.9
loop-invgen/up_true-unreach-call_true-termination.i timeout 0 wit inspect 900     730 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .018 4.8
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 wit inspect 680     1300 8100    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 true 2 wit inspect 8.5   270  
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 .67 41 error (2) 0 wit inspect .021 4.8
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .085 26 .67 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 true 2 wit inspect 9.5   290  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     350 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 4.9
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect .24  26 3.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  270 true 2 wit inspect 7.3   260  
loop-lit/css2003_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     5600 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .49 42 error (2) 0 wit inspect .022 4.8
loop-lit/ddlm2013_true-unreach-call.i timeout 0 wit inspect 900     1400 9900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .019 4.8
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect .27  26 2.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 46    600 true 2 wit inspect 96     1400  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     870 9900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.8
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect .32  26 3.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 60    910 true 2 wit inspect 98     1600  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     94 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.8
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     330 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .024 4.8
loop-lit/jm2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     1000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 41 error (2) 0 wit inspect .019 4.8
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 .54 43 error (2) 0 wit inspect .018 4.8
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900     190 12000    - 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
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .12  28 .82 timeout 0 wit inspect 92    2200 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 2.9  180 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 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .019 4.8
loop-new/count_by_1_variant_true-unreach-call_true-termination.i timeout 0 wit inspect 900     11000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit