Tool ULTIMATE Kojak 0.1.23-3204b741 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-12-02 02:33:02 CET 2017-12-03 03:22:18 CET 2017-12-03 03:55:21 CET 2017-12-03 04:22:06 CET 2017-12-03 04:36:43 CET 2017-12-03 00:36:56 CET 2017-12-03 03:32:10 CET
Run set ukojak.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Loops
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/ukojak.2017-12-02_0233.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 4.7 280 43 false(unreach-call) 1 wit inspect 4.3  280 false(unreach-call) 1 wit inspect 6.3   260   unknown 0 wit inspect 3.3  190 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/bubble_sort_false-unreach-call.i error (7) 0 wit inspect 7.8 230 70 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.2 250 35 false(unreach-call) 1 wit inspect 3.0  250 false(unreach-call) 1 wit inspect 5.3   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 94   2000 1200 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 36     770   unknown 0 wit inspect 4.2  210 true -32 wit inspect .80   19    - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.1 420 58 false(unreach-call) 1 wit inspect 2.3  260 false(unreach-call) 1 wit inspect 5.3   250   unknown 0 wit inspect 3.6  180 true -32 wit inspect .75   18    - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i timeout 0 wit inspect 900   680 12000 error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 13   580 110 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 3.9  210 true -32 wit inspect .59   18    - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i timeout 0 wit inspect 900   4500 7100 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.2  48 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i timeout 0 wit inspect 900   3400 12000 error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.9 370 51 timeout 0 wit inspect 92    1900 false(unreach-call) 1 wit inspect 4.4   270   unknown 0 wit inspect 3.0  210 true -32 wit inspect 10      18    - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i timeout 0 wit inspect 900   4700 12000 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .76 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 4.6 250 35 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.5   260   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .80   18    - wit inspect - wit inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.9 280 37 false(unreach-call) 1 wit inspect 4.1  260 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
loops/s3_false-unreach-call.i error (7) 0 wit inspect 400   3300 4800 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .91 47 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 17   520 140 false(unreach-call) 1 wit inspect 3.6  270 false(unreach-call) 1 wit inspect 12     300   unknown 0 wit inspect 3.9  210 true -32 wit inspect .69   19    - wit inspect - wit inspect
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.5 460 72 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 6.0   270   unknown 0 wit inspect 3.0  190 true -32 wit inspect .69   19    - wit inspect - wit inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.5 470 60 false(unreach-call) 1 wit inspect 3.3  270 false(unreach-call) 1 wit inspect 7.1   270   unknown 0 wit inspect 3.2  210 true -32 wit inspect .71   18    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 10   500 96 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 9.3   350   unknown 0 wit inspect 3.8  190 true -32 wit inspect .68   19    - wit inspect - wit inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 21   720 200 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 17     940   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.9 380 59 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.7   270   unknown 0 wit inspect 3.2  180 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect 6.9 340 54 timeout 0 wit inspect 91    2000 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 2.9  180 true -32 wit inspect .75   18    - wit inspect - wit inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.7 260 39 true -32 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .75   18    - wit inspect - wit inspect
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.4 260 37 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 3.5  180 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.4 260 33 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.9   260   unknown 0 wit inspect 2.1  180 true -32 wit inspect .72   18    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.6 250 42 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.9   260   unknown 0 wit inspect 3.1  210 true -32 wit inspect .64   18    - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.2 260 38 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.8   260   unknown 0 wit inspect 3.5  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.5 350 59 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.7   260   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .75   18    - wit inspect - wit inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.4 340 50 true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 6.8   250   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 8.9 470 74 false(unreach-call) 1 wit inspect 4.1  270 false(unreach-call) 1 wit inspect 14     520   unknown 0 wit inspect 4.0  210 error (2) 0 wit inspect .58   19    - wit inspect - wit inspect
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect 41   990 400 false(unreach-call) 1 wit inspect 4.2  290 timeout 0 wit inspect 97     810   unknown 0 wit inspect 3.3  210 true -32 wit inspect .78   19    - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.5 250 36 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 3.5   230   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .75   18    - wit inspect - wit inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 5.4 310 46 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  280 true 2 wit inspect 7.4   280  
loops/bubble_sort_true-unreach-call_true-termination.i true 2 wit inspect 5.1 270 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 true 2 wit inspect 5.2   230  
loops/count_up_down_true-unreach-call_true-termination.i true 2 wit inspect 5.6 310 52 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 44     500  
loops/eureka_01_true-unreach-call.i timeout 0 wit inspect 900   4600 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .019 5.0
loops/eureka_05_true-unreach-call_true-termination.i true 1 wit inspect 160   2600 2600 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 53    990 false(unreach-call) -16 wit inspect 8.2   310  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 5.4 300 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  270 true 2 wit inspect 5.8   260  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 5.1 290 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 true 2 wit inspect 5.9   260  
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900   890 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 130   1500 1600 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 160    1200 true 2 wit inspect 130     1300  
loops/linear_sea.ch_true-unreach-call.i timeout 0 wit inspect 900   1000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .020 4.9
loops/lu.cmp_true-unreach-call.i timeout 0 wit inspect 900   3900 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 8.7 470 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  290 true 2 wit inspect 12     510  
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect 7.0 410 57 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  290 true 2 wit inspect 7.6   350  
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 7.6 490 58 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 6.2   300  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 7.8 480 63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  270 true 2 wit inspect 6.2   300  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 6.9 390 55 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    460 true 2 wit inspect 10     390  
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 6.3 370 51 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    7000 true 2 wit inspect 8.4   310  
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect 5.1 270 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  270 true 2 wit inspect 5.6   260  
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 8.9 470 78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  280 true 2 wit inspect 9.7   430  
loops/sum_array_true-unreach-call.i timeout 0 wit inspect 900   990 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.8
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 5.2 290 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  270 true 2 wit inspect 6.1   260  
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect 4.7 260 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.7  270 true 2 wit inspect 5.5   260  
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 4.8 270 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27    1000 true 2 wit inspect 5.4   260  
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 4.4 260 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  270 true 2 wit inspect 5.3   260  
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect 4.9 280 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  270 true 2 wit inspect 5.6   250  
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect 5.0 280 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  280 true 2 wit inspect 3.9   270  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect 6.9 460 58 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 true 2 wit inspect 7.8   300  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 5.9 320 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    390 true 2 wit inspect 6.7   270  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 4.8 250 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 true 2 wit inspect 3.7   270  
loops/vogal_true-unreach-call.i timeout 0 wit inspect 900   1700 11000 - 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/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 4.2 260 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 5.8   260  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 4.3 260 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  260 true 2 wit inspect 5.1   260  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect 4.6 260 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 4.9   250  
loop-acceleration/array_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   5000 12000 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0019 .30 - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call2_true-termination.i timeout 0 wit inspect 900   4700 14000 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .026 4.8 error (invalid witness file) 0 wit inspect .89 50 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 0 wit inspect 900   4700 12000 error (invalid witness file) 0 wit inspect .63 46 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i timeout 0 wit inspect 900   3900 11000 error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0015 .30 - wit inspect - wit inspect
loop-acceleration/diamond_false-unreach-call1.i timeout 0 wit inspect 900   710 10000 error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0018 .27 - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   4700 12000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .026 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect - wit inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 4.2 240 37 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 3.3   250   unknown 0 wit inspect 3.1  180 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900   4300 12000 error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .027 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i timeout 0 wit inspect 900   9600 12000 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect 4.4 250 37 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 5.0   260   unknown 0 wit inspect 3.5  190 true -32 wit inspect .71   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call1.i timeout 0 wit inspect 900   2300 12000 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 4.2 250 36 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 5.5   240   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .84   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect 4.5 250 35 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 3.4  180 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call4.i timeout 0 wit inspect 900   2900 10000 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 6.8 380 59 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 9.2   350   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .78   19    - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 7.0 380 57 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 7.1   360   unknown 0 wit inspect 3.6  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loop-acceleration/array_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 45 error (2) 0 wit inspect .018 4.8
loop-acceleration/array_true-unreach-call2_true-termination.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 4.9
loop-acceleration/array_true-unreach-call3_true-termination.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .020 5.0
loop-acceleration/array_true-unreach-call4_true-termination.i timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .019 4.8
loop-acceleration/const_true-unreach-call1.i timeout 0 wit inspect 900   2800 12000 - 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/diamond_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   600 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 4.9
loop-acceleration/diamond_true-unreach-call2.i timeout 0 wit inspect 900   4700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.8
loop-acceleration/functions_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   4700 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.8
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 4.5 260 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 800    6200 true 2 wit inspect 5.5   260  
loop-acceleration/nested_true-unreach-call1.i timeout 0 wit inspect 900   4600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 4.8
loop-acceleration/overflow_true-unreach-call1.i timeout 0 wit inspect 900   2400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 5.0
loop-acceleration/phases_true-unreach-call1.i timeout 0 wit inspect 900   8700 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 5.0
loop-acceleration/phases_true-unreach-call2_false-termination.i true 2 wit inspect 9.6 270 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    410 true 2 wit inspect 7.6   260  
loop-acceleration/simple_true-unreach-call1.i timeout 0 wit inspect 900   2800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .017 5.0
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 4.5 260 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 5.0   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i timeout 0 wit inspect 900   2100 12000 - 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-acceleration/simple_true-unreach-call4.i timeout 0 wit inspect 900   2600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.8
loop-acceleration/underapprox_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   490 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .017 4.8
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 7.3 440 61 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  270 true 2 wit inspect 9.6   410  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 1 wit inspect 4.4 260 36 true -32 wit inspect 4.3  260 false(unreach-call) 1 wit inspect 7.3   320   unknown 0 wit inspect 3.2  210 true -32 wit inspect .79   18    - wit inspect - wit inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   2800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .023 4.9
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i timeout 0 wit inspect 900   2000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .81 43 error (2) 0 wit inspect .018 4.9
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i timeout 0 wit inspect 900   2300 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .020 5.0
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i timeout 0 wit inspect 900   3200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .024 4.8
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true 2 wit inspect 5.6 310 50 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  280 true 2 wit inspect 6.4   270  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i timeout 0 wit inspect 900   1700 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 45 error (2) 0 wit inspect .018 4.9
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.5 380 55 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 4.8   260   unknown 0 wit inspect 2.9  180 true -32 wit inspect .64   18    - wit inspect - wit inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i true 2 wit inspect 8.4 470 67 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 true 2 wit inspect 8.6   340  
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect 8.2 480 72 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 620    7000 true 2 wit inspect 8.9   350  
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 2 wit inspect 22   830 230 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 13     500  
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i true 2 wit inspect 19   710 180 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 true 2 wit inspect 12     510  
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i true 2 wit inspect 12   490 82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.0  300 true 2 wit inspect 10     440  
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5300 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5300 12000 - 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/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4700 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .025 4.8
loop-invgen/heapsort_true-unreach-call_true-termination.i true 2 wit inspect 91   1800 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 true 2 wit inspect 66     860  
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 7.0 450 61 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  290 true 2 wit inspect 7.1   270  
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 7.5 460 59 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  280 true 2 wit inspect 10     450  
loop-invgen/nest-if3_true-unreach-call_true-termination.i true 2 wit inspect 9.4 510 82 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 true 2 wit inspect 7.1   260  
loop-invgen/nested6_true-unreach-call_true-termination.i true 2 wit inspect 9.5 490 75 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 true 2 wit inspect 11     380  
loop-invgen/nested9_true-unreach-call_true-termination.i true 2 wit inspect 18   680 180 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 true 2 wit inspect 17     500  
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i true 2 wit inspect 21   710 230 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 650    7000 true 2 wit inspect 14     570  
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5300 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .77 43 error (2) 0 wit inspect .022 4.8
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i timeout 0 wit inspect 900   6000 13000 - 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/up_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5300 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .018 4.9
loop-lit/afnp2014_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   5200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 4.8
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i true 2 wit inspect 5.8 340 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    650 true 2 wit inspect 8.9   410  
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect 7.2 460 62 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  280 true 2 wit inspect 8.5   320  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 6.0 340 45 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 9.0   290  
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect 6.4 370 57 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  290 true 2 wit inspect 7.8   280  
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 5.6 320 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  270 true 2 wit inspect 6.2   260  
loop-lit/ddlm2013_true-unreach-call.i timeout 0 wit inspect 900   5600 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .022 4.9
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect 240   3200 3100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    420 true 2 wit inspect 93     1200  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i true 2 wit inspect 6.9 470 57 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2400 true 2 wit inspect 8.8   310  
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect 880   5300 12000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    450 true 2 wit inspect 56     1400  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i true 2 wit inspect 6.4 420 49 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1400 true 2 wit inspect 6.4   270  
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 wit inspect 5.7 310 46 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 5.7   260  
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect 5.6 320 47 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 6.4   260  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 5.7 330 49 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 true 2 wit inspect 6.3   260  
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   2800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 5.0
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 4.5 260 38 false(unreach-call) 1 wit inspect 3.6  280 false(unreach-call) 1 wit inspect 5.5   250   unknown 0 wit inspect 3.4  180 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
loop-new/count_by_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect 5.8 350 45 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 true 2 wit inspect 7.6   290  
loop-new/count_by_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54