Tool CPAchecker 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-05 07:52:24 CET 2017-12-05 13:10:09 CET 2017-12-05 13:34:02 CET 2017-12-05 13:37:41 CET 2017-12-05 13:41:35 CET 2017-12-05 12:37:13 CET 2017-12-05 13:13:01 CET
Run set interpchecker.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-Loops
Options -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/interpchecker.2017-12-05_0752.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.6 290 42 true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 4.6   260   unknown 0 wit inspect 2.7  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
loops/bubble_sort_false-unreach-call.i timeout 0 wit inspect 900   4400 12000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0036 .34 - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.8 280 26 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 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 20   830 170 timeout 0 wit inspect 91    1200 true -32 wit inspect 5.4   270   unknown 0 wit inspect 3.1  210 error (1) 0 wit inspect .53   19    - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.2 260 29 timeout 0 wit inspect 92    2300 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 2.8  180 true -32 wit inspect .58   19    - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 420   4100 5000 timeout 0 wit inspect 92    2000 out of memory 0 wit inspect 60     7000   unknown 0 wit inspect 3.7  220 true -32 wit inspect .66   20    - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 520   4500 6600 timeout 0 wit inspect 92    2100 false(unreach-call) 1 wit inspect 8.3   350   unknown 0 wit inspect 2.9  190 true -32 wit inspect .61   19    - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i timeout 0 wit inspect 900   2800 11000 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0032 .29 - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 0 wit inspect 16   650 140 true -32 wit inspect 4.0  260 timeout 0 wit inspect 97     4500   unknown 0 wit inspect 3.0  210 error (2) 0 wit inspect .57   19    - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 44   1900 390 timeout 0 wit inspect 92    1900 false(unreach-call) 1 wit inspect 5.2   270   unknown 0 wit inspect 2.9  210 true -32 wit inspect 6.1    19    - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i timeout 0 wit inspect 900   5100 12000 error (invalid witness file) 0 wit inspect .49 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0046 .26 - wit inspect - wit inspect
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 2.9 270 24 true -32 wit inspect 2.8  260 false(unreach-call) 1 wit inspect 4.7   260   unknown 0 wit inspect 2.6  190 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 3.1 270 31 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 2.8  190 error (2) 0 wit inspect .59   18    - wit inspect - wit inspect
loops/s3_false-unreach-call.i false(unreach-call) 0 wit inspect 86   3500 770 timeout 0 wit inspect 92    1900 true -32 wit inspect 8.4   330   unknown 0 wit inspect 4.2  260 error (1) 0 wit inspect .68   19    - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 6.1 310 54 true -32 wit inspect 4.3  260 out of memory 0 wit inspect 82     7000   unknown 0 wit inspect 3.1  210 true -32 wit inspect .64   19    - wit inspect - wit inspect
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.0 440 57 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 6.9   260   unknown 0 wit inspect 3.0  210 true -32 wit inspect .59   19    - wit inspect - wit inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.6 420 51 timeout 0 wit inspect 92    2100 false(unreach-call) 1 wit inspect 6.2   290   unknown 0 wit inspect 2.9  210 true -32 wit inspect .61   19    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.4 440 56 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 8.0   580   unknown 0 wit inspect 3.1  210 true -32 wit inspect .59   18    - wit inspect - wit inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 10   470 84 false(unreach-call) 1 wit inspect 3.6  270 false(unreach-call) 1 wit inspect 30     3000   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.0 290 45 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.5   330   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect 72   3700 760 timeout 0 wit inspect 91    2000 false(unreach-call) 1 wit inspect 6.5   270   unknown 0 wit inspect 3.0  210 true -32 wit inspect .62   18    - wit inspect - wit inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.8 260 22 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.3   270   unknown 0 wit inspect 2.7  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 2.9 270 27 true -32 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 4.7   260   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.9 280 29 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 2.7  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.7 260 23 true -32 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 5.0   260   unknown 0 wit inspect 2.7  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.7 280 23 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.8   260   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.1 280 31 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.8   260   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.9 270 29 true -32 wit inspect 2.8  250 false(unreach-call) 1 wit inspect 7.8   330   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 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 5.7 300 48 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 16     540   unknown 0 wit inspect 3.2  230 error (2) 0 wit inspect .62   19    - wit inspect - wit inspect
loops/vogal_false-unreach-call.i false(unreach-call) 0 wit inspect 190   2200 2100 true -32 wit inspect 9.5  410 timeout 0 wit inspect 96     2100   unknown 0 wit inspect 4.5  220 true -32 wit inspect .70   23    - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.8 270 25 timeout 0 wit inspect 96    2700 false(unreach-call) 1 wit inspect 4.9   250   timeout 0 wit inspect 97    2700 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 4.5 280 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  270 true 2 wit inspect 8.1   280  
loops/bubble_sort_true-unreach-call_true-termination.i true 2 wit inspect 2.8 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 4.8   230  
loops/count_up_down_true-unreach-call_true-termination.i true 2 wit inspect 4.2 290 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5000 true 2 wit inspect 15     330  
loops/eureka_01_true-unreach-call.i timeout 0 wit inspect 900   4200 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.8
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect 33   1100 250 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 52     840  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 3.0 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 5.1   270  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 2.9 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 4.8   260  
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 4.9
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect 15   640 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 22    520 true 2 wit inspect 160     770  
loops/linear_sea.ch_true-unreach-call.i timeout 0 wit inspect 900   2600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9
loops/lu.cmp_true-unreach-call.i true 1 wit inspect 10   450 75 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5600 timeout 0 wit inspect 960     4300  
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 9.6 450 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  280 true 2 wit inspect 14     390  
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect 4.5 280 37 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 840    7000 true 2 wit inspect 10     340  
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 3.5 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  270 true 2 wit inspect 6.3   350  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 3.5 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  270 true 2 wit inspect 6.3   340  
loops/string_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .017 4.8
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 3.7 270 33 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    7000 true 2 wit inspect 8.6   380  
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect 3.0 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 5.4   260  
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 6.2 420 59 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 9.6   430  
loops/sum_array_true-unreach-call.i timeout 0 wit inspect 900   4500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .019 4.8
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 3.3 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  270 true 2 wit inspect 6.1   260  
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect 3.5 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  270 true 2 wit inspect 5.8   260  
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27    890 true 2 wit inspect 5.4   260  
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 2.8 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 4.8   260  
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect 5.8 300 45 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  270 true 2 wit inspect 5.2   260  
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect 3.1 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 true 2 wit inspect 5.2   260  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 1 wit inspect 2.9 270 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 false(unreach-call) -16 wit inspect 4.9   250  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 4.4 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  380 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 7.0 420 57 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 5.0   260  
loops/vogal_true-unreach-call.i timeout 0 wit inspect 900   4000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .023 4.8
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 true 2 wit inspect 5.0   250  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 2.9 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 5.1   250  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect 3.0 280 27 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5200 true 2 wit inspect 5.2   260  
loop-acceleration/array_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   4700 13000 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0011 .31 - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call2_true-termination.i timeout 0 wit inspect 900   4600 14000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .85 51 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 0 wit inspect 900   4300 12000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0046 .29 - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i timeout 0 wit inspect 900   5000 14000 error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .026 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0036 .34 - wit inspect - wit inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 34   1800 290 true -32 wit inspect 3.4  260 out of memory 0 wit inspect 66     7000   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   4700 13000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .035 5.0 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0047 .26 - wit inspect - wit inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 2.9 280 26 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 4.4   240   unknown 0 wit inspect 2.6  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900   5300 13000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .036 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0039 .31 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i timeout 0 wit inspect 900   4800 12000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0019 .34 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect 2.8 270 27 true -32 wit inspect 2.8  250 false(unreach-call) 1 wit inspect 5.0   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call1.i timeout 0 wit inspect 900   4900 12000 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .028 4.8 error (invalid witness file) 0 wit inspect .88 47 error (invalid witness file) 0 wit inspect .0029 .28 - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 2.8 280 25 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 4.4   240   unknown 0 wit inspect 2.6  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect 2.8 260 23 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 5.3   250   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call4.i timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0043 .28 - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 4.1 290 35 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 7.9   320   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 3.8 280 31 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 7.4   330   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
loop-acceleration/array_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   4700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .022 4.9
loop-acceleration/array_true-unreach-call2_true-termination.i timeout 0 wit inspect 900   4600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .017 5.0
loop-acceleration/array_true-unreach-call3_true-termination.i timeout 0 wit inspect 900   4300 9900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .018 4.9
loop-acceleration/array_true-unreach-call4_true-termination.i timeout 0 wit inspect 900   4600 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.9
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 3.0 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 6.6   270  
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 140   3800 2000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    480 timeout 0 wit inspect 960     670  
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect 23   1600 220 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4  310 true 2 wit inspect 65     670  
loop-acceleration/functions_true-unreach-call1_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 43 error (2) 0 wit inspect .018 4.9
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 2.9 280 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 4.9   250  
loop-acceleration/nested_true-unreach-call1.i timeout 0 wit inspect 900   5200 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .018 4.8
loop-acceleration/overflow_true-unreach-call1.i true 1 wit inspect 2.9 270 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 timeout 0 wit inspect 960     570  
loop-acceleration/phases_true-unreach-call1.i timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .026 4.9
loop-acceleration/phases_true-unreach-call2_false-termination.i false(unreach-call) -16 wit inspect 3.2 280 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 true 2 wit inspect 6.5   280  
loop-acceleration/simple_true-unreach-call1.i timeout 0 wit inspect 900   4900 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .023 4.8
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 2.8 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 5.3   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i false(unreach-call) -16 wit inspect 3.3 280 31 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2400 true 2 wit inspect 240     540  
loop-acceleration/simple_true-unreach-call4.i timeout 0 wit inspect 900   4800 11000 - 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-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 5.0 300 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    490 true 2 wit inspect 77     430  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 4.2 290 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  270 true 2 wit inspect 6.6   270  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 1 wit inspect 4.3 290 36 false(unreach-call) 1 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 4.5   240   unknown 0 wit inspect 2.7  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   4100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .017 4.9
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i timeout 0 wit inspect 900   4100 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 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   4600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.8
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i timeout 0 wit inspect 900   5100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .020 4.9
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true 2 wit inspect 2.9 280 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 true 2 wit inspect 5.8   260  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i true 2 wit inspect 3.4 270 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  270 true 2 wit inspect 5.6   260  
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.0 280 29 true -32 wit inspect 2.9  250 false(unreach-call) 1 wit inspect 5.0   270   unknown 0 wit inspect 2.7  210 true -32 wit inspect .58   19    - wit inspect - wit inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .018 4.9
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .049 4.9
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 2 wit inspect 5.8 300 47 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 true 2 wit inspect 13     500  
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .017 4.9
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .045 4.9
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4900 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 4.8
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4900 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.8
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .039 5.0
loop-invgen/heapsort_true-unreach-call_true-termination.i true 2 wit inspect 41   2200 350 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 true 2 wit inspect 64     690  
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 2.9 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  270 true 2 wit inspect 6.2   270  
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 5.3 300 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  280 true 2 wit inspect 11     370  
loop-invgen/nest-if3_true-unreach-call_true-termination.i true 2 wit inspect 3.2 280 25 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 true 2 wit inspect 6.2   260  
loop-invgen/nested6_true-unreach-call_true-termination.i true 2 wit inspect 6.8 430 58 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 true 2 wit inspect 10     400  
loop-invgen/nested9_true-unreach-call_true-termination.i true 2 wit inspect 6.3 390 54 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 true 2 wit inspect 10     460  
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i true 2 wit inspect 7.3 440 59 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    7000 true 2 wit inspect 16     520  
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .018 4.9
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i true 1 wit inspect 2.9 270 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 300    7000 false(unreach-call) -16 wit inspect 400     4500  
loop-invgen/up_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5000 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .047 5.0
loop-lit/afnp2014_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   4200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 4.8
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i true 2 wit inspect 4.6 300 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    650 true 2 wit inspect 9.0   410  
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect 4.5 290 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  280 true 2 wit inspect 7.7   310  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 3.8 280 30 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 8.1   310  
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect 4.3 280 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 true 2 wit inspect 6.9   260  
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 3.5 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  290 true 2 wit inspect 5.4   260  
loop-lit/ddlm2013_true-unreach-call.i timeout 0 wit inspect 900   4500 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .017 4.9
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect 66   3700 630 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 290    2700 true 2 wit inspect 110     1200  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i true 2 wit inspect 5.5 310 47 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 true 2 wit inspect 5.8   310  
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect 110   3800 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 45    1000 true 2 wit inspect 92     1800  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i true 2 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1300 true 2 wit inspect 5.8   260  
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 wit inspect 4.3 280 36 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 7.7   280  
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect 3.0 270 25 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 true 2 wit inspect 7.4   280  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   5400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .018 4.8
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i false(unreach-call) -16 wit inspect 5.1 300 41 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 out of memory 0 wit inspect 110     7000  
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 2.8 260 27 timeout 0 wit inspect 92    2300 false(unreach-call) 1 wit inspect 4.6   250   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loop-new/count_by_1_true-unreach-call_true-termination.i timeout 0 wit inspect 910   5000 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
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect 3.4 280 29 - wit inspect - wit inspect - wit