Tool Pinaka 0.1 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-06 20:14:43 CET 2018-12-07 17:00:25 CET 2018-12-07 18:15:01 CET 2018-12-07 18:51:03 CET 2018-12-12 20:55:30 CET 2018-12-07 16:17:05 CET 2018-12-07 17:47:50 CET
Run set pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-seq-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops uautomizer-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops uautomizer-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops
Options --graphml-witness witness.graphml -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/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pinaka.2018-12-06_2014.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/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pinaka.2018-12-06_2014.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 .35 .35 58 3.4 0      0     false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0   false(unreach-call) 1 --- inspect 9.1   5.4   290   .66 0   unknown 0 --- inspect 4.3  2.5  250 0   0    false(unreach-call) 1 --- inspect .59   .59   20    .057 0      - --- inspect - --- inspect
loops/bubble_sort_false-unreach-call.i timeout 0 --- inspect 900    900    2100 9900   .020  0     error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0   error (invalid witness file) 0 --- inspect 1.3  .82 47 0   0    error (invalid witness file) 0 --- inspect .0052 .0071 .52 0     0      - --- inspect - --- inspect
loops/count_up_down_false-unreach-call_true-termination.i timeout 0 --- inspect 900    900    380 3800   .012  0     error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .038 .039 5.5 0    0   error (invalid witness file) 0 --- inspect 1.0  .68 47 0   0    error (invalid witness file) 0 --- inspect .0014 .0016 .40 0     0      - --- inspect - --- inspect
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.4  4.4  890 69   0      0     false(unreach-call) 1 wit inspect 12    9.1  400 0   0   out of memory 0 --- inspect 72     46     7000   .63 0   true -32 --- inspect 5.9  3.3  260 0   0    error (2) 0 --- inspect .61   .61   21    .037 0      - --- inspect - --- inspect
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .36 .36 58 3.2 0      0     false(unreach-call) 1 wit inspect 4.1  2.2  250 0   0   false(unreach-call) 1 --- inspect 8.2   4.6   320   .66 0   false(unreach-call) 1 --- inspect 5.0  2.9  250 0   0    false(unreach-call) 1 --- inspect .59   .61   20    .049 0      - --- inspect - --- inspect
loops/insertion_sort_false-unreach-call_true-termination.i timeout 0 --- inspect 900    900    680 7000   .012  0     error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .67 47 0   0    error (invalid witness file) 0 --- inspect .0019 .0028 .52 0     0      - --- inspect - --- inspect
loops/invert_string_false-unreach-call_true-termination.i timeout 0 --- inspect 900    900    11000 4900   .012  0     error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .025 .027 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .74 48 0   0    error (invalid witness file) 0 --- inspect .0018 .0023 .54 0     0      - --- inspect - --- inspect
loops/linear_search_false-unreach-call.i false(unreach-call) 1 wit inspect .41 .41 58 3.9 0      0     false(unreach-call) 1 wit inspect 5.5  3.0  270 0   0   false(unreach-call) 1 --- inspect 16     8.8   530   .62 0   unknown 0 --- inspect 4.3  2.5  250 0   0    true -32 --- inspect .58   .58   21    .053 0      - --- inspect - --- inspect
loops/ludcmp_false-unreach-call.i false(unreach-call) 1 wit inspect 1.2  1.2  59 16   0      .057 false(unreach-call) 1 wit inspect 8.3  5.7  510 0   0   true -32 --- inspect 50     37     800   .75 0   false(unreach-call) 1 --- inspect 5.0  2.8  260 0   0    error (2) 0 --- inspect .58   .58   21    .037 0      - --- inspect - --- inspect
loops/matrix_false-unreach-call_true-termination.i error (8) 0 --- inspect .36 .36 58 3.0 0      0     error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .031 .032 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .68 46 0   0    error (invalid witness file) 0 --- inspect .0018 .0024 .65 0     0      - --- inspect - --- inspect
loops/n.c24_false-unreach-call.i error (8) 0 --- inspect 1.5  1.5  120 16   .0082 0     error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .037 .038 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .69 47 0   0    error (invalid witness file) 0 --- inspect .0022 .0029 .53 0     0      - --- inspect - --- inspect
loops/nec11_false-unreach-call_false-termination.i out of memory 0 --- inspect 710    700    15000 11000   .012  0     error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .023 .024 5.8 0    0   error (invalid witness file) 0 --- inspect .95 .61 47 0   0    error (invalid witness file) 0 --- inspect .0017 .0022 .52 0     0      - --- inspect - --- inspect
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.6  1.6  86 20   0      0     false(unreach-call) 1 wit inspect 5.3  3.0  280 0   0   false(unreach-call) 1 --- inspect 7.2   4.5   310   .66 0   unknown 0 --- inspect 4.5  2.6  260 0   0    false(unreach-call) 1 --- inspect .75   .75   20    .061 0      - --- inspect - --- inspect
loops/s3_false-unreach-call.i error (8) 0 --- inspect .93 .93 80 8.5 .0082 0     error (invalid witness file) 0 --- inspect .57 .36 41 0   0   error (2) 0 --- inspect .026 .028 5.6 0    0   error (invalid witness file) 0 --- inspect 1.3  .81 47 0   0    error (invalid witness file) 0 --- inspect .0015 .0020 .41 0     0      - --- inspect - --- inspect
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .41 .41 58 3.6 0      0     false(unreach-call) 1 wit inspect 4.8  2.7  260 0   0   false(unreach-call) 1 --- inspect 19     11     370   .75 0   unknown 0 --- inspect 4.9  2.8  250 0   0    false(unreach-call) 1 --- inspect .60   .60   21    .061 .0041 - --- inspect - --- inspect
loops/sum01_bug02_false-unreach-call_true-termination.i timeout 0 --- inspect 900    900    510 5600   .012  0     error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 47 0   0    error (invalid witness file) 0 --- inspect .0049 .0063 .53 0     0      - --- inspect - --- inspect
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i timeout 0 --- inspect 900    900    500 4200   .012  .057 error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .68 47 0   0    error (invalid witness file) 0 --- inspect .0047 .0058 .53 0     0      - --- inspect - --- inspect
loops/sum01_false-unreach-call_true-termination.i timeout 0 --- inspect 900    900    450 5800   .012  0     error (invalid witness file) 0 --- inspect .59 .35 41 0   0   error (2) 0 --- inspect .028 .029 5.5 0    0   error (invalid witness file) 0 --- inspect 1.2  .81 47 0   0    error (invalid witness file) 0 --- inspect .0053 .0065 .52 0     0      - --- inspect - --- inspect
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .37 .37 58 3.5 0      0     false(unreach-call) 1 wit inspect 4.4  2.4  260 0   0   false(unreach-call) 1 --- inspect 16     9.4   630   .66 0   unknown 0 --- inspect 4.4  2.5  250 0   0    false(unreach-call) 1 --- inspect .58   .58   21    .045 0      - --- inspect - --- inspect
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .38 .38 58 3.0 0      .057 false(unreach-call) 1 wit inspect 5.1  2.8  250 0   0   false(unreach-call) 1 --- inspect 8.0   4.4   290   .66 0   false(unreach-call) 1 --- inspect 4.1  2.4  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
loops/sum_array_false-unreach-call.i timeout 0 --- inspect 900    900    10000 6000   .012  0     error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .90 .60 47 0   0    error (invalid witness file) 0 --- inspect .0020 .0025 .52 0     0      - --- inspect - --- inspect
loops/terminator_01_false-unreach-call_true-termination.i timeout 0 --- inspect 900    900    370 4900   .012  0     error (invalid witness file) 0 --- inspect .60 .37 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 .0046 .0059 .41 0     0      - --- inspect - --- inspect
loops/terminator_02_false-unreach-call_true-termination.i timeout 0 --- inspect 900    900    340 3600   .012  0     error (invalid witness file) 0 --- inspect .61 .39 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .63 49 0   0    error (invalid witness file) 0 --- inspect .0059 .0072 .41 0     0      - --- inspect - --- inspect
loops/terminator_03_false-unreach-call_true-termination.i timeout 0 --- inspect 900    900    7100 3600   .012  0     error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .030 .031 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .73 47 0   0    error (invalid witness file) 0 --- inspect .0041 .0065 .54 0     0      - --- inspect - --- inspect
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .39 .39 58 3.3 0      0     false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0   false(unreach-call) 1 --- inspect 8.1   4.6   310   .66 0   unknown 0 --- inspect 4.8  2.8  250 0   0    false(unreach-call) 1 --- inspect .59   .58   20    .053 0      - --- inspect - --- inspect
loops/trex02_false-unreach-call_true-termination.i timeout 0 --- inspect 900    900    310 5200   .012  0     error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .025 .026 5.5 0    0   error (invalid witness file) 0 --- inspect .98 .64 48 0   0    error (invalid witness file) 0 --- inspect .0046 .0061 .52 0     0      - --- inspect - --- inspect
loops/trex03_false-unreach-call_true-termination.i timeout 0 --- inspect 900    900    340 6000   .012  0     error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .026 .028 5.5 0    0   error (invalid witness file) 0 --- inspect .90 .60 47 0   0    error (invalid witness file) 0 --- inspect .0048 .0058 .52 0     0      - --- inspect - --- inspect
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .39 .39 58 3.2 0      0     true -32 wit inspect 4.1  2.3  250 0   0   false(unreach-call) 1 --- inspect 8.0   4.8   310   .62 0   false(unreach-call) 1 --- inspect 4.7  2.7  250 0   0    error (2) 0 --- inspect .59   .59   20    .037 0      - --- inspect - --- inspect
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .76 .76 61 8.7 .0082 0     false(unreach-call) 1 wit inspect 4.4  2.4  260 0   0   false(unreach-call) 1 --- inspect 16     9.2   530   .62 0   unknown 0 --- inspect 4.0  2.3  250 0   .18 true -32 --- inspect .58   .58   20    .057 0      - --- inspect - --- inspect
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect 7.9  7.9  940 100   0      0     false(unreach-call) 1 wit inspect 5.9  3.6  280 0   0   timeout 0 --- inspect 97     88     560   .66 0   unknown 0 --- inspect 4.8  2.8  260 0   0    false(unreach-call) 1 --- inspect .61   .61   21    .061 0      - --- inspect - --- inspect
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .35 .35 58 3.9 0      0     false(unreach-call) 1 wit inspect 3.6  2.0  250 0   0   false(unreach-call) 1 --- inspect 8.7   5.2   300   .66 0   false(unreach-call) 1 --- inspect 3.9  2.3  250 0   0    false(unreach-call) 1 --- inspect .56   .56   20    .045 0      - --- inspect - --- inspect
loops/array_true-unreach-call_true-termination.i true 2 wit inspect .36 .36 58 2.8 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  290 0   0   true 2 --- inspect 14     8.0   370   .66 0  
loops/bubble_sort_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    9200 4500   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
loops/count_up_down_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    380 3700   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 40 0   0   error (2) 0 --- inspect .026 .028 5.6 0    0  
loops/eureka_01_true-unreach-call.i true 1 wit inspect .41 .41 59 4.7 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5100 0   0   timeout 0 --- inspect 960     920     4100   .68 0  
loops/eureka_05_true-unreach-call_true-termination.i true 1 wit inspect .39 .39 58 3.3 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3600 0   0   timeout 0 --- inspect 960     920     1300   .63 0  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i out of memory 0 --- inspect 450    450    15000 5600   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i out of memory 0 --- inspect 460    460    15000 6400   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 41 0   0   error (2) 0 --- inspect .026 .028 5.7 0    0  
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    560 6200   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .35 .35 58 3.1 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    13    500 0   0   true 2 --- inspect 320     300     1000   .62 0  
loops/linear_sea.ch_true-unreach-call.i out of memory 0 --- inspect 840    830    15000 4300   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
loops/lu.cmp_true-unreach-call.i true 2 wit inspect 8.1  8.1  59 110   0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 93    84    7000 0   0   true 2 --- inspect 15     8.4   410   .66 0  
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect .37 .37 58 3.5 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  290 0   0   true 2 --- inspect 12     6.9   440   .66 0  
loops/n.c11_true-unreach-call_false-termination.i timeout 0 --- inspect 900    900    1200 13000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 42 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .35 .35 58 3.1 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  280 0   0   true 2 --- inspect 8.3   4.7   310   .62 0  
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .36 .36 58 2.9 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.9  280 0   0   true 2 --- inspect 9.5   5.3   310   .66 0  
loops/string_true-unreach-call_true-termination.i true 2 wit inspect .54 .55 59 5.8 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.5  3.0  290 0   0   true 2 --- inspect 13     7.4   410   .62 0  
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 38    38    13000 490   0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 410    400    7000 0   0   true 2 --- inspect 12     7.5   400   .66 0  
loops/sum03_true-unreach-call_false-termination.i out of memory 0 --- inspect 660    660    15000 8500   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect .37 .37 58 3.0 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.0  2.7  280 0   0   true 2 --- inspect 11     7.0   430   .62 0  
loops/sum_array_true-unreach-call.i out of memory 0 --- inspect 37    37    15000 540   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
loops/terminator_02_true-unreach-call_true-termination.i out of memory 0 --- inspect 250    250    15000 3300   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 40 0   0   error (2) 0 --- inspect .027 .028 5.5 0    0  
loops/terminator_03_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    7700 4400   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0  
loops/trex01_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    470 4200   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0  
loops/trex02_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    310 3900   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0  
loops/trex03_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    330 4800   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
loops/trex04_true-unreach-call_false-termination.i timeout 0 --- inspect 900    900    370 4100   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect .37 .38 58 3.0 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  270 0   0   true 2 --- inspect 13     6.9   340   .62 0  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect 30    30    2500 390   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.8  4.2  370 0   0   true 2 --- inspect 10     5.9   310   .62 0  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect .37 .38 59 4.4 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  280 0   0   true 2 --- inspect 9.0   5.4   310   .66 0  
loops/vogal_true-unreach-call.i true 2 wit inspect 1.6  1.6  170 17   0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 62    50    970 0   0   timeout 0 --- inspect 960     940     870   .68 0  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i out of memory 0 --- inspect 98    97    15000 1000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .027 .028 5.5 0    0  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i out of memory 0 --- inspect 97    96    15000 1100   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 40 0   0   error (2) 0 --- inspect .026 .028 5.6 0    0  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i out of memory 0 --- inspect 370    370    15000 4500   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0  
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 2.2  2.2  65 26   0      0     timeout 0 wit inspect 97    86    1000 0   0   timeout 0 --- inspect 97     62     7000   .65 0   false(unreach-call) 1 --- inspect 27    14    680 0   0    false(unreach-call) 1 --- inspect 1.2    1.2    32    .061 0      - --- inspect - --- inspect
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 5.5  5.5  95 75   0      0     timeout 0 wit inspect 98    78    1700 0   0   out of memory 0 --- inspect 83     54     7000   .63 0   false(unreach-call) 1 --- inspect 64    41    1400 0   0    false(unreach-call) 1 --- inspect 2.4    2.4    55    .086 0      - --- inspect - --- inspect
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect 5.8  5.8  130 79   0      0     timeout 0 wit inspect 97    85    1000 0   0   out of memory 0 --- inspect 80     51     7000   .63 0   unknown 0 --- inspect 24    13    650 0   0    false(unreach-call) 1 --- inspect 1.2    1.2    32    .082 0      - --- inspect - --- inspect
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect 2.0  2.0  59 24   0      0     false(unreach-call) 1 wit inspect 23    12    920 0   0   timeout 0 --- inspect 98     76     6300   .68 0   false(unreach-call) 1 --- inspect 23    13    630 0   0    false(unreach-call) 1 --- inspect 1.2    1.2    36    .045 0      - --- inspect - --- inspect
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect .44 .44 58 3.9 0      0     false(unreach-call) 1 wit inspect 6.9  3.8  280 0   0   timeout 0 --- inspect 98     59     6700   .64 0   false(unreach-call) 1 --- inspect 5.2  2.9  270 0   0    false(unreach-call) 1 --- inspect .61   .61   22    .045 0      - --- inspect - --- inspect
loop-acceleration/functions_false-unreach-call1_true-termination.i out of memory 0 --- inspect 680    680    15000 8800   .0041 0     error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 47 0   0    error (invalid witness file) 0 --- inspect .0042 .0054 .53 0     0      - --- inspect - --- inspect
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 2.2  2.2  79 22   0      0     false(unreach-call) 1 wit inspect 3.7  2.0  250 0   0   false(unreach-call) 1 --- inspect 8.3   4.9   310   .62 0   false(unreach-call) 1 --- inspect 4.5  2.6  250 0   0    false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
loop-acceleration/nested_false-unreach-call1.i out of memory 0 --- inspect 810    810    15000 13000   .012  0     error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .028 .028 5.5 0    0   error (invalid witness file) 0 --- inspect 1.1  .74 47 0   0    error (invalid witness file) 0 --- inspect .0048 .0053 .40 0     0      - --- inspect - --- inspect
loop-acceleration/phases_false-unreach-call1.i out of memory 0 --- inspect 800    800    15000 10000   .012  0     error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .91 .59 46 0   0    error (invalid witness file) 0 --- inspect .0017 .0028 .53 0     0      - --- inspect - --- inspect
loop-acceleration/phases_false-unreach-call2_false-termination.i out of memory 0 --- inspect 300    300    15000 3700   .0041 0     error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .027 .028 5.7 0    0   error (invalid witness file) 0 --- inspect .97 .63 47 0   0    error (invalid witness file) 0 --- inspect .0019 .0026 .53 0     0      - --- inspect - --- inspect
loop-acceleration/simple_false-unreach-call1.i out of memory 0 --- inspect 800    800    15000 11000   .012  0     error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .026 .027 5.7 0    0   error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0    error (invalid witness file) 0 --- inspect .0019 .0034 .40 0     0      - --- inspect - --- inspect
loop-acceleration/simple_false-unreach-call2_true-termination.i timeout 0 --- inspect 900    900    380 3900   .012  0     error (invalid witness file) 0 --- inspect .61 .37 42 0   0   error (2) 0 --- inspect .025 .027 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0    error (invalid witness file) 0 --- inspect .0014 .0018 .52 0     0      - --- inspect - --- inspect
loop-acceleration/simple_false-unreach-call3_true-termination.i timeout 0 --- inspect 900    900    410 5100   .012  0     error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 49 0   0    error (invalid witness file) 0 --- inspect .0047 .0055 .39 0     0      - --- inspect - --- inspect
loop-acceleration/simple_false-unreach-call4.i out of memory 0 --- inspect 820    820    15000 11000   .012  0     error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .74 47 0   0    error (invalid witness file) 0 --- inspect .0059 .0074 .53 0     0      - --- inspect - --- inspect
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .35 .35 58 4.3 0      0     false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0   false(unreach-call) 1 --- inspect 12     6.7   390   .66 0   false(unreach-call) 1 --- inspect 4.3  2.5  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .36 .36 58 3.4 0      0     false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0   false(unreach-call) 1 --- inspect 11     6.9   380   .66 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0    false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect .73 .73 58 9.3 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  280 0   0   true 2 --- inspect 12     8.2   340   .66 0  
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect 1.5  1.5  58 17   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    900    5000 0   0   timeout 0 --- inspect 960     930     790   .64 0  
loop-acceleration/array_true-unreach-call3_true-termination.i true 2 wit inspect 33    33    13000 420   0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  280 0   0   true 2 --- inspect 11     6.4   380   .66 0  
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 32    32    12000 460   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    6200 0   0   timeout 0 --- inspect 960     930     930   .65 0  
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect .68 .69 58 7.5 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  270 0   0   true 2 --- inspect 9.3   5.3   320   .62 0  
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect .45 .45 59 4.4 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    12    570 0   0   timeout 0 --- inspect 960     940     660   .80 0  
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect .38 .39 60 4.3 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.4  4.2  320 0   0   true 2 --- inspect 260     250     670   .62 0  
loop-acceleration/functions_true-unreach-call1_true-termination.i out of memory 0 --- inspect 680    680    15000 7900   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .41 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
loop-acceleration/multivar_true-unreach-call1_true-termination.i out of memory 0 --- inspect 42    42    15000 590   .041  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .35 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
loop-acceleration/nested_true-unreach-call1.i out of memory 0 --- inspect 800    800    15000 10000   .025  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0  
loop-acceleration/overflow_true-unreach-call1.i out of memory 0 --- inspect 790    790    15000 11000   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0  
loop-acceleration/phases_true-unreach-call1.i out of memory 0 --- inspect 800    800    15000 10000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .020 .022 5.6 0    0  
loop-acceleration/phases_true-unreach-call2_false-termination.i out of memory 0 --- inspect 300    300    15000 3700   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .026 .028 5.6 0    0  
loop-acceleration/simple_true-unreach-call1.i out of memory 0 --- inspect 790    790    15000 12000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0  
loop-acceleration/simple_true-unreach-call2_true-termination.i timeout 0 --- inspect 900    900    380 4000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
loop-acceleration/simple_true-unreach-call3_true-termination.i timeout 0 --- inspect 900    900    400 4200   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0  
loop-acceleration/simple_true-unreach-call4.i out of memory 0 --- inspect 820    820    15000 12000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect .36 .36 58 3.3 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.7  5.3  390 0   0   true 2 --- inspect 24     19     440   .62 0  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect .38 .38 58 3.0 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  280 0   0   true 2 --- inspect 9.2   5.3   320   .66 0  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i timeout 0 --- inspect 900    900    2500 7900   .012  0     error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0   error (invalid witness file) 0 --- inspect 1.2  .83 47 0   0    error (invalid witness file) 0 --- inspect .0034 .0044 .54 0     0      - --- inspect - --- inspect
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i true 1 wit inspect .98 .98 59 13   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4300 0   0   timeout 0 --- inspect 960     940     720   .63 0  
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i out of memory 0 --- inspect 41    41    15000 610   .045  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 41 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0  
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i true 1 wit inspect 12    12    230 150   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6200 0   0   timeout 0 --- inspect 960     940     770   1.5  0  
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i error (139) 0 --- inspect 5.4  5.4  2000 64   0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i out of memory 0 --- inspect 760    760    15000 8900   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 40 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i out of memory 0 --- inspect 780    780    15000 9300   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+lhb-reducer.c error (139) 0 --- inspect 3.8  3.8  1100 44   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0  
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+nlh-reducer.c error (139) 0 --- inspect 3.7  3.7  1100 44   .0041 .057 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 40 0   0   error (2) 0 --- inspect .027 .029 5.6 0    0  
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .36 .36 58 3.1 0      0     false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0   false(unreach-call) 1 --- inspect 7.0   4.4   300   .66 0   false(unreach-call) 1 --- inspect 4.6  2.6  250 0   0    false(unreach-call) 1 --- inspect .60   .60   20    .053 0      - --- inspect - --- inspect
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i out of memory 0 --- inspect 140    140    15000 1500   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0  
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i out of memory 0 --- inspect 40    39    15000 550   .049  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 41 0   0   error (2) 0 --- inspect .026 .027 5.7 0    0  
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i out of memory 0 --- inspect 43    43    15000 620   .045  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0   error (2) 0 --- inspect .025 .027 5.6 0    0  
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i out of memory 0 --- inspect 78    77    15000 1000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 40 0   0   error (2) 0 --- inspect .026 .027 5.8 0    0  
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i out of memory 0 --- inspect 53    53    15000 690   .045  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 42 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0  
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    400 4700   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .34 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0  
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    680 12000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0  
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    380 4400   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0  
loop-invgen/heapsort_true-unreach-call_true-termination.i out of memory 0 --- inspect 48    47    15000 660   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
loop-invgen/id_build_true-unreach-call_true-termination.i out of memory 0 --- inspect 44    43    15000 550   .053  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .027 .028 5.5 0    0  
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect .44 .44 64 3.7 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  2.9  290 0   0   true 2 --- inspect 13     7.8   360   .62 0  
loop-invgen/nest-if3_true-unreach-call_true-termination.i out of memory 0 --- inspect 82    81    15000 1200   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
loop-invgen/nested6_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    410 4400   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
loop-invgen/nested9_true-unreach-call_true-termination.i out of memory 0 --- inspect 45    44    15000 530   .037  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 42 0   0   error (2) 0 --- inspect .021 .022 5.8 0    0  
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i out of memory 0 --- inspect 43    42    15000 570   .053  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    370 3900   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
loop-invgen/string_concat-noarr_true-unreach-call_false-termination.i timeout 0 --- inspect 900    900    670 12000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 42 0   0   error (2) 0 --- inspect .026 .028 5.7 0    0  
loop-invgen/up_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    400 3900   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .020 .022 5.7 0    0  
loop-invgen/SpamAssassin-loop_true-unreach-call.i.v+cfa-reducer.c out of memory 0 --- inspect 49    48    15000 650   .053  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0  
loop-invgen/apache-escape-absolute_true-unreach-call.i.v+cfa-reducer.c out of memory 0 --- inspect 72    71    15000 1200   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
loop-invgen/apache-get-tag_true-unreach-call.i.p+lhb-reducer.c out of memory 0 --- inspect 70    70    15000 890   .025  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
loop-invgen/apache-get-tag_true-unreach-call.i.p+nlh-reducer.c out of memory 0 --- inspect 68    67    15000 840   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
loop-invgen/apache-get-tag_true-unreach-call.i.p+sep-reducer.c out of memory 0 --- inspect 73    73    15000 1000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0   error (2) 0 --- inspect .023 .024 5.7 0    0  
loop-invgen/apache-get-tag_true-unreach-call.i.v+lhb-reducer.c out of memory 0 --- inspect 67    67    15000 990   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 42 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
loop-invgen/apache-get-tag_true-unreach-call.i.v+nlh-reducer.c out of memory 0 --- inspect 67    67    15000 1000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .026 .026 5.5 0    0  
loop-invgen/id_build_true-unreach-call.i.p+nlh-reducer.c out of memory 0 --- inspect 42    41    15000 650   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0   error (2) 0 --- inspect .025 .027 5.7 0    0  
loop-invgen/id_build_true-unreach-call.i.p+sep-reducer.c out of memory 0 --- inspect 42    41    15000 640   .045  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .022 .024 5.7 0    0  
loop-invgen/id_build_true-unreach-call.i.v+lhb-reducer.c out of memory 0 --- inspect 41    40    15000 470   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 42 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0  
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 wit inspect 19    19    6300 280   0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 370    360    7000 0   0   true 2 --- inspect 10     6.1   310   .66 0  
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 0 --- inspect 900    900    440 8100   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .026 .028 5.7 0    0  
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .39 .39 58 3.1 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.6  280 0   0   true 2 --- inspect 10     5.7   330   .66 0  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 0 --- inspect 900    900    460 4000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0  
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect .41 .41 58 3.9 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  280 0   0   true 2 --- inspect 8.7   4.9   310   .66 0  
loop-lit/css2003_true-unreach-call_true-termination.c.i out of memory 0 --- inspect 43    43    15000 460   .061  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
loop-lit/ddlm2013_true-unreach-call.i timeout 0 --- inspect 900    900    890 12000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .36 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect .42 .42 58 3.3 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 73    64    800 0   0   true 2 --- inspect 110     71     940   .62 0  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout 0 --- inspect 900    900    480 7900   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect .40 .41 58 3.6 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 120    110    1100 0   0   true 2 --- inspect 110     79     1200   .62 0  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i timeout 0 --- inspect 900    900    8000 4900   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0  
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 0 --- inspect 900    900    460 5000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
loop-lit/jm2006_true-unreach-call_true-termination.c.i timeout 0 --- inspect 900    900    500 7400   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0   error (2) 0 --- inspect .022 .023 5.8 0    0  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 0 --- inspect 900    900    490 3600   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0  
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i out of memory 0 --- inspect 700    700    15000 9400   .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .37 41 0   0   error (2) 0 --- inspect .026 .029 5.6 0    0  
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .86 .86 58 10   0      0     false(unreach-call) 1 wit inspect 9.0  4.9  370 0   0   false(unreach-call) 1 --- inspect 15     8.2   540   .66 0   unknown 0 --- inspect 7.8  4.3  300 0   0    false(unreach-call) 1 --- inspect .73   .74   23    .061 0      - --- inspect - --- inspect
loop-lit/gj2007_true-unreach-call.c.i.p+lhb-reducer.c true 2 wit inspect .38 .38 59 3.7 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 59    50    790 0   0   true 2 --- inspect 100     68     1100   .62 0  
loop-lit/gj2007_true-unreach-call.c.i.p+nlh-reducer.c true 2 wit inspect .43 .43 63 3.4 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    9.9  480 0   0   true 2 --- inspect 140     93     1100   .62 0  
loop-lit/gsv2008_true-unreach-call.c.i.p+cfa-reducer.c timeout 0 --- inspect 900    900    7700 4300   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
loop-lit/gsv2008_true-unreach-call.c.i.v+cfa-reducer.c timeout 0 --- inspect 900    900    8100 5800   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 43 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0  
loop-lit/gsv2008_true-unreach-call.c.i.v+lhb-reducer.c timeout 0 --- inspect 900    900    8000 4400   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0   error (2) 0 --- inspect .020 .022 5.6 0    0  
loop-lit/jm2006_true-unreach-call.c.i.v+cfa-reducer.c timeout 0 --- inspect 900    900    630 6400   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0  
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect 170    170    3700 2500   0      .057 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  280 0   0   true 2 --- inspect 9.0   5.5   310   .62 0  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect 220    220    7400 2600   0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  270 0   0   true 2 --- inspect 12     6.5   330   .66 0  
loop-new/count_by_2_true-unreach-call_true-termination.i true 1 wit inspect 87    87    1900 1000   0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 360    350    7000 0   0   timeout 0 --- inspect 960     780     1600   .64 0  
loop-new/count_by_k_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    8700 6600   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
loop-new/count_by_nondet_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    4900 12000   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
loop-new/gauss_sum_true-unreach-call_true-termination.i true 1 wit inspect 42    42    15000 580   0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5100 0   0   timeout 0 --- inspect 960     830     960   .63 0  
loop-new/half_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    360 5900   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
loop-new/nested_true-unreach-call_true-termination.i timeout 0 --- inspect 900    900    10000 9800   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
loop-new/gauss_sum_true-unreach-call.i.p+cfa-reducer.c true 1 wit inspect 44    44    15000 540   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5100 0   0   timeout 0 --- inspect 960     880     750   .63 0  
loop-new/gauss_sum_true-unreach-call.i.p+lhb-reducer.c true 1 wit inspect 44    44    15000 730   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5100 0   0   timeout 0 --- inspect 960     860     980   .62 0  
loop-new/gauss_sum_true-unreach-call.i.v+cfa-reducer.c true 1 wit inspect 44    44    15000 570   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5100 0   0   timeout 0 --- inspect 960     880     750   .63 0  
loop-industry-pattern/aiob_1_true-unreach-call.c error (8) 0 --- inspect 1.1  1.1  70 9.6 .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0  
loop-industry-pattern/aiob_2_true-unreach-call.c error (8) 0 --- inspect 1.1  1.1  70 9.3 .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .030 .032 5.5 0    0  
loop-industry-pattern/aiob_3_true-unreach-call.c error (8) 0 --- inspect 1.1  1.1  70 10   .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0  
loop-industry-pattern/aiob_4_true-unreach-call.c error (8) 0 --- inspect 1.1  1.1  70 9.2 .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
loop-industry-pattern/aiob_4_true-unreach-call.c.v+cfa-reducer.c error (8) 0 --- inspect 1.1  1.1  70 9.7 .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .028 .029 5.7 0    0  
loop-industry-pattern/aiob_4_true-unreach-call.c.v+lh-reducer.c error (8) 0 --- inspect 1.1  1.1  70 11   .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0  
loop-industry-pattern/aiob_4_true-unreach-call.c.v+lhb-reducer.c error (8) 0 --- inspect 1.2  1.1  74 13   .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0  
loop-industry-pattern/aiob_4_true-unreach-call.c.v+nlh-reducer.c error (8) 0 --- inspect 1.4  1.4  100 11   .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0  
loop-industry-pattern/mod3_true-unreach-call.c out of memory 0 --- inspect 630    630    15000 7700   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
loop-industry-pattern/mod3_true-unreach-call.c.v+cfa-reducer.c out of memory 0 --- inspect 630    620    15000 7500   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0  
loop-industry-pattern/mod3_true-unreach-call.c.v+lhb-reducer.c out of memory 0 --- inspect 630    630    15000 8100   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
loop-industry-pattern/mod3_true-unreach-call.c.v+sep-reducer.c out of memory 0 --- inspect 630    630    15000 8400   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
loop-industry-pattern/nested_true-unreach-call.c out of memory 0 --- inspect 190    190    15000 2500   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0  
loop-industry-pattern/ofuf_1_true-unreach-call.c error (8) 0 --- inspect .79 .78 71 9.1 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0  
loop-industry-pattern/ofuf_2_true-unreach-call.c error (8) 0 --- inspect .82 .82 71 6.8 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .34 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
loop-industry-pattern/ofuf_3_true-unreach-call.c error (8) 0 --- inspect .81 .81 71 7.2 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
loop-industry-pattern/ofuf_4_true-unreach-call.c error (8) 0 --- inspect .80 .80 71 7.0 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
loop-industry-pattern/ofuf_5_true-unreach-call.c error (8) 0 --- inspect .77 .77 71 9.9 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .023 .024 5.7 0    0  
loops/heavy_true-unreach-call.c timeout 0 --- inspect 900    900    14000 11000   .016  .057 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
loops/compact_false-unreach-call.c out of memory 0 --- inspect 150    150    15000 1400   .016  0     error (invalid witness file) 0 --- inspect .61 .38 40 0   0   error (2) 0 --- inspect .025 .027 5.7 0    0   error (invalid witness file) 0 --- inspect 1.1  .71 47 0   0    error (invalid witness file) 0 --- inspect .0020 .0026 .53 0     0      - --- inspect - --- inspect
loops/heavy_false-unreach-call.c timeout 0 --- inspect 900    900    14000 12000   .016  0     error (invalid witness file) 0 --- inspect .62 .41 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 47 0   0    error (invalid witness file) 0 --- inspect .0045 .0057 .40 0     0      - --- inspect - --- inspect
loops-crafted-1/Mono1_false-unreach-call1.c out of memory 0 --- inspect 530    530    15000 7200   .0082 0     error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .91 .61 46 0   0    error (invalid witness file) 0 --- inspect .0024 .0028 .39 0     0      - --- inspect - --- inspect
loops-crafted-1/Mono3_false-unreach-call1.c timeout 0 --- inspect 900    900    12000 10000   .016  0     error (invalid witness file) 0 --- inspect .75 .48 40 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.3  .81 47 0   0    error (invalid witness file) 0 --- inspect .0065 .0084 .53 0     0      - --- inspect - --- inspect
loops-crafted-1/Mono4_false-unreach-call1.c timeout 0 --- inspect 900    900    13000 13000   .016  0     error (invalid witness file) 0 --- inspect .61 .37 42 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 47 0   0    error (invalid witness file) 0 --- inspect .0050 .0064 .53 0     0      - --- inspect - --- inspect
loops-crafted-1/Mono5_false-unreach-call1.c out of memory 0 --- inspect 740    730    15000 8500   .016  0     error (invalid witness file) 0 --- inspect .57 .36 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .67 48 0   0    error (invalid witness file) 0 --- inspect .0058 .0079 .53 0     0      - --- inspect - --- inspect
loops-crafted-1/Mono6_false-unreach-call1.c out of memory 0 --- inspect 730    730    15000 8600   .016  0     error (invalid witness file) 0 --- inspect .65 .40 41 0   0   error (2) 0 --- inspect .023 .025 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .70 47 0   0    error (invalid witness file) 0 --- inspect .0032 .0041 .53 0     0      - --- inspect - --- inspect
loops-crafted-1/nested3_false-unreach-call.c out of memory 0 --- inspect 760    760    15000 9000   .016  0     error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0    error (invalid witness file) 0 --- inspect .0018 .0023 .40 0     0      - --- inspect - --- inspect
loops-crafted-1/nested5_false-unreach-call.c out of memory 0 --- inspect 730    730    15000 9300   .016  0     error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .021 .021 5.7 0    0   error (invalid witness file) 0 --- inspect .99 .65 47 0   0    error (invalid witness file) 0 --- inspect .0064 .0086 .53 0     0      - --- inspect - --- inspect
loops-crafted-1/Mono1_true-unreach-call1.c out of memory 0 --- inspect 530    530    15000 7500   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .027 .028 5.5 0    0  
loops-crafted-1/nested3_true-unreach-call.c out of memory 0 --- inspect 770    770    15000 9500   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
loops-crafted-1/nested5_true-unreach-call.c out of memory 0 --- inspect 700    700    15000 9800   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 40 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
loop-invariants/bin-suffix-5_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 0 --- inspect 900    900    630 12000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0  
loop-invariants/const_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 0 --- inspect 900    900    620 13000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0  
loop-invariants/eq1_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 0 --- inspect 900    900    490 5900   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0  
loop-invariants/eq2_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 0 --- inspect 900    900    500 4600   .016  .057 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .027 .027 5.5 0    0  
loop-invariants/even_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 0 --- inspect 900    900    630 12000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
loop-invariants/mod4_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 0 --- inspect 900    900    630 15000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0   error (2) 0 --- inspect .026 .028 5.7 0    0  
loop-invariants/odd_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 0 --- inspect 900    900    630 14000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0  
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)
total 208 95 81000 81000 1300000 750000 2.4    .40  59 -12 440   340   12000 0   0   59 -16 850 580 49000 16    0   59 -19 270   160   10000 0   .18 59 -45 18   18   590 1.3  .0041 149 54 11000 11000 94000 0   0   149 56 14000 13000 30000 27 0  
    correct results 54 84 570 570 50000 7300 .025  .17  20 20 130   73   6400 0   0   16 16 180 100 6100 10    0   13 13 160   93   5300 0   0    19 19 15   15   470 1.1  .0041 27 54 470 360 11000 0   0   28 56 1300 1000 14000 18 0  
        correct true 30 60 530 530 47000 6800 .016  .057 0 0 0 0 27 54 470 360 11000 0   0   28 56 1300 1000 14000 18 0  
        correct false 24 24 39 39 3300 490 .0082 .11  20 20 130   73   6400 0   0   16 16 180 100 6100 10    0   13 13 160   93   5300 0   0    19 19 15   15   470 1.1  .0041 0 0
    correct-unconfimed results 11 11 310 310 74000 4100 .012  0     0 0 0 0 0 0
        correct-unconfirmed true 11 11 310 310 74000 4100 .012  0     0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 1 -32 4.1 2.3 250 0   0   1 -32 50 37 800 .75 0   1 -32 5.9 3.3 260 0   0    2 -64 1.2 1.2 41 .11 0      0 0
        incorrect true 0 1 -32 4.1 2.3 250 0   0   1 -32 50 37 800 .75 0   1 -32 5.9 3.3 260 0   0    2 -64 1.2 1.2 41 .11 0      0 0
        incorrect false 0 0 0 0 0 0 0
score (208 tasks, max score: 357) 95 -12 -16 -19 -45 54 56
Run set pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-seq-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops uautomizer-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops uautomizer-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops