Tool CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:36:53 CET 2017-12-01 08:24:12 CET 2017-12-01 08:27:09 CET 2017-12-01 08:31:26 CET 2017-12-01 04:24:37 CET 2017-12-01 07:42:15 CET
Run set cpa-bam-bnb.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Loops
Options -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
loops/array_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.5 290 29 false(unreach-call) 1 wit inspect 3.6  280 false(unreach-call) 1 wit inspect 5.6   270   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/bubble_sort_false-unreach-call.i false(unreach-call) 1 wit inspect 5.3 310 42 unknown 0 wit inspect 4.5  270 error (7) 0 wit inspect 8.2   210   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.2 280 31 false(unreach-call) 1 wit inspect 3.0  250 false(unreach-call) 1 wit inspect 4.7   250   unknown 0 wit inspect 3.5  180 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
loops/eureka_01_false-unreach-call_true-termination.i error 0 wit inspect 13   480 110 error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.7 300 35 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.8   260   unknown 0 wit inspect 3.1  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
loops/insertion_sort_false-unreach-call_true-termination.i error 0 wit inspect 4.1 300 35 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .025 5.0 error (invalid witness file) 0 wit inspect .84 48 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.8 340 48 false(unreach-call) 1 wit inspect 4.1  260 false(unreach-call) 1 wit inspect 9.6   350   unknown 0 wit inspect 2.9  210 true -32 wit inspect .60   19    - wit inspect - wit inspect
loops/linear_search_false-unreach-call.i error 0 wit inspect 3.5 310 31 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 1 wit inspect 5.0 330 42 false(unreach-call) 1 wit inspect 7.3  520 timeout 0 wit inspect 97     4500   unknown 0 wit inspect 3.3  180 false(unreach-call) 1 wit inspect .63   19    - wit inspect - wit inspect
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.9 300 34 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.3   270   unknown 0 wit inspect 3.0  210 true -32 wit inspect 4.8    19    - wit inspect - wit inspect
loops/n.c24_false-unreach-call.i timeout 0 wit inspect 900   4400 10000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .69 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 3.3 280 29 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 3.3  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.1 320 32 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 6.7   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
loops/s3_false-unreach-call.i witness invalid (false(unreach-call)) 0 wit inspect 13   530 96 error (invalid witness file) 0 wit inspect 3.0  170 unknown 0 wit inspect 3.3   190   error (invalid witness file) 0 wit inspect 3.4  190 error (invalid witness file) 0 wit inspect .68   19    - wit inspect - wit inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.2 330 52 false(unreach-call) 1 wit inspect 4.2  270 false(unreach-call) 1 wit inspect 24     440   unknown 0 wit inspect 4.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 4.5 310 36 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 7.6   270   unknown 0 wit inspect 3.2  190 true -32 wit inspect .61   19    - wit inspect - wit inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.2 300 37 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 7.6   270   unknown 0 wit inspect 3.0  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.7 300 43 false(unreach-call) 1 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 8.7   450   unknown 0 wit inspect 3.6  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.8 310 46 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 16     1300   unknown 0 wit inspect 3.4  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 3.9 290 34 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 7.8   280   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect 4.1 300 32 false(unreach-call) 1 wit inspect 4.3  260 false(unreach-call) 1 wit inspect 9.0   280   unknown 0 wit inspect 3.4  190 true -32 wit inspect .62   19    - wit inspect - wit inspect
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.3 280 28 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.8   260   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.2 280 32 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.4 280 32 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.8   260   unknown 0 wit inspect 3.3  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.3 280 28 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 6.8   270   unknown 0 wit inspect 3.1  210 true -32 wit inspect .59   18    - wit inspect - wit inspect
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.2 280 31 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.8   260   unknown 0 wit inspect 3.4  190 true -32 wit inspect .61   18    - wit inspect - wit inspect
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.3 280 29 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.8   250   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.3 310 29 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 8.9   310   unknown 0 wit inspect 3.2  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 4.5 320 38 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 17     500   unknown 0 wit inspect 2.1  210 error (2) 0 wit inspect .69   19    - wit inspect - wit inspect
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect 7.3 380 67 false(unreach-call) 1 wit inspect 4.8  290 timeout 0 wit inspect 97     2400   unknown 0 wit inspect 4.0  210 true -32 wit inspect .62   19    - wit inspect - wit inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.3 280 30 timeout 0 wit inspect 96    2700 false(unreach-call) 1 wit inspect 6.1   250   timeout 0 wit inspect 97    2700 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 3.1 270 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  280 true 2 wit inspect 21     390  
loops/bubble_sort_true-unreach-call_true-termination.i true 2 wit inspect 3.2 300 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  260 true 2 wit inspect 5.9   230  
loops/count_up_down_true-unreach-call_true-termination.i error 0 wit inspect 3.0 280 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .036 4.9
loops/eureka_01_true-unreach-call.i true 1 wit inspect 11   570 89 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4600 out of memory 0 wit inspect 630     7000  
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect 4.9 290 46 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 97     1100  
loops/for_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.6  260 true 2 wit inspect 5.4   260  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  290 true 2 wit inspect 5.9   270  
loops/insertion_sort_true-unreach-call_true-termination.i error 0 wit inspect 4.2 310 34 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .023 4.9
loops/invert_string_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 5.3 330 46 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.2  270 true 2 wit inspect 75     800  
loops/linear_sea.ch_true-unreach-call.i error 0 wit inspect 3.5 310 33 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 5.0
loops/lu.cmp_true-unreach-call.i true 1 wit inspect 4.3 280 42 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3200 timeout 0 wit inspect 960     4500  
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 3.2 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  280 true 2 wit inspect 18     350  
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect 3.0 270 29 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6300 true 2 wit inspect 9.5   340  
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 3.4 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 true 2 wit inspect 7.4   340  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 3.1 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  270 true 2 wit inspect 7.0   340  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  280 true 2 wit inspect 9.4   370  
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 3.9 280 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 500    7000 true 2 wit inspect 9.0   370  
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect 4.0 290 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  270 true 2 wit inspect 5.8   260  
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 3.0 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  280 true 2 wit inspect 12     510  
loops/sum_array_true-unreach-call.i error 0 wit inspect 7.1 360 57 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .018 4.9
loops/terminator_02_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 4.1  270 true 2 wit inspect 6.5   260  
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect 3.1 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 5.4   260  
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 6.3 340 57 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 28    1000 true 2 wit inspect 7.6   250  
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 5.4   260  
loops/trex03_true-unreach-call_true-termination.i error 0 wit inspect 3.5 290 35 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8
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 4.1  270 true 2 wit inspect 5.9   260  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect 3.1 300 29 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 8.0   300  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 19   800 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    380 false(unreach-call) -16 wit inspect 16     480  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 3.2 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  270 true 2 wit inspect 13     340  
loops/vogal_true-unreach-call.i true 2 wit inspect 60   2900 670 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 110    1300 false(unreach-call) -16 wit inspect 24     630  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 2.9 270 24 - wit inspect - wit inspect - wit inspect - wit inspect out of java memory 0 wit inspect 540    5200 true 2 wit inspect 6.0   250  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect out of java memory 0 wit inspect 620    5200 true 2 wit inspect 5.0   250  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect 2.8 270 28 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5200 true 2 wit inspect 5.3   260  
loop-acceleration/array_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   4200 8800 error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .98 49 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call2_true-termination.i timeout 0 wit inspect 900   4300 10000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect - wit inspect
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 0 wit inspect 900   4200 8600 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .031 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
loop-acceleration/const_false-unreach-call1.i timeout 0 wit inspect 900   4300 10000 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0030 .26 - wit inspect - wit inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 45   1900 380 false(unreach-call) 1 wit inspect 4.5  280 out of memory 0 wit inspect 85     7000   unknown 0 wit inspect 4.4  220 false(unreach-call) 1 wit inspect .67   20    - wit inspect - wit inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   4400 7700 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 3.1 280 25 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.6   240   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900   4100 11000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call1.i timeout 0 wit inspect 900   4100 12000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0012 .32 - wit inspect - wit inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) 1 wit inspect 3.1 280 28 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.0   260   unknown 0 wit inspect 3.2  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call1.i timeout 0 wit inspect 900   4200 8200 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 3.1 280 26 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.6   240   unknown 0 wit inspect 3.6  190 false(unreach-call) 1 wit inspect .82   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect 3.2 280 27 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.1   250   unknown 0 wit inspect 3.2  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
loop-acceleration/simple_false-unreach-call4.i timeout 0 wit inspect 900   4300 8500 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 3.7 290 27 false(unreach-call) 1 wit inspect 3.6  290 false(unreach-call) 1 wit inspect 8.2   320   unknown 0 wit inspect 3.2  180 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 3.7 290 29 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 8.6   320   unknown 0 wit inspect 4.1  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
loop-acceleration/array_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   4200 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 4.9
loop-acceleration/array_true-unreach-call2_true-termination.i timeout 0 wit inspect 900   4300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .024 4.8
loop-acceleration/array_true-unreach-call3_true-termination.i timeout 0 wit inspect 900   4300 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9
loop-acceleration/array_true-unreach-call4_true-termination.i timeout 0 wit inspect 900   4200 9500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 4.8
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 3.1 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  270 false(unreach-call) -16 wit inspect 4.8   260  
loop-acceleration/diamond_true-unreach-call1_true-termination.i error 0 wit inspect 54   2400 570 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .021 4.8
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect 9.4 470 72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  310 true 2 wit inspect 65     700  
loop-acceleration/functions_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   4400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 5.0
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 670    6000 true 2 wit inspect 5.2   260  
loop-acceleration/nested_true-unreach-call1.i timeout 0 wit inspect 900   4000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .022 5.0
loop-acceleration/overflow_true-unreach-call1.i true 1 wit inspect 3.0 270 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 570    7000 false(unreach-call) -16 wit inspect 5.6   250  
loop-acceleration/phases_true-unreach-call1.i timeout 0 wit inspect 900   4100 7700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.9
loop-acceleration/phases_true-unreach-call2_false-termination.i error 0 wit inspect 3.3 290 31 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .024 4.9
loop-acceleration/simple_true-unreach-call1.i timeout 0 wit inspect 900   4300 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.9
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 3.0 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 4.9   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i timeout 0 wit inspect 910   8400 6700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.9
loop-acceleration/simple_true-unreach-call4.i timeout 0 wit inspect 900   4300 8700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .024 4.9
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 3.5 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  360 true 2 wit inspect 14     490  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  260 true 2 wit inspect 6.8   270  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i error 0 wit inspect 2.6 290 21 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0012 .28 - wit inspect - wit inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   4200 8400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .021 4.9
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i error 0 wit inspect 2.8 290 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .021 4.9
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i error 0 wit inspect 2.6 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.8
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i error 0 wit inspect 2.6 270 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true 2 wit inspect 4.3 290 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 false(unreach-call) -16 wit inspect 5.6   260  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i true 2 wit inspect 4.6 290 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  270 false(unreach-call) -16 wit inspect 6.1   260  
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.8 290 34 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 2.9  180 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 3.5 280 34 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 true 2 wit inspect 9.8   320  
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect 4.8 290 38 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    7000 true 2 wit inspect 10     340  
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 2 wit inspect 68   3600 660 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 true 2 wit inspect 16     500  
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i true 2 wit inspect 15   620 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 true 2 wit inspect 13     500  
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i true 2 wit inspect 13   630 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  290 true 2 wit inspect 11     410  
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.8
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4200 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .026 5.0
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4100 7800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .020 4.9
loop-invgen/heapsort_true-unreach-call_true-termination.i true 2 wit inspect 64   2900 660 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3000 true 2 wit inspect 67     680  
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 3.2 270 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  280 true 2 wit inspect 7.8   280  
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 4.2 290 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  280 true 2 wit inspect 11     350  
loop-invgen/nest-if3_true-unreach-call_true-termination.i true 2 wit inspect 4.6 290 40 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3300 true 2 wit inspect 6.5   260  
loop-invgen/nested6_true-unreach-call_true-termination.i true 2 wit inspect 140   3900 1500 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 true 2 wit inspect 9.7   400  
loop-invgen/nested9_true-unreach-call_true-termination.i true 2 wit inspect 11   470 79 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 true 2 wit inspect 11     450  
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i true 2 wit inspect 12   580 85 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 610    7000 true 2 wit inspect 16     560  
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4000 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4300 8800 - 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-invgen/up_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .019 4.9
loop-lit/afnp2014_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   4000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 4.9
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i true 2 wit inspect 3.0 270 28 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    640 true 2 wit inspect 9.1   410  
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect 2.9 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  280 true 2 wit inspect 10     440  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 3.1 280 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 10     320  
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect 4.0 280 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 timeout 0 wit inspect 960     1200  
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 5.9 370 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  270 true 2 wit inspect 6.1   260  
loop-lit/ddlm2013_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 .53 43 error (2) 0 wit inspect .018 4.8
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect 87   3900 820 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 39    590 true 2 wit inspect 100     1200  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i true 2 wit inspect 16   630 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2300 true 2 wit inspect 11     310  
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect 47   2300 440 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 54    1000 false(unreach-call) -16 wit inspect 5.4   270  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i true 2 wit inspect 3.6 280 31 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1300 true 2 wit inspect 6.4   260  
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 wit inspect 3.2 280 29 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 440    7000 true 2 wit inspect 9.4   300  
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect 3.1 280 29 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5300 true 2 wit inspect 5.2   280  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 4.2 290 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 true 2 wit inspect 8.0   290  
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i false(unreach-call) -16 wit inspect 4.0 300 37 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.7  260 true 2 wit inspect 45     1100  
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 92   4200 820 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.0   250   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
loop-new/count_by_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4200 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect 3.7 280 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit