Tool CBMC 5.8 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:26:01 CET 2017-12-01 07:56:00 CET 2017-12-01 08:08:00 CET 2017-12-01 08:15:34 CET 2017-12-01 04:22:29 CET 2017-12-01 07:31:28 CET
Run set cbmc.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Loops
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cbmc.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 .22 33 2.4 true -32 wit inspect 3.0  250 false(unreach-call) 1 wit inspect 6.6   260   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
loops/bubble_sort_false-unreach-call.i false(unreach-call) 0 wit inspect 2.1  200 24   true -32 wit inspect 4.8  270 error (7) 0 wit inspect 8.0   210   unknown 0 wit inspect 4.1  260 error (2) 0 wit inspect .99   19    - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .22 33 2.2 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 4.9   240   unknown 0 wit inspect 3.6  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .89 36 8.3 false(unreach-call) 1 wit inspect 5.3  280 false(unreach-call) 1 wit inspect 30     710   unknown 0 wit inspect 3.7  220 error (2) 0 wit inspect .61   18    - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .26 33 2.0 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.7   260   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.8  190 19   false(unreach-call) 1 wit inspect 4.1  280 false(unreach-call) 1 wit inspect 9.7   410   unknown 0 wit inspect 4.3  210 true -32 wit inspect .64   19    - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .77 41 8.2 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 5.9   270   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i false(unreach-call) 1 wit inspect 1.9  35 26   true -32 wit inspect 4.5  260 false(unreach-call) 1 wit inspect 17     480   unknown 0 wit inspect 3.6  220 error (2) 0 wit inspect .58   18    - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 0 wit inspect 2.6  130 35   true -32 wit inspect 8.1  410 timeout 0 wit inspect 97     4500   unknown 0 wit inspect 7.8  320 error (2) 0 wit inspect 40      62    - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .28 35 2.5 false(unreach-call) 1 wit inspect 4.4  270 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 3.7  210 error (2) 0 wit inspect .61   18    - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i error (134) 0 wit inspect 680    14000 3800   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .25 33 1.9 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 3.6  180 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .41 50 3.9 false(unreach-call) 1 wit inspect 4.8  270 false(unreach-call) 1 wit inspect 5.7   260   unknown 0 wit inspect 3.8  210 error (2) 0 wit inspect .85   18    - wit inspect - wit inspect
loops/s3_false-unreach-call.i false(unreach-call) 1 wit inspect 21    770 240   false(unreach-call) 1 wit inspect 8.4  280 false(unreach-call) 1 wit inspect 68     620   unknown 0 wit inspect 7.9  330 error (2) 0 wit inspect .80   20    - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .64 33 7.3 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 15     320   unknown 0 wit inspect 3.6  210 true -32 wit inspect .75   18    - wit inspect - wit inspect
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.0  33 10   false(unreach-call) 1 wit inspect 4.1  260 false(unreach-call) 1 wit inspect 7.1   270   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .61 35 6.5 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 6.7   280   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.0  33 9.3 true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 8.6   290   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.0  33 8.5 true -32 wit inspect 2.4  260 false(unreach-call) 1 wit inspect 11     470   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .99 33 9.3 true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 6.7   270   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect .26 33 2.4 false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 7.5   260   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .25 33 2.3 false(unreach-call) 1 wit inspect 2.0  260 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 3.2  190 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .25 33 2.0 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 5.0   250   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .25 33 2.1 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 5.2   250   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .24 33 2.1 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 6.0   260   unknown 0 wit inspect 3.7  210 true -32 wit inspect .68   18    - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .22 33 2.0 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.2   250   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .24 33 2.1 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.1   250   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .78   18    - wit inspect - wit inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .66 33 6.1 unknown 0 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.7   260   unknown 0 wit inspect 3.3  230 error (2) 0 wit inspect .58   18    - wit inspect - wit inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .71 34 6.3 timeout 0 wit inspect 91    1400 false(unreach-call) 1 wit inspect 15     510   unknown 0 wit inspect 3.2  210 error (2) 0 wit inspect .60   18    - wit inspect - wit inspect
loops/vogal_false-unreach-call.i false(unreach-call) 0 wit inspect 1.2  38 12   true -32 wit inspect 6.2  280 timeout 0 wit inspect 97     2300   unknown 0 wit inspect 7.8  270 true -32 wit inspect .74   21    - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .23 33 2.4 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.8   230   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect .41 33 4.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  280 true 2 wit inspect 7.4   280  
loops/bubble_sort_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    15000 5400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .019 4.8
loops/count_up_down_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    5100 3600   - 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
loops/eureka_01_true-unreach-call.i true 1 wit inspect 2.3  35 22   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4600 timeout 0 wit inspect 960     1500  
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect .80 33 7.9 - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 6.1  280 true 2 wit inspect 50     740  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i out of memory 0 wit inspect 420    15000 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .020 5.0
loops/for_infinite_loop_2_true-unreach-call_false-termination.i out of memory 0 wit inspect 420    15000 6100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .020 4.8
loops/insertion_sort_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    2200 5500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .027 4.8
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .77 33 8.8 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 520    3600 true 2 wit inspect 150     750  
loops/linear_sea.ch_true-unreach-call.i error (6) 0 wit inspect 790    8400 3500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .020 4.9
loops/lu.cmp_true-unreach-call.i true 1 wit inspect 2.3  51 31   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 100    2700 timeout 0 wit inspect 960     4500  
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect .42 33 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2  300 true 2 wit inspect 10     380  
loops/n.c11_true-unreach-call_false-termination.i error (42) 0 wit inspect 870    2900 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .047 4.9
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .41 33 3.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 6.6   340  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .40 33 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 6.8   350  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 1.3  34 12   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 99    1700 true 2 wit inspect 7.0   390  
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 22    130 300   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 21    550 true 2 wit inspect 15     390  
loops/sum03_true-unreach-call_false-termination.i out of memory 0 wit inspect 460    15000 5800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.9
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 1.1  33 10   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.1  260 true 2 wit inspect 10     430  
loops/sum_array_true-unreach-call.i error (42) 0 wit inspect 870    1500 4100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .021 5.0
loops/terminator_02_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    350 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .051 4.9
loops/terminator_03_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    510 8400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 45 error (2) 0 wit inspect .019 4.9
loops/trex01_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    4400 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .020 4.9
loops/trex02_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    1300 8300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .042 5.0
loops/trex03_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    840 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .019 4.9
loops/trex04_true-unreach-call_false-termination.i error (42) 0 wit inspect 870    2700 5800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .024 4.9
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect .78 33 7.1 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 7.7   290  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 2.5  44 30   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5700 true 2 wit inspect 11     330  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 1.1  33 13   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    380 true 2 wit inspect 5.8   260  
loops/vogal_true-unreach-call.i true 2 wit inspect .84 33 7.3 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2300 true 2 wit inspect 240     1200  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i out of memory 0 wit inspect 410    15000 4600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .047 4.8
loops/while_infinite_loop_2_true-unreach-call_false-termination.i out of memory 0 wit inspect 410    15000 4200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .018 4.9
loops/while_infinite_loop_3_true-unreach-call_false-termination.i out of memory 0 wit inspect 430    15000 6400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .020 5.0
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 0 wit inspect 22    1800 280   timeout 0 wit inspect 93    3300 out of memory 0 wit inspect 73     7000   unknown 0 wit inspect 80    3100 timeout 0 wit inspect 96      74    - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 0 wit inspect 45    3700 510   timeout 0 wit inspect 97    4500 out of memory 0 wit inspect 72     7000   timeout 0 wit inspect 97    4600 timeout 0 wit inspect 96      150    - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 wit inspect 21    1000 240   timeout 0 wit inspect 93    3300 out of memory 0 wit inspect 61     7000   unknown 0 wit inspect 42    2500 timeout 0 wit inspect 96      59    - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect 4.1  34 47   true -32 wit inspect 7.4  570 timeout 0 wit inspect 97     5600   unknown 0 wit inspect 15    590 false(unreach-call) 1 wit inspect 1.2    32    - wit inspect - wit inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 3.0  55 32   true -32 wit inspect 3.4  260 out of memory 0 wit inspect 87     7000   unknown 0 wit inspect 3.8  220 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i out of memory 0 wit inspect 420    15000 5600   error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .99 49 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .23 33 1.9 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.6   240   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i out of memory 0 wit inspect 380    15000 5100   error (invalid witness file) 0 wit inspect .43 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i out of memory 0 wit inspect 360    15000 4600   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .95 50 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect .22 33 2.0 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.2   250   unknown 0 wit inspect 3.1  190 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call1.i out of memory 0 wit inspect 320    15000 4100   error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .23 33 1.9 false(unreach-call) 1 wit inspect 3.4  280 false(unreach-call) 1 wit inspect 6.0   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .21 33 1.9 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.2   240   unknown 0 wit inspect 3.2  180 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call4.i out of memory 0 wit inspect 320    15000 4200   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .97 33 9.3 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 9.8   340   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .96 33 10   true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 8.2   350   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 12    1100 170   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 65    1400 true 2 wit inspect 12     310  
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect 26    2200 330   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 33    1600 timeout 0 wit inspect 960     3900  
loop-acceleration/array_true-unreach-call3_true-termination.i true 2 wit inspect 11    640 130   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 250    5400 true 2 wit inspect 18     370  
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 11    640 140   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6400 out of memory 0 wit inspect 120     7000  
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 3.8  34 40   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 15    590 true 2 wit inspect 11     310  
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 1 wit inspect 3.8  58 39   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 8.8  360 timeout 0 wit inspect 960     670  
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect .88 35 10   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 9.4  350 true 2 wit inspect 78     670  
loop-acceleration/functions_true-unreach-call1_true-termination.i out of memory 0 wit inspect 430    15000 5600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 4.9
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 89    270 1000   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 14    520 true 2 wit inspect 9.5   310  
loop-acceleration/nested_true-unreach-call1.i out of memory 0 wit inspect 380    15000 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 4.8
loop-acceleration/overflow_true-unreach-call1.i out of memory 0 wit inspect 310    15000 4100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 5.0
loop-acceleration/phases_true-unreach-call1.i out of memory 0 wit inspect 360    15000 5200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.8
loop-acceleration/phases_true-unreach-call2_false-termination.i error (42) 0 wit inspect 870    5900 5600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 4.9
loop-acceleration/simple_true-unreach-call1.i out of memory 0 wit inspect 310    15000 3800   - 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
loop-acceleration/simple_true-unreach-call2_true-termination.i error (42) 0 wit inspect 870    3900 6300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.8
loop-acceleration/simple_true-unreach-call3_true-termination.i error (42) 0 wit inspect 870    8100 3000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.9
loop-acceleration/simple_true-unreach-call4.i out of memory 0 wit inspect 320    15000 4700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 1.2  33 11   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.2  260 true 2 wit inspect 82     440  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 1.1  33 11   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.3  270 true 2 wit inspect 6.9   270  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 1 wit inspect 9.8  1100 68   false(unreach-call) 1 wit inspect 3.5  270 false(unreach-call) 1 wit inspect 4.9   240   unknown 0 wit inspect 3.2  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 9.0  580 110   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 timeout 0 wit inspect 960     790  
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i out of memory 0 wit inspect 140    15000 2000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .018 4.8
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i out of memory 0 wit inspect 140    15000 1700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .018 4.9
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i error (134) 0 wit inspect 35    14000 560   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .018 4.9
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i out of memory 0 wit inspect 430    15000 6200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .019 4.9
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i out of memory 0 wit inspect 480    15000 6300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 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 .27 35 2.2 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.0   260   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    200 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .050 4.9
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    11000 4500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .019 4.8
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i error (42) 0 wit inspect 870    470 8600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    480 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .018 4.9
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    690 9800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .020 4.9
loop-invgen/down_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    2600 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    1600 6400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .020 5.0
loop-invgen/half_2_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    1100 6800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .023 4.9
loop-invgen/heapsort_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    12000 7100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .023 4.9
loop-invgen/id_build_true-unreach-call_true-termination.i error (134) 0 wit inspect 380    12000 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect .44 35 3.9 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.8  280 true 2 wit inspect 9.6   350  
loop-invgen/nest-if3_true-unreach-call_true-termination.i error (134) 0 wit inspect 710    13000 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .021 4.9
loop-invgen/nested6_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    500 3600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .023 5.0
loop-invgen/nested9_true-unreach-call_true-termination.i error (134) 0 wit inspect 230    12000 1800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .019 4.8
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    3800 8200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .018 4.8
loop-invgen/seq_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    240 6000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .017 4.9
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    9600 5700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.8
loop-invgen/up_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    1400 9600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .018 4.8
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 wit inspect 17    150 190   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 15    500 true 2 wit inspect 10     310  
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 870    370 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .76 33 7.5 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.4  270 true 2 wit inspect 7.6   310  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 870    2700 4600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .020 4.9
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect 2.8  33 28   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 6.4  280 true 2 wit inspect 8.2   270  
loop-lit/css2003_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 870    900 3800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.8
loop-lit/ddlm2013_true-unreach-call.i error (42) 0 wit inspect 870    1300 9200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 5.0
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect 2.6  33 25   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 810    7000 true 2 wit inspect 110     1400  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 870    2700 6400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .020 4.8
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect 2.7  33 28   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.4  280 true 2 wit inspect 97     1800  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i true 2 wit inspect 220    620 2500   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 21    650 true 2 wit inspect 16     370  
loop-lit/hhk2008_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 870    270 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .024 4.9
loop-lit/jm2006_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 870    5400 4200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .022 4.8
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 870    4200 5000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .018 4.8
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i error (42) 0 wit inspect 870    13000 6800   - 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-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .26 33 1.8 timeout 0 wit inspect 92    2100 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect 120    3400 1400   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    1500 true 2 wit inspect 11     1500  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i out of memory 0 wit inspect 840    15000 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .024 4.9
loop-new/count_by_2_true-unreach-call_true-termination.i true 1 wit inspect 60    1700 680   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000