Tool ULTIMATE Taipan 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]
Date of execution 2017-12-02 17:23:13 CET 2017-12-03 07:22:17 CET 2017-12-03 07:45:29 CET 2017-12-03 07:47:53 CET 2017-12-03 07:50:34 CET 2017-12-03 06:47:45 CET 2017-12-03 07:25:40 CET
Run set utaipan.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-Loops
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/utaipan.2017-12-02_1723.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.9 270 39 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.8   260   unknown 0 wit inspect 2.6  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
loops/bubble_sort_false-unreach-call.i error (7) 0 wit inspect 7.7 240 58 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .046 4.8 error (invalid witness file) 0 wit inspect .83 50 error (invalid witness file) 0 wit inspect .0042 .30 - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.4 270 38 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.8   240   unknown 0 wit inspect 2.6  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 130   1500 1600 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 34     780   unknown 0 wit inspect 3.2  210 true -32 wit inspect .61   19    - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.5 320 50 timeout 0 wit inspect 92    2300 false(unreach-call) 1 wit inspect 5.3   270   unknown 0 wit inspect 2.7  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i timeout 0 wit inspect 900   1700 9800 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0041 .35 - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 15   670 150 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 5.3   270   unknown 0 wit inspect 2.9  190 true -32 wit inspect .58   19    - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i timeout 0 wit inspect 900   2200 11000 error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .027 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0045 .26 - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i timeout 0 wit inspect 900   4200 12000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.5 280 40 timeout 0 wit inspect 92    1900 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 2.8  210 true -32 wit inspect 23      18    - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i timeout 0 wit inspect 900   4800 13000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .047 5.0 error (invalid witness file) 0 wit inspect .80 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 4.5 270 39 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 6.2   320   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.9 280 35 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/s3_false-unreach-call.i false(unreach-call) 1 wit inspect 170   950 1900 true -32 wit inspect 5.1  270 false(unreach-call) 1 wit inspect 53     590   unknown 0 wit inspect 3.8  220 error (2) 0 wit inspect .75   20    - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 18   490 140 false(unreach-call) 1 wit inspect 3.4  270 false(unreach-call) 1 wit inspect 11     300   unknown 0 wit inspect 2.9  210 true -32 wit inspect .61   19    - wit inspect - wit inspect
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 13   590 120 false(unreach-call) 1 wit inspect 3.3  270 false(unreach-call) 1 wit inspect 6.5   270   unknown 0 wit inspect 2.8  180 true -32 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 9.4 540 78 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.5   280   unknown 0 wit inspect 2.7  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 13   600 110 false(unreach-call) 1 wit inspect 3.6  270 false(unreach-call) 1 wit inspect 6.7   350   unknown 0 wit inspect 2.7  180 true -32 wit inspect .61   19    - wit inspect - wit inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 540   670 6500 true -32 wit inspect 3.2  250 false(unreach-call) 1 wit inspect 13     1000   unknown 0 wit inspect 2.8  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 8.4 470 67 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.1   270   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect 5.8 290 46 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 2.8  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.9 290 40 true -32 wit inspect 3.8  250 false(unreach-call) 1 wit inspect 4.7   260   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.5 270 35 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 2.9  190 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 4.8 290 43 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 5.0   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.6 280 40 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 2.7  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.4 270 40 false(unreach-call) 1 wit inspect 2.8  260 false(unreach-call) 1 wit inspect 4.8   260   unknown 0 wit inspect 2.7  180 true -32 wit inspect .62   18    - wit inspect - wit inspect
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.5 270 41 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 5.0   260   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 8.8 540 73 true -32 wit inspect 2.8  260 false(unreach-call) 1 wit inspect 5.5   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 46   2600 430 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 14     490   unknown 0 wit inspect 2.9  210 error (2) 0 wit inspect .60   19    - wit inspect - wit inspect
loops/vogal_false-unreach-call.i timeout 0 wit inspect 900   4600 13000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .81 50 error (invalid witness file) 0 wit inspect .0019 .26 - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.6 270 36 true -32 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 5.0   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 8.6 490 82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  270 true 2 wit inspect 7.5   270  
loops/bubble_sort_true-unreach-call_true-termination.i true 2 wit inspect 4.5 250 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 true 2 wit inspect 5.1   250  
loops/count_up_down_true-unreach-call_true-termination.i true 1 wit inspect 17   470 200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5200 timeout 0 wit inspect 960     660  
loops/eureka_01_true-unreach-call.i timeout 0 wit inspect 900   1100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 4.8
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect 130   1400 1700 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6700 true 2 wit inspect 51     810  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 4.5 280 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  270 true 2 wit inspect 4.9   260  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 4.8 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  270 true 2 wit inspect 5.2   260  
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .043 5.0
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect 250   980 3300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 55    640 true 2 wit inspect 75     830  
loops/linear_sea.ch_true-unreach-call.i timeout 0 wit inspect 900   1800 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .048 4.8
loops/lu.cmp_true-unreach-call.i timeout 0 wit inspect 900   3700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .025 4.8
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 14   620 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  280 true 2 wit inspect 13     520  
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect 8.5 490 66 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  270 true 2 wit inspect 7.6   300  
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 6.5 370 53 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  270 true 2 wit inspect 6.6   350  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 6.9 370 52 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 6.5   340  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 11   540 92 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  370 true 2 wit inspect 10     420  
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 8.5 510 75 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    7000 true 2 wit inspect 7.6   300  
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect 4.8 290 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 5.3   260  
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 9.8 530 82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  270 true 2 wit inspect 8.5   390  
loops/sum_array_true-unreach-call.i timeout 0 wit inspect 900   1600 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 44 error (2) 0 wit inspect .017 4.9
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 5.6 290 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 6.7   260  
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect 5.0 290 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 5.7   260  
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 4.9 280 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 31    1100 true 2 wit inspect 5.1   260  
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 4.9 280 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 5.1   260  
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect 4.7 270 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 true 2 wit inspect 5.4   260  
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect 5.0 280 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 5.5   260  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 1 wit inspect 9.8 540 75 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 error (7) 0 wit inspect 7.4   200  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 6.3 290 52 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6  300 true 2 wit inspect 6.9   280  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 5.0 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  270 true 2 wit inspect 5.0   260  
loops/vogal_true-unreach-call.i timeout 0 wit inspect 900   4600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 5.0
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 4.7 280 38 - wit inspect - wit inspect - wit inspect - wit inspect out of java memory 0 wit inspect 500    5200 true 2 wit inspect 5.5   270  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 4.7 280 38 - wit inspect - wit inspect - wit inspect - wit inspect out of java memory 0 wit inspect 470    5200 true 2 wit inspect 5.2   260  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect 4.8 280 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  270 true 2 wit inspect 5.5   260  
loop-acceleration/array_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   980 11000 error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .048 5.0 error (invalid witness file) 0 wit inspect .83 51 error (invalid witness file) 0 wit inspect .0040 .30 - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call2_true-termination.i timeout 0 wit inspect 900   1000 12000 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .040 5.0 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 0 wit inspect 900   990 10000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .048 4.9 error (invalid witness file) 0 wit inspect .90 47 error (invalid witness file) 0 wit inspect .0034 .34 - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i timeout 0 wit inspect 900   710 11000 error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .031 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0028 .34 - wit inspect - wit inspect
loop-acceleration/diamond_false-unreach-call1.i timeout 0 wit inspect 900   750 11000 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   790 13000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0038 .35 - wit inspect - wit inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 4.5 270 40 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.7   240   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900   1200 11000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .91 49 error (invalid witness file) 0 wit inspect .0036 .34 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i timeout 0 wit inspect 900   620 10000 error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .050 4.9 error (invalid witness file) 0 wit inspect .88 47 error (invalid witness file) 0 wit inspect .0035 .31 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect 4.5 270 39 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 4.6   250   unknown 0 wit inspect 2.7  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call1.i timeout 0 wit inspect 900   660 11000 error (invalid witness file) 0 wit inspect .53 45 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .82 51 error (invalid witness file) 0 wit inspect .0041 .31 - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 4.5 260 40 false(unreach-call) 1 wit inspect 2.8  260 false(unreach-call) 1 wit inspect 4.2   240   unknown 0 wit inspect 2.6  210 false(unreach-call) 1 wit inspect .81   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect 4.5 270 38 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 4.6   250   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call4.i timeout 0 wit inspect 900   810 13000 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .035 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 8.7 570 76 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 7.8   350   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 7.8 470 76 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 7.9   350   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 6.7 340 55 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  270 true 2 wit inspect 6.7   280  
loop-acceleration/array_true-unreach-call2_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 .54 44 error (2) 0 wit inspect .028 4.9
loop-acceleration/array_true-unreach-call3_true-termination.i true 2 wit inspect 6.2 290 45 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  280 true 2 wit inspect 6.9   260  
loop-acceleration/array_true-unreach-call4_true-termination.i timeout 0 wit inspect 900   1100 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 5.6 300 45 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  270 true 2 wit inspect 5.3   260  
loop-acceleration/diamond_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   710 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .052 4.9
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect 130   720 1400 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  280 timeout 0 wit inspect 960     4500  
loop-acceleration/functions_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .051 4.9
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 4.9 280 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 760    6100 true 2 wit inspect 6.0   260  
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect 41   560 440 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0  290 true 2 wit inspect 78     550  
loop-acceleration/overflow_true-unreach-call1.i true 1 wit inspect 5.6 280 49 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 770    7000 timeout 0 wit inspect 960     530  
loop-acceleration/phases_true-unreach-call1.i timeout 0 wit inspect 900   760 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .020 4.9
loop-acceleration/phases_true-unreach-call2_false-termination.i true 2 wit inspect 11   440 88 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    400 true 2 wit inspect 7.5   270  
loop-acceleration/simple_true-unreach-call1.i true 2 wit inspect 6.0 290 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 9.4   330  
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 4.6 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 4.8   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i true 2 wit inspect 6.7 310 53 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 true 2 wit inspect 8.9   280  
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect 6.3 290 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  280 timeout 0 wit inspect 960     600  
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 130   570 1800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  270 true 2 wit inspect 59     440  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 6.9 360 53 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 11     380  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 1 wit inspect 4.6 270 37 true -32 wit inspect 3.4  280 false(unreach-call) 1 wit inspect 4.2   240   unknown 0 wit inspect 2.7  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   810 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .031 4.8
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i timeout 0 wit inspect 900   830 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .025 4.9
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i timeout 0 wit inspect 900   790 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .017 4.9
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i true 1 wit inspect 69   550 880 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 false(unreach-call) -16 wit inspect 7.5   280  
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true 2 wit inspect 4.8 280 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  280 true 2 wit inspect 5.3   260  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i true 2 wit inspect 5.0 290 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 5.6   260  
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.8 330 51 timeout 0 wit inspect 92    2200 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 2.8  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i true 2 wit inspect 8.2 480 75 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 true 2 wit inspect 9.7   410  
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect 9.1 490 78 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 9.2   370  
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 2 wit inspect 86   2000 810 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 160     1500  
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i true 2 wit inspect 37   870 330 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 true 2 wit inspect 14     490  
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i true 2 wit inspect 9.7 550 91 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6  290 false(unreach-call) -16 wit inspect 4.8   260  
loop-invgen/down_true-unreach-call_true-termination.i true 1 wit inspect 7.7 390 60 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 300    7000 timeout 0 wit inspect 960     2100  
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   3000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.8
loop-invgen/heapsort_true-unreach-call_true-termination.i error (7) 0 wit inspect 460   1300 4800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .040 4.8
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 8.4 420 64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  280 true 2 wit inspect 14     550  
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 16   720 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  280 true 2 wit inspect 14     500  
loop-invgen/nest-if3_true-unreach-call_true-termination.i true 2 wit inspect 4.9 280 41 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 true 2 wit inspect 6.5   260  
loop-invgen/nested6_true-unreach-call_true-termination.i true 2 wit inspect 43   950 480 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 true 2 wit inspect 15     570  
loop-invgen/nested9_true-unreach-call_true-termination.i true 2 wit inspect 11   550 81 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3200 true 2 wit inspect 13     500  
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i true 1 wit inspect 27   840 230 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 610    7000 false(unreach-call) -16 wit inspect 5.0   260  
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.9
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i true 1 wit inspect 8.3 430 63 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 320    7000 timeout 0 wit inspect 960     4800  
loop-invgen/up_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5100 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 wit inspect 6.5 340 54 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 520    7000 true 2 wit inspect 6.2   260  
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i true 2 wit inspect 10   530 93 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    660 true 2 wit inspect 7.0   280  
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect 7.2 420 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  270 true 2 wit inspect 9.1   360  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 7.6 420 70 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 7.9   300  
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect 7.6 390 62 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  270 true 2 wit inspect 8.2   310  
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 4.9 290 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 6.0   270  
loop-lit/ddlm2013_true-unreach-call.i true 2 wit inspect 17   530 180 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 12     490  
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect 100   1400 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  280 true 2 wit inspect 22     650  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i true 2 wit inspect 9.6 520 76 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 true 2 wit inspect 12     490  
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect 180   2400 2200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.9  440 true 2 wit inspect 52     1500  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i true 2 wit inspect 6.1 310 47 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1300 true 2 wit inspect 6.4   270  
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 wit inspect 6.9 350 57 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 true 2 wit inspect 7.6   260  
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect 7.3 350 59 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4600 true 2 wit inspect 5.9   260  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 7.3 400 57 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 6.1   260  
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   860 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.8
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 4.5 280 35 false(unreach-call) 1 wit inspect 3.1  270 false(unreach-call) 1 wit inspect 4.6   250   unknown 0 wit inspect 2.7  180 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 5.3 290 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  270 true 2 wit inspect 5.6   260  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect 5.5 300 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  270 true 2 wit inspect 6.9   280  
loop-new/count_by_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   2600