Tool VerifierIntegerAssignmentPrograms 1.1.12(Date 28/11/2018) CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
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.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-09 18:49:43 CET 2018-12-09 21:23:04 CET 2018-12-09 22:02:00 CET 2018-12-09 22:04:11 CET 2018-12-12 22:08:25 CET 2018-12-09 21:05:40 CET 2018-12-09 21:25:32 CET
Run set viap.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-seq-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Loops uautomizer-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Loops uautomizer-validate-correctness-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Loops
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
loops/array_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.3 5.3 130 70 1.2  0      false(unreach-call) 1 wit inspect 3.5  2.0  250 0   0      false(unreach-call) 1 --- inspect 7.3   4.6   320   .66 0      unknown 0 --- inspect 3.5  2.1  250 0   0      true -32 --- inspect .60   .60   20    .049  0      - --- inspect - --- inspect
loops/bubble_sort_false-unreach-call.i unknown 0 --- inspect 2.4 2.4 130 31 .22 .70   error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .94 .61 47 0   0      error (invalid witness file) 0 --- inspect .0018 .0031 .54 0      0      - --- inspect - --- inspect
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.9 4.9 130 66 .95 .0041 false(unreach-call) 1 wit inspect 7.9  4.4  350 0   0      false(unreach-call) 1 --- inspect 16     8.6   860   .66 0      unknown 0 --- inspect 5.3  3.0  270 0   0      false(unreach-call) 1 --- inspect .61   .61   25    .045  0      - --- inspect - --- inspect
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 14   14   130 210 3.9  1.0    timeout 0 wit inspect 98    85    1300 0   0      true -32 --- inspect 7.0   4.0   300   .35 0      unknown 0 --- inspect 3.6  2.1  250 0   0      true -32 --- inspect .59   .59   20    .057  0      - --- inspect - --- inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.7 6.7 130 94 1.4  0      false(unreach-call) 1 wit inspect 3.6  2.0  250 0   0      true -32 --- inspect 7.7   4.4   310   .66 0      unknown 0 --- inspect 3.8  2.2  250 0   0      true -32 --- inspect .57   .57   20    .049  0      - --- inspect - --- inspect
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 10   10   510 120 1.6  .17   timeout 0 wit inspect 98    83    2000 0   0      timeout 0 --- inspect 96     55     7000   1.5  0      unknown 0 --- inspect 84    71    1900 0   0      true -32 --- inspect 1.4    1.4    90    .049  0      - --- inspect - --- inspect
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 8.1 8.1 310 110 1.4  0      exception 0 --- inspect 4.6  2.4  200 0   0      true -32 --- inspect 29     18     2100   .62 0      exception 0 --- inspect 5.2  2.8  210 0   0      true -32 --- inspect .97   .99   57    .057  0      - --- inspect - --- inspect
loops/linear_search_false-unreach-call.i unknown 0 --- inspect 2.4 2.4 130 37 .22 0      error (invalid witness file) 0 --- inspect .61 .40 43 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .94 .60 47 0   0      error (invalid witness file) 0 --- inspect .0055 .0071 .53 0      0      - --- inspect - --- inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 1 wit inspect 30   30   140 410 5.2  .96   false(unreach-call) 1 wit inspect 9.6  7.3  520 0   0      true -32 --- inspect 41     31     840   .71 0      false(unreach-call) 1 --- inspect 3.9  2.3  250 0   0      false(unreach-call) 1 --- inspect .59   .59   21    .061  0      - --- inspect - --- inspect
loops/matrix_false-unreach-call_true-termination.i unknown 0 --- inspect 430   430   900 5000 .69 1.7    error (invalid witness file) 0 --- inspect .63 .41 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .91 .58 47 0   0      error (invalid witness file) 0 --- inspect .0053 .0059 .39 0      0      - --- inspect - --- inspect
loops/n.c24_false-unreach-call.i unknown 0 --- inspect 2.5 2.5 130 34 .22 0      error (invalid witness file) 0 --- inspect .61 .39 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .96 .61 47 0   0      error (invalid witness file) 0 --- inspect .0051 .0069 .40 0      0      - --- inspect - --- inspect
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 5.0 5.0 130 83 1.2  .62   exception 0 --- inspect 2.3  1.3  170 0   0      false(unreach-call) 1 --- inspect 7.1   4.0   310   .66 .0041 exception 0 --- inspect 2.8  1.6  200 0   0      false(unreach-call) 1 --- inspect .61   .61   20    .049  0      - --- inspect - --- inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.7 7.7 130 120 2.1  0      false(unreach-call) 1 wit inspect 3.8  2.1  260 0   0      true -32 --- inspect 6.8   4.3   310   .62 .0041 unknown 0 --- inspect 3.7  2.2  250 0   0      false(unreach-call) 1 --- inspect .59   .59   20    .053  0      - --- inspect - --- inspect
loops/s3_false-unreach-call.i unknown 0 --- inspect 2.5 2.5 130 31 .22 .066  error (invalid witness file) 0 --- inspect .60 .36 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .93 .59 47 0   0      error (invalid witness file) 0 --- inspect .0021 .0026 .53 0      0      - --- inspect - --- inspect
loops/string_false-unreach-call_true-termination.i unknown 0 --- inspect 17   17   130 260 .65 0      error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .94 .61 47 0   0      error (invalid witness file) 0 --- inspect .0060 .0077 .39 0      0      - --- inspect - --- inspect
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.3 5.3 130 69 1.2  0      false(unreach-call) 1 wit inspect 4.6  2.5  260 0   0      true -32 --- inspect 7.5   4.2   310   .66 0      unknown 0 --- inspect 3.7  2.1  250 0   0      true -32 --- inspect .59   .61   20    .049  0      - --- inspect - --- inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 5.5 5.5 140 68 1.2  0      true -32 wit inspect 13    6.7  430 0   0      timeout 0 --- inspect 91     58     7000   .63 0      unknown 0 --- inspect 9.7  5.2  280 0   .0041 true -32 --- inspect .69   .68   30    .049  0      - --- inspect - --- inspect
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 5.6 5.6 150 78 1.2  0      true -32 wit inspect 6.0  3.2  260 0   0      out of memory 0 --- inspect 74     47     7000   1.4  0      unknown 0 --- inspect 11    5.6  340 0   0      true -32 --- inspect .71   .70   32    .045  0      - --- inspect - --- inspect
loops/sum03_false-unreach-call_true-termination.i unknown 0 --- inspect 98   82   15000 1500 .27 .0041 error (invalid witness file) 0 --- inspect .61 .37 42 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .96 .61 48 0   0      error (invalid witness file) 0 --- inspect .0063 .0081 .52 0      0      - --- inspect - --- inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.2 5.3 130 71 1.2  .64   true -32 wit inspect 4.4  2.4  260 0   0      out of memory 0 --- inspect 59     38     7000   .63 0      false(unreach-call) 1 --- inspect 5.0  2.8  260 0   0      false(unreach-call) 1 --- inspect .61   .61   22    .045  0      - --- inspect - --- inspect
loops/sum_array_false-unreach-call.i false(unreach-call) 0 wit inspect 8.0 8.1 200 110 1.6  0      timeout 0 wit inspect 95    89    1000 0   .0041 timeout 0 --- inspect 91     58     7000   .62 0      unknown 0 --- inspect 12    6.3  360 0   0      true -32 --- inspect .82   .84   40    .057  0      - --- inspect - --- inspect
loops/terminator_01_false-unreach-call_true-termination.i unknown 0 --- inspect 2.4 2.4 130 34 .22 0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .92 .60 47 0   0      error (invalid witness file) 0 --- inspect .0037 .0048 .41 0      0      - --- inspect - --- inspect
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.8 5.8 130 72 1.4  .0041 exception 0 --- inspect 2.7  1.5  190 0   0      false(unreach-call) 1 --- inspect 7.0   4.0   310   .66 0      exception 0 --- inspect 2.8  1.6  200 0   0      false(unreach-call) 1 --- inspect .65   .65   20    .049  0      - --- inspect - --- inspect
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.3 5.3 130 81 1.2  0      exception 0 --- inspect 2.4  1.4  190 0   0      false(unreach-call) 1 --- inspect 8.1   4.9   310   .66 0      exception 0 --- inspect 2.8  1.6  180 0   0      true -32 --- inspect .58   .59   20    .045  0      - --- inspect - --- inspect
loops/trex01_false-unreach-call_true-termination.i error (1) 0 --- inspect 4.8 4.9 130 69 .46 0      error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .95 .62 47 0   0      error (invalid witness file) 0 --- inspect .0030 .0033 .40 0      0      - --- inspect - --- inspect
loops/trex02_false-unreach-call_true-termination.i unknown 0 --- inspect 5.9 5.9 130 74 .49 0      error (invalid witness file) 0 --- inspect .62 .39 41 0   0      error (2) 0 --- inspect .020 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .91 .60 46 0   0      error (invalid witness file) 0 --- inspect .0066 .0083 .52 0      0      - --- inspect - --- inspect
loops/trex03_false-unreach-call_true-termination.i witness invalid (false(unreach-call)) 0 wit inspect 6.5 6.5 130 92 1.6  0      error (invalid witness file) 0 --- inspect 2.5  1.4  200 0   0      error (invalid witness file) 0 --- inspect 5.2   2.8   270   .65 0      error (invalid witness file) 0 --- inspect 2.9  1.7  180 0   0      error (invalid witness file) 0 --- inspect .56   .58   20    .0041 0      - --- inspect - --- inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i unknown 0 --- inspect 2.4 2.4 130 34 .22 .48   error (invalid witness file) 0 --- inspect .58 .37 40 0   0      error (2) 0 --- inspect .019 .020 5.6 0    0      error (invalid witness file) 0 --- inspect .98 .63 48 0   0      error (invalid witness file) 0 --- inspect .0062 .0078 .52 0      0      - --- inspect - --- inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i unknown 0 --- inspect 2.5 2.5 130 33 .22 0      error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0      error (invalid witness file) 0 --- inspect .92 .59 46 0   0      error (invalid witness file) 0 --- inspect .0063 .0082 .52 0      0      - --- inspect - --- inspect
loops/vogal_false-unreach-call.i unknown 0 --- inspect 340   350   550 4100 .88 0      error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .95 .62 47 0   0      error (invalid witness file) 0 --- inspect .0054 .0067 .53 0      0      - --- inspect - --- inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i unknown 0 --- inspect 97   81   15000 1600 .27 .0041 error (invalid witness file) 0 --- inspect .58 .35 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .97 .63 48 0   0      error (invalid witness file) 0 --- inspect .0067 .010  .53 0      0      - --- inspect - --- inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 18   18   250 180 .48 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  290 0   0      true 2 --- inspect 11     6.8   400   .62 0     
loops/bubble_sort_true-unreach-call_true-termination.i true 1 --- inspect 9.5 9.6 130 140 .46 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
loops/count_up_down_true-unreach-call_true-termination.i true 2 wit inspect 4.6 4.7 130 55 .48 2.2    - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 380    370    7000 0   0      true 2 --- inspect 11     6.7   370   .62 .0041
loops/eureka_01_true-unreach-call.i true 1 wit inspect 110   110   420 1500 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    5200 0   0      timeout 0 --- inspect 960     930     5000   .70 0     
loops/eureka_05_true-unreach-call_true-termination.i true 1 wit inspect 8.4 8.4 230 95 .48 2.1    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3600 0   0      timeout 0 --- inspect 960     930     1500   1.1  0     
loops/for_infinite_loop_1_true-unreach-call_false-termination.i unknown 0 --- inspect 110   98   15000 1600 .27 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .41 40 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0     
loops/for_infinite_loop_2_true-unreach-call_false-termination.i unknown 0 --- inspect 110   98   15000 1700 .27 1.0    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .036 .037 5.6 0    0     
loops/insertion_sort_true-unreach-call_true-termination.i true 1 wit inspect 35   35   530 360 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1200 0   0      timeout 0 --- inspect 960     900     1500   1.8  0     
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect 59   59   430 670 .51 2.4    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    12    500 0   0      true 2 --- inspect 390     370     1300   .62 0     
loops/linear_sea.ch_true-unreach-call.i unknown 0 --- inspect 2.4 2.4 130 37 .22 .62   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
loops/lu.cmp_true-unreach-call.i error (1) 0 --- inspect 160   160   130 2100 5.1  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0     
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect 60   60   570 720 .50 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  290 0   0      true 2 --- inspect 11     6.9   430   .62 0     
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect 56   56   150 830 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 760    740    7000 0   0      true 2 --- inspect 11     6.1   360   .62 0     
loops/n.c40_true-unreach-call_true-termination.i unknown 0 --- inspect 160   160   510 1800 .50 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .056 .057 5.5 0    0     
loops/nec40_true-unreach-call_true-termination.i unknown 0 --- inspect 160   160   570 1600 .52 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
loops/string_true-unreach-call_true-termination.i unknown 0 --- inspect 17   17   130 220 .65 1.7    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 41 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0     
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 5.5 5.5 130 65 .52 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 460    450    7000 0   0      true 2 --- inspect 11     6.3   390   .62 0     
loops/sum03_true-unreach-call_false-termination.i unknown 0 --- inspect 88   72   15000 1400 .27 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .048 .051 5.7 0    0     
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 5.2 5.3 130 73 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.1  3.3  290 0   0      true 2 --- inspect 11     6.9   430   .62 0     
loops/sum_array_true-unreach-call.i unknown 0 --- inspect 470   470   430 5800 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0      error (2) 0 --- inspect .024 .034 5.7 0    0     
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 5.8 6.0 130 81 .52 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  290 0   0      true 2 --- inspect 7.8   4.9   310   .62 0     
loops/terminator_03_true-unreach-call_true-termination.i unknown 0 --- inspect 7.5 7.7 130 96 .56 1.7    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0      error (2) 0 --- inspect .034 .038 5.6 0    0     
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 9.5 9.6 150 140 .47 2.1    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    21    1100 0   0      true 2 --- inspect 7.4   4.6   310   .62 0     
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 4.7 5.0 130 53 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  280 0   0      true 2 --- inspect 7.0   4.4   310   .62 0     
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect 5.7 5.8 130 67 .48 1.1    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.3  3.0  290 0   0      true 2 --- inspect 7.3   4.6   310   .62 0     
loops/trex04_true-unreach-call_false-termination.i timeout 0 --- inspect 900   900   130 8600 .27 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .049 .051 5.5 0    0     
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i unknown 0 --- inspect 2.4 2.4 130 36 .22 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 42 0   0      error (2) 0 --- inspect .040 .041 5.5 0    0     
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i unknown 0 --- inspect 2.5 2.5 130 37 .22 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .050 .051 5.5 0    0     
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i unknown 0 --- inspect 2.7 2.7 130 39 .22 .91   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 41 0   0      error (2) 0 --- inspect .048 .049 5.5 0    0     
loops/vogal_true-unreach-call.i true 2 wit inspect 240   240   350 3500 .76 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 72    59    1000 0   0      timeout 0 --- inspect 960     920     1300   .63 0     
loops/while_infinite_loop_1_true-unreach-call_false-termination.i out of memory 0 --- inspect 96   81   15000 1600 .25 .64   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .021 .030 5.5 0    0     
loops/while_infinite_loop_2_true-unreach-call_false-termination.i out of memory 0 --- inspect 95   80   15000 1300 .25 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .40 41 0   0      error (2) 0 --- inspect .041 .042 5.5 0    0     
loops/while_infinite_loop_3_true-unreach-call_false-termination.i out of memory 0 --- inspect 97   81   15000 1400 .25 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .023 .023 5.6 0    0     
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 4.7 4.7 130 67 .95 0      timeout 0 --- inspect 97    91    810 0   0      true -32 --- inspect 7.6   4.3   310   .66 0      false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0      false(unreach-call) 1 --- inspect .60   .60   20    .045  0      - --- inspect - --- inspect
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 4.7 4.7 130 70 .95 0      timeout 0 --- inspect 97    91    1100 0   0      true -32 --- inspect 7.6   4.3   310   .66 0      false(unreach-call) 1 --- inspect 3.4  2.0  240 0   0      false(unreach-call) 1 --- inspect .59   .58   20    .045  0      - --- inspect - --- inspect
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 wit inspect 5.5 5.5 130 79 1.2  0      timeout 0 wit inspect 96    89    1000 0   0      true -32 --- inspect 7.3   4.6   310   .66 0      true -32 --- inspect 3.8  2.2  250 0   0      true -32 --- inspect .57   .57   20    .049  0      - --- inspect - --- inspect
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect 4.7 4.7 130 63 .95 0      true -32 wit inspect 5.5  2.9  260 0   0      out of memory 0 --- inspect 81     55     7000   .63 .0041 false(unreach-call) 1 --- inspect 4.7  2.6  260 0   .0041 false(unreach-call) 1 --- inspect .58   .58   22    .045  0      - --- inspect - --- inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect 5.8 5.8 130 76 1.4  0      false(unreach-call) 1 wit inspect 43    34    800 0   0      true -32 --- inspect 8.5   5.4   320   .66 0      unknown 0 --- inspect 3.4  2.0  240 0   0      false(unreach-call) 1 --- inspect .61   .61   20    .045  0      - --- inspect - --- inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 5.9 5.9 130 80 1.2  .041  exception 0 --- inspect 3.0  1.6  210 0   0      true -32 --- inspect 8.0   4.4   300   .66 0      exception 0 --- inspect 3.2  1.8  210 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    22    .045  0      - --- inspect - --- inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 4.7 4.7 130 70 .95 .078  exception 0 --- inspect 2.4  1.3  170 0   0      false(unreach-call) 1 --- inspect 6.8   4.3   300   .66 0      exception 0 --- inspect 3.0  1.7  170 0   0      false(unreach-call) 1 --- inspect .56   .56   20    .045  0      - --- inspect - --- inspect
loop-acceleration/nested_false-unreach-call1.i false(unreach-call) 1 wit inspect 26   26   2600 240 1.2  0      exception 0 --- inspect 14    8.1  990 0   0      true -32 --- inspect 13     6.8   680   .66 0      exception 0 --- inspect 12    6.9  930 0   0      false(unreach-call) 1 --- inspect 8.6    8.6    450    .045  0      - --- inspect - --- inspect
loop-acceleration/phases_false-unreach-call1.i false(unreach-call) 1 wit inspect 6.1 6.1 130 81 1.4  .0041 exception 0 --- inspect 2.7  1.5  200 0   0      true -32 --- inspect 7.9   4.4   410   .62 .0041 exception 0 --- inspect 3.3  1.9  210 0   0      false(unreach-call) 1 --- inspect .86   .86   22    .045  0      - --- inspect - --- inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i timeout 0 --- inspect 900   900   130 14000 .27 .98   error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .92 .60 47 0   0      error (invalid witness file) 0 --- inspect .0047 .0054 .39 0      0      - --- inspect - --- inspect
loop-acceleration/simple_false-unreach-call1.i false(unreach-call) 1 wit inspect 4.9 4.9 130 73 .95 0      exception 0 --- inspect 2.6  1.4  190 0   0      true -32 --- inspect 7.8   4.3   340   .66 0      exception 0 --- inspect 3.2  1.8  200 0   0      false(unreach-call) 1 --- inspect .80   .80   21    .045  0      - --- inspect - --- inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 0 wit inspect 5.1 5.2 130 68 .95 0      exception 0 --- inspect 2.8  1.5  190 0   0      true -32 --- inspect 10     5.5   530   .66 .0041 exception 0 --- inspect 3.0  1.7  200 0   0      true -32 --- inspect .57   .57   21    .045  0      - --- inspect - --- inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect 4.7 4.7 130 60 .95 .62   exception 0 --- inspect 2.6  1.5  200 0   0      true -32 --- inspect 8.0   4.8   430   .62 0      exception 0 --- inspect 3.1  1.8  200 0   0      false(unreach-call) 1 --- inspect .57   .57   21    .045  0      - --- inspect - --- inspect
loop-acceleration/simple_false-unreach-call4.i out of memory 0 --- inspect 39   28   15000 500 .95 0      error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .98 .64 49 0   0      error (invalid witness file) 0 --- inspect .0049 .0061 .52 0      0      - --- inspect - --- inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 4.8 4.8 130 60 .95 .0041 false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0      true -32 --- inspect 9.4   5.8   310   .62 0      false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0      false(unreach-call) 1 --- inspect .61   .63   20    .045  0      - --- inspect - --- inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 4.8 4.8 130 60 .95 .62   false(unreach-call) 1 wit inspect 3.5  2.0  250 0   .0041 true -32 --- inspect 8.9   5.5   310   .66 0      false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0      false(unreach-call) 1 --- inspect .58   .58   20    .045  0      - --- inspect - --- inspect
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect 7.6 7.8 240 86 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  280 0   0      true 2 --- inspect 12     8.1   340   .62 0     
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect 55   55   200 640 .49 2.1    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5000 0   0      timeout 0 --- inspect 960     930     800   .94 0     
loop-acceleration/array_true-unreach-call3_true-termination.i true 2 wit inspect 8.0 8.3 220 88 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  280 0   0      true 2 --- inspect 10     6.0   380   .62 0     
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 6.6 6.6 140 80 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    6000 0   0      timeout 0 --- inspect 960     930     940   .62 0     
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 4.4 4.4 130 70 .48 2.0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  280 0   .0041 true 2 --- inspect 8.4   5.3   320   .62 0     
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 140   140   240 1900 .51 .13   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    12    590 0   0      timeout 0 --- inspect 960     940     560   .97 0     
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect 310   310   230 4900 .55 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.4  4.3  330 0   0      true 2 --- inspect 270     260     660   .62 0     
loop-acceleration/functions_true-unreach-call1_true-termination.i true 1 wit inspect 23   25   130 340 .48 1.7    - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 430    420    7000 0   0      timeout 0 --- inspect 960     930     580   .63 0     
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 4.6 4.7 130 62 .48 1.7    - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 410    400    7000 0   0      true 2 --- inspect 7.3   4.6   310   .62 0     
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect 150   150   130 1700 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.0  3.3  300 0   0      true 2 --- inspect 43     31     750   .62 0     
loop-acceleration/overflow_true-unreach-call1.i true 1 wit inspect 190   190   130 1800 .48 .0041 - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 520    510    7000 0   0      timeout 0 --- inspect 960     940     540   .99 .0041
loop-acceleration/phases_true-unreach-call1.i true 1 wit inspect 120   120   260 1600 .51 .0041 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6100 0   .0041 timeout 0 --- inspect 960     940     540   .63 0     
loop-acceleration/phases_true-unreach-call2_false-termination.i timeout 0 --- inspect 900   900   130 12000 .27 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .030 .032 5.6 0    0     
loop-acceleration/simple_true-unreach-call1.i true 1 wit inspect 16   17   130 170 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 570    550    7000 0   0      timeout 0 --- inspect 960     940     650   .63 0     
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 26   28   130 320 .48 1.1    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  280 0   0      true 2 --- inspect 6.9   4.0   300   .62 0     
loop-acceleration/simple_true-unreach-call3_true-termination.i true 2 wit inspect 4.5 4.6 130 54 .48 2.4    - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 750    740    7000 0   0      true 2 --- inspect 9.4   6.2   330   .62 0     
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect 16   17   130 170 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.4  280 0   0      true 2 --- inspect 8.6   4.9   310   .62 0     
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 6.0 6.0 130 85 .50 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.0  4.8  390 0   0      true 2 --- inspect 26     22     460   .62 0     
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 5.2 5.3 130 75 .48 2.0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  280 0   0      true 2 --- inspect 8.5   5.2   320   .62 0     
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i timeout 0 --- inspect 900   900   130 11000 .27 .0041 error (invalid witness file) 0 --- inspect .59 .39 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .91 .60 46 0   0      error (invalid witness file) 0 --- inspect .0049 .0059 .39 0      0      - --- inspect - --- inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i true 1 wit inspect 11   11   240 130 .50 2.2    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4300 0   0      timeout 0 --- inspect 960     940     620   1.0  .0041
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i unknown 0 --- inspect 160   160   250 2000 .57 2.4    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 42 0   0      error (2) 0 --- inspect .039 .042 5.7 0    0     
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i true 1 wit inspect 10   10   240 130 .48 2.3    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5600 0   0      timeout 0 --- inspect 960     940     720   1.1  0     
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i true 2 wit inspect 14   14   130 180 .59 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1800 0   0      true 2 --- inspect 31     26     430   .62 0     
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true 2 wit inspect 29   29   190 460 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  280 0   0      true 2 --- inspect 7.3   4.1   320   .62 0     
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i true 2 wit inspect 28   29   190 450 .48 1.3    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  280 0   0      true 2 --- inspect 8.0   4.5   310   .62 0     
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+lhb-reducer.c unknown 0 --- inspect 2.6 2.6 130 34 .22 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 42 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+nlh-reducer.c unknown 0 --- inspect 2.5 2.5 130 39 .22 .63   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .040 .041 5.7 0    0     
loop-invgen/id_trans_false-unreach-call_true-termination.i unknown 0 --- inspect 7.3 7.5 130 110 .54 1.7    error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .95 .61 48 0   0      error (invalid witness file) 0 --- inspect .0066 .0085 .52 0      0      - --- inspect - --- inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i error (1) 0 --- inspect 4.1 4.2 130 57 .46 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0      error (2) 0 --- inspect .020 .033 5.6 0    0     
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect 6.7 6.7 140 81 .50 1.7    - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 550    540    7000 0   0      true 2 --- inspect 10     6.3   360   .62 0     
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i timeout 0 --- inspect 900   900   130 11000 .57 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .033 .034 5.6 0    0     
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i unknown 0 --- inspect 230   230   140 3300 3.3  2.0    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i unknown 0 --- inspect 500   500   290 6400 3.6  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
loop-invgen/down_true-unreach-call_true-termination.i true 1 wit inspect 6.2 6.2 130 86 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 340    320    7000 0   .0041 timeout 0 --- inspect 960     790     3200   .63 0     
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i true 1 wit inspect 8.8 9.2 160 100 .48 1.4    - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 450    400    7000 0   0      timeout 0 --- inspect 960     800     3300   .66 .0041
loop-invgen/half_2_true-unreach-call_true-termination.i true 1 wit inspect 45   45   280 770 .52 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 870    850    7000 0   0      timeout 0 --- inspect 960     800     1500   .63 0     
loop-invgen/heapsort_true-unreach-call_true-termination.i unknown 0 --- inspect 180   180   190 2400 .87 1.7    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .031 .031 5.6 0    0     
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 8.5 8.5 130 120 .50 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.7  290 0   0      true 2 --- inspect 8.1   4.6   310   .62 0     
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 34   34   160 370 .78 1.7    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.8  290 0   0      true 2 --- inspect 10     6.1   360   .66 0     
loop-invgen/nest-if3_true-unreach-call_true-termination.i unknown 0 --- inspect 110   120   450 1600 .56 2.2    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 40 0   0      error (2) 0 --- inspect .050 .051 5.5 0    0     
loop-invgen/nested6_true-unreach-call_true-termination.i true 2 wit inspect 270   270   390 3000 .84 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2300 0   0      true 2 --- inspect 10     6.1   390   .62 0     
loop-invgen/nested9_true-unreach-call_true-termination.i true 2 wit inspect 180   180   900 2000 .61 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 490    470    7000 0   0      true 2 --- inspect 13     7.3   450   .62 0     
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i unknown 0 --- inspect 220