Tool CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:36:48 CET 2017-12-01 08:27:40 CET 2017-12-01 08:32:13 CET 2017-12-01 08:39:14 CET 2017-12-01 04:24:39 CET 2017-12-01 07:43:13 CET
Run set cpa-bam-slicing.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Loops
Options -ldv-bam-svcomp -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
loops/array_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.4 290 29 true -32 wit inspect 3.0  250 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/bubble_sort_false-unreach-call.i false(unreach-call) 1 wit inspect 5.0 300 43 true -32 wit inspect 5.0  270 error (7) 0 wit inspect 8.1   210   unknown 0 wit inspect 3.9  220 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.1 280 29 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 5.3   250   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/eureka_01_false-unreach-call_true-termination.i true -32 wit inspect 23   860 190 timeout 0 wit inspect 91    1900 timeout 0 wit inspect 96     1500   unknown 0 wit inspect .97 52 error (1) 0 wit inspect .090  9.0  - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.5 280 31 timeout 0 wit inspect 92    2200 true -32 wit inspect 4.7   220   unknown 0 wit inspect 2.8  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.5 290 31 timeout 0 wit inspect 92    2000 true -32 wit inspect 3.2   230   unknown 0 wit inspect 2.9  210 true -32 wit inspect .63   19    - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 4.4 300 39 timeout 0 wit inspect 92    2000 true -32 wit inspect 4.6   230   unknown 0 wit inspect 2.9  210 true -32 wit inspect .66   19    - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i unknown 0 wit inspect 3.2 280 28 error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 1 wit inspect 3.2 270 29 true -32 wit inspect 4.4  260 true -32 wit inspect 20     1700   unknown 0 wit inspect 3.0  190 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 4.0 290 36 timeout 0 wit inspect 92    1900 true -32 wit inspect 5.4   260   unknown 0 wit inspect 2.9  210 true -32 wit inspect 7.6    19    - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i timeout 0 wit inspect 900   4300 11000 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .046 4.8 error (invalid witness file) 0 wit inspect .88 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 3.2 280 29 true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.2 280 29 timeout 0 wit inspect 92    2100 true -32 wit inspect 4.6   220   unknown 0 wit inspect 2.9  190 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/s3_false-unreach-call.i false(unreach-call) 0 wit inspect 16   540 120 true -32 wit inspect 5.5  270 true -32 wit inspect 7.8   320   unknown 0 wit inspect 4.3  220 error (2) 0 wit inspect .77   20    - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 5.3 300 48 true -32 wit inspect 4.6  260 true -32 wit inspect 6.6   300   unknown 0 wit inspect 3.0  210 true -32 wit inspect .61   19    - wit inspect - wit inspect
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 4.1 300 34 timeout 0 wit inspect 92    2100 true -32 wit inspect 4.7   240   unknown 0 wit inspect 2.9  180 true -32 wit inspect .59   19    - wit inspect - wit inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.7 290 32 timeout 0 wit inspect 92    2000 true -32 wit inspect 5.7   300   unknown 0 wit inspect 3.1  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 4.2 290 34 timeout 0 wit inspect 92    2000 true -32 wit inspect 4.7   220   unknown 0 wit inspect 2.8  190 true -32 wit inspect .59   19    - wit inspect - wit inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.2 290 33 true -32 wit inspect 3.5  260 out of memory 0 wit inspect 84     7000   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.5 280 33 true -32 wit inspect 3.6  260 true -32 wit inspect 5.7   290   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
loops/sum_array_false-unreach-call.i false(unreach-call) 0 wit inspect 4.0 290 35 timeout 0 wit inspect 91    2000 true -32 wit inspect 4.8   230   unknown 0 wit inspect 2.8  210 true -32 wit inspect .62   19    - wit inspect - wit inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.9 270 26 true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 5.0   260   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.9 280 26 true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 7.2   250   unknown 0 wit inspect 2.9  180 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 3.3 290 26 true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.5   260   unknown 0 wit inspect 2.9  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.2 290 27 true -32 wit inspect 3.9  260 true -32 wit inspect 4.6   230   unknown 0 wit inspect 2.0  210 true -32 wit inspect .62   18    - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.1 270 31 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 2.9  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.3 290 30 true -32 wit inspect 4.1  260 true -32 wit inspect 5.0   240   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .63   19    - wit inspect - wit inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 11   470 87 true -32 wit inspect 3.8  260 true -32 wit inspect 9.8   480   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.8 290 36 timeout 0 wit inspect 91    1900 true -32 wit inspect 5.2   230   unknown 0 wit inspect 3.0  190 error (2) 0 wit inspect .61   18    - wit inspect - wit inspect
loops/vogal_false-unreach-call.i false(unreach-call) 0 wit inspect 7.8 420 65 true -32 wit inspect 9.5  410 true -32 wit inspect 4.9   240   unknown 0 wit inspect 3.0  220 true -32 wit inspect .62   19    - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.1 270 27 timeout 0 wit inspect 96    2700 false(unreach-call) 1 wit inspect 4.7   230   timeout 0 wit inspect 96    2800 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 3.1 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  270 true 2 wit inspect 7.6   280  
loops/bubble_sort_true-unreach-call_true-termination.i true 2 wit inspect 2.6 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 4.9   230  
loops/count_up_down_true-unreach-call_true-termination.i unknown 0 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .020 4.9
loops/eureka_01_true-unreach-call.i true 1 wit inspect 10   580 82 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 timeout 0 wit inspect 960     1400  
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect 3.7 280 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 53     830  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  270 false(unreach-call) -16 wit inspect 4.9   230  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 false(unreach-call) -16 wit inspect 4.9   220  
loops/insertion_sort_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.5 280 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 true 2 wit inspect 4.7   220  
loops/invert_string_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.9 290 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 true 2 wit inspect 4.9   220  
loops/linear_sea.ch_true-unreach-call.i unknown 0 wit inspect 3.2 290 27 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .022 5.0
loops/lu.cmp_true-unreach-call.i true 1 wit inspect 3.5 270 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5900 timeout 0 wit inspect 960     3400  
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 3.2 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 13     390  
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect 3.0 270 29 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 850    7000 true 2 wit inspect 8.5   350  
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 3.2 270 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 7.9   350  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 3.0 270 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 6.9   350  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 3.0 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  300 true 2 wit inspect 9.5   370  
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 3.9 270 38 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 10     380  
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect 5.8 410 52 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  270 true 2 wit inspect 5.6   270  
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  270 true 2 wit inspect 10     430  
loops/sum_array_true-unreach-call.i false(unreach-call) -16 wit inspect 4.1 290 38 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 true 2 wit inspect 5.1   230  
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 false(unreach-call) -16 wit inspect 4.8   230  
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 5.6   260  
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 6.4 350 55 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 33    1000 false(unreach-call) -16 wit inspect 4.7   230  
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 true 2 wit inspect 5.8   260  
loops/trex03_true-unreach-call_true-termination.i unknown 0 wit inspect 3.2 290 32 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 5.0
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  270 true 2 wit inspect 5.4   260  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect 12   470 98 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 8.7   310  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 17   790 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.3  370 true 2 wit inspect 8.7   270  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 3.2 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  270 true 2 wit inspect 6.5   260  
loops/vogal_true-unreach-call.i true 2 wit inspect 58   3100 590 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 49    790 true 2 wit inspect 270     1300  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 5.5   260  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 2.7 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 6.1   260  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5200 true 2 wit inspect 6.4   250  
loop-acceleration/array_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   3900 12000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 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/array_false-unreach-call2_true-termination.i timeout 0 wit inspect 900   4200 12000 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0010 .34 - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 0 wit inspect 900   4200 9700 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .045 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i timeout 0 wit inspect 900   4200 12000 error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0020 .27 - wit inspect - wit inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 52   1800 420 true -32 wit inspect 3.5  260 out of memory 0 wit inspect 69     7000   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .61   20    - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   4300 7800 error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 3.1 280 26 true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 5.3   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900   4200 9400 error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i timeout 0 wit inspect 900   4100 12000 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 0 wit inspect 2.9 280 27 true -32 wit inspect 3.1  250 true -32 wit inspect 4.6   220   unknown 0 wit inspect 2.9  190 true -32 wit inspect .60   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call1.i timeout 0 wit inspect 900   4300 11000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 3.1 280 31 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.7   240   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .90   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect 3.0 280 26 timeout 0 wit inspect 91    1900 false(unreach-call) 1 wit inspect 5.1   240   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call4.i timeout 0 wit inspect 900   4300 13000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .83 50 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 3.3 290 34 true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 8.7   340   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 3.4 280 31 true -32 wit inspect 3.0  250 false(unreach-call) 1 wit inspect 6.0   360   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
loop-acceleration/array_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   3900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .021 4.8
loop-acceleration/array_true-unreach-call2_true-termination.i timeout 0 wit inspect 900   4200 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 5.0
loop-acceleration/array_true-unreach-call3_true-termination.i timeout 0 wit inspect 900   4200 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.9
loop-acceleration/array_true-unreach-call4_true-termination.i timeout 0 wit inspect 900   4200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .020 4.8
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 3.0 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  280 true 2 wit inspect 7.4   270  
loop-acceleration/diamond_true-unreach-call1_true-termination.i unknown 0 wit inspect 64   2400 470 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 5.0
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect 10   470 79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.0  310 true 2 wit inspect 63     660  
loop-acceleration/functions_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   4300 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.9
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 2.7 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 750    6400 true 2 wit inspect 5.9   260  
loop-acceleration/nested_true-unreach-call1.i timeout 0 wit inspect 900   4200 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .024 4.8
loop-acceleration/overflow_true-unreach-call1.i true 1 wit inspect 3.3 270 31 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    7000 timeout 0 wit inspect 960     580  
loop-acceleration/phases_true-unreach-call1.i timeout 0 wit inspect 900   4100 9400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .018 4.8
loop-acceleration/phases_true-unreach-call2_false-termination.i unknown 0 wit inspect 3.2 290 29 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.8
loop-acceleration/simple_true-unreach-call1.i timeout 0 wit inspect 900   4300 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .020 4.9
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  270 true 2 wit inspect 5.7   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i timeout 0 wit inspect 900   8500 7100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .022 4.9
loop-acceleration/simple_true-unreach-call4.i timeout 0 wit inspect 900   4300 9100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.8
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 4.0 280 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  290 true 2 wit inspect 39     440  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 8.2   270  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i error 0 wit inspect 2.6 260 21 error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   3900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.9
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i error 0 wit inspect 2.5 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 43 error (2) 0 wit inspect .020 5.0
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i error 0 wit inspect 2.5 260 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .020 4.8
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i error 0 wit inspect 2.5 260 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 5.0
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true 2 wit inspect 5.2 330 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 true 2 wit inspect 5.5   260  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i true 2 wit inspect 6.8 410 55 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 true 2 wit inspect 5.4   250  
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.6 290 32 timeout 0 wit inspect 92    2200 true -32 wit inspect 4.4   220   unknown 0 wit inspect 3.0  180 true -32 wit inspect .67   19    - wit inspect - wit inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i true 2 wit inspect 3.5 270 32 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 true 2 wit inspect 8.7   330  
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect 5.3 290 52 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 640    7000 true 2 wit inspect 8.5   320  
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 2 wit inspect 98   4000 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 15     500  
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i true 1 wit inspect 12   610 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 false(unreach-call) -16 wit inspect 10     360  
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i true 2 wit inspect 17   730 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0  290 true 2 wit inspect 10     420  
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4100 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.8
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .49 41 error (2) 0 wit inspect .019 5.0
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4100 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .019 4.8
loop-invgen/heapsort_true-unreach-call_true-termination.i true 2 wit inspect 60   2900 620 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 true 2 wit inspect 68     710  
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 3.2 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  270 true 2 wit inspect 6.4   260  
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 4.2 280 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 true 2 wit inspect 9.6   350  
loop-invgen/nest-if3_true-unreach-call_true-termination.i true 2 wit inspect 4.6 280 46 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3500 true 2 wit inspect 5.2   260  
loop-invgen/nested6_true-unreach-call_true-termination.i true 2 wit inspect 120   4100 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 10     390  
loop-invgen/nested9_true-unreach-call_true-termination.i true 2 wit inspect 10   460 83 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 true 2 wit inspect 12     460  
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i true 2 wit inspect 14   600 99 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    7000 true 2 wit inspect 18     560  
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4000 10000 - 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
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4100 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .024 4.8
loop-invgen/up_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .018 4.8
loop-lit/afnp2014_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   4000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .025 5.0
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i true 1 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    650 false(unreach-call) -16 wit inspect 4.8   230  
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 true 2 wit inspect 7.8   320  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 3.2 270 29 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 8.8   320  
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect 4.3 280 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  270 true 2 wit inspect 6.9   260  
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 3.2 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 false(unreach-call) -16 wit inspect 5.9   320  
loop-lit/ddlm2013_true-unreach-call.i true 2 wit inspect 270   4000 2800 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 12     500  
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect 100   3600 1000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 40    600 true 2 wit inspect 88     1300  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i true 2 wit inspect 24   890 160 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 true 2 wit inspect 11     310  
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect 66   2300 720 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 53    910 true 2 wit inspect 110     1700  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i true 1 wit inspect 3.5 270 30 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1200 false(unreach-call) -16 wit inspect 4.8   240  
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 wit inspect 3.4 270 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.0   280  
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4600 true 2 wit inspect 9.3   280  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 4.0 290 32 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 true 2 wit inspect 7.8   290  
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i false(unreach-call) -16 wit inspect 5.2 300 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 true 2 wit inspect 5.2   240  
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 89   4300 760 timeout 0 wit inspect 92    2200 true -32 wit inspect 5.6   230   unknown 0 wit inspect 3.1  190 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
loop-new/count_by_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4200 8500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .020