Tool symbiotic 6.0.3-77d4af47 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-07 21:42:05 CET 2018-12-08 23:40:56 CET 2018-12-09 00:46:04 CET 2018-12-09 01:29:54 CET 2018-12-12 21:10:03 CET 2018-12-08 22:46:12 CET 2018-12-08 23:47:25 CET
Run set symbiotic.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other] cpa-seq-validate-violation-witnesses-symbiotic.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other] uautomizer-validate-violation-witnesses-symbiotic.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other] cpa-witness2test-validate-violation-witnesses-symbiotic.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows] fshell-witness2test-validate-violation-witnesses-symbiotic.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows] cpa-seq-validate-correctness-witnesses-symbiotic.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] uautomizer-validate-correctness-witnesses-symbiotic.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows]
Options --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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i unreach-call false(unreach-call) 1 1.3   1.3   110 17    0      0      timeout 0 97    76    2600 0      .0041 true -32 7.9   4.5   310   .66  0   false(unreach-call) 1 3.6  2.1  240 0      0      false(unreach-call) 1 .68   .68   20    .049 0      - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call probably out of memory (killed (signal 9, verification)) 0 290     300     15000 4000    .074  0      error (invalid witness file) 0 .70 .43 41 0      0      error (2) 0 .021 .024 5.7 0     0   error (invalid witness file) 0 1.0  .68 49 0      0      error (invalid witness file) 0 .0050 .0062 .53 0     0      - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call probably out of memory (killed (signal 9, verification)) 0 290     300     15000 4000    .12   0      error (invalid witness file) 0 .58 .37 41 0      0      error (2) 0 .021 .023 5.6 0     0   error (invalid witness file) 0 .95 .62 47 0      0      error (invalid witness file) 0 .0016 .0022 .52 0     0      - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call probably out of memory (killed (signal 9, verification)) 0 350     360     15000 5200    .066  0      error (invalid witness file) 0 .68 .42 41 0      0      error (2) 0 .022 .025 5.7 0     0   error (invalid witness file) 0 .95 .60 47 0      0      error (invalid witness file) 0 .0017 .0022 .52 0     0      - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call probably out of memory (killed (signal 9, verification)) 0 350     360     15000 5200    .11   0      error (invalid witness file) 0 .70 .42 40 0      0      error (2) 0 .022 .023 5.6 0     0   error (invalid witness file) 0 .94 .64 47 0      0      error (invalid witness file) 0 .0054 .0064 .53 0     0      - -
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call false(unreach-call) 1 .17  .17  16 1.8  0      0      timeout 0 98    83    2000 0      .0041 true -32 7.5   4.2   300   .62  0   false(unreach-call) 1 15    14    250 0      0      false(unreach-call) 1 12      12      20    .045 0      - -
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call false(unreach-call) 1 6.6   6.6   410 87    0      0      timeout 0 98    84    2000 0      .0041 true -32 8.3   4.5   310   .62  0   true -32 3.3  2.0  250 0      .0041 false(unreach-call) 1 .57   .57   20    .049 0      - -
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call false(unreach-call) 1 8.7   8.7   520 120    0      0      timeout 0 97    84    2000 0      .0041 true -32 6.7   4.2   300   .62  0   true -32 3.4  2.0  240 0      0      false(unreach-call) 1 .57   .57   20    .049 0      - -
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call false(unreach-call) 1 9.7   9.7   590 140    0      0      timeout 0 97    83    2000 0      0      true -32 7.0   3.9   300   .62  0   true -32 3.5  2.1  250 0      .0041 false(unreach-call) 1 .58   .59   20    .049 0      - -
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call false(unreach-call) 1 11     11     650 150    0      0      timeout 0 97    84    2000 0      0      true -32 7.3   4.6   310   .62  0   true -32 4.4  2.6  240 0      0      false(unreach-call) 1 .58   .58   20    .049 0      - -
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call false(unreach-call) 1 12     12     730 170    0      0      timeout 0 98    85    2000 0      0      true -32 7.2   4.1   310   .62  0   true -32 3.6  2.1  250 0      0      false(unreach-call) 1 .58   .58   20    .049 0      - -
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call false(unreach-call) 1 13     13     820 150    0      0      timeout 0 97    84    2100 0      0      true -32 7.1   4.5   310   .62  0   true -32 3.6  2.1  250 0      0      false(unreach-call) 1 .58   .58   20    .049 0      - -
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call false(unreach-call) 1 13     13     910 180    0      0      timeout 0 97    83    2200 0      0      true -32 7.6   4.3   300   .62  0   true -32 3.8  2.2  250 0      0      false(unreach-call) 1 .58   .59   20    .053 .0041 - -
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call false(unreach-call) 1 15     15     1000 190    0      0      timeout 0 97    83    2100 0      0      true -32 7.6   4.3   310   .62  0   true -32 3.8  2.2  250 0      0      false(unreach-call) 1 .61   .61   20    .057 0      - -
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call false(unreach-call) 1 16     16     1100 210    0      0      timeout 0 98    83    2100 0      0      true -32 7.4   4.2   300   .62  0   true -32 3.6  2.1  250 0      0      false(unreach-call) 1 .59   .59   20    .057 .0041 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call false(unreach-call) 1 2.1   2.1   250 31    0      0      timeout 0 97    88    1100 0      0      true -32 7.3   4.6   320   .62  0   false(unreach-call) 1 3.6  2.1  250 0      0      false(unreach-call) 1 .59   .59   20    .045 0      - -
array-examples/standard_init1_false-unreach-call_ground.i unreach-call false(unreach-call) 1 .77  .77  100 11    0      0      timeout 0 97    87    910 0      0      true -32 7.4   4.6   300   .62  0   false(unreach-call) 1 3.5  2.1  250 0      0      false(unreach-call) 1 .56   .56   20    .045 0      - -
array-examples/standard_init2_false-unreach-call_ground.i unreach-call false(unreach-call) 1 1.4   1.4   190 24    0      0      timeout 0 97    87    960 0      0      true -32 6.9   3.9   310   .62  0   false(unreach-call) 1 3.5  2.0  240 0      0      false(unreach-call) 1 .57   .57   20    .045 0      - -
array-examples/standard_init3_false-unreach-call_ground.i unreach-call false(unreach-call) 1 2.0   2.0   280 31    0      0      timeout 0 97    88    980 0      0      true -32 7.1   4.5   310   .62  0   false(unreach-call) 1 4.2  2.5  240 0      0      false(unreach-call) 1 .58   .57   20    .045 .0041 - -
array-examples/standard_init4_false-unreach-call_ground.i unreach-call false(unreach-call) 1 2.6   2.6   370 38    0      0      timeout 0 97    88    1100 0      0      true -32 6.6   4.1   300   .62  0   false(unreach-call) 1 3.5  2.0  250 0      0      false(unreach-call) 1 .57   .57   20    .045 0      - -
array-examples/standard_init5_false-unreach-call_ground.i unreach-call false(unreach-call) 1 3.2   3.2   460 46    0      0      timeout 0 97    86    900 0      0      true -32 7.0   4.0   300   .62  0   false(unreach-call) 1 3.5  2.1  250 0      0      false(unreach-call) 1 .60   .61   20    .045 0      - -
array-examples/standard_init6_false-unreach-call_ground.i unreach-call false(unreach-call) 1 3.8   3.8   540 51    0      0      timeout 0 97    87    980 0      0      true -32 7.3   4.6   300   .62  0   false(unreach-call) 1 3.6  2.1  240 0      0      false(unreach-call) 1 .58   .58   20    .045 .0041 - -
array-examples/standard_init7_false-unreach-call_ground.i unreach-call false(unreach-call) 1 4.5   4.5   630 66    0      0      timeout 0 97    87    1100 0      0      true -32 7.4   4.7   310   .62  0   false(unreach-call) 1 3.6  2.1  250 0      0      false(unreach-call) 1 .57   .57   20    .045 0      - -
array-examples/standard_init8_false-unreach-call_ground.i unreach-call false(unreach-call) 1 5.1   5.1   720 70    0      0      timeout 0 97    88    1100 0      0      true -32 7.5   4.2   310   .62  0   false(unreach-call) 1 3.6  2.1  250 0      .0041 false(unreach-call) 1 .58   .58   20    .045 0      - -
array-examples/standard_init9_false-unreach-call_ground.i unreach-call false(unreach-call) 1 5.6   5.6   810 90    0      0      timeout 0 97    87    1100 0      0      true -32 7.4   4.3   310   .62  0   false(unreach-call) 1 3.6  2.1  240 0      0      false(unreach-call) 1 .56   .56   20    .045 0      - -
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call false(unreach-call) 1 .99  .98  100 12    0      0      timeout 0 97    83    2000 0      0      true -32 7.4   4.2   320   .62  0   false(unreach-call) 1 3.4  2.0  250 0      0      false(unreach-call) 1 .59   .59   20    .045 0      - -
array-examples/standard_partition_false-unreach-call_ground.i unreach-call timeout (verification) 0 900     900     2800 7700    .020  0      error (invalid witness file) 0 .60 .36 42 0      0      error (2) 0 .021 .022 5.8 0     0   error (invalid witness file) 0 1.1  .73 46 0      0      error (invalid witness file) 0 .0013 .0015 .41 0     0      - -
array-examples/standard_running_false-unreach-call.i unreach-call false(unreach-call) 1 1.9   1.9   180 29    0      0      timeout 0 97    82    2000 0      0      true -32 7.3   4.7   310   .66  0   false(unreach-call) 1 3.4  2.0  250 0      0      true -32 .57   .57   20    .045 0      - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call true 2 .97  .97  95 15    0      0      - - - - out of memory 0 630    550    7000 0   0      true 2 9.0   5.1   310   .66  0     
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call true 2 1.1   1.1   86 16    0      0      - - - - out of memory 0 660    610    7000 0   0      timeout 0 960     920     2200   .82  .39  
array-examples/relax_true-unreach-call.i unreach-call timeout (verification) 0 900     900     750 11000    .025  0      - - - - error (invalid witness file) 0 .73 .46 41 0   0      error (2) 0 .026 .027 5.7 0     0     
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call true 2 1.7   1.7   95 24    0      0      - - - - timeout 0 900    890    2500 0   0      timeout 0 960     820     1700   .66  0     
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call true 2 1.4   1.4   68 21    0      0      - - - - timeout 0 900    890    5100 0   .13   timeout 0 960     940     1200   .68  .016 
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call timeout (verification) 0 900     900     1200 10000    .025  0      - - - - error (invalid witness file) 0 .59 .36 40 0   0      error (2) 0 .026 .026 5.6 0     0     
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call true 2 1.1   1.1   62 14    0      0      - - - - timeout 0 900    890    2500 0   0      timeout 0 960     820     1700   .73  0     
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call true 2 .14  .13  16 1.4  0      0      - - - - true 2 4.9  2.7  270 0   0      true 2 6.8   4.3   300   .66  0     
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call probably out of memory (killed (signal 9, verification)) 0 290     300     15000 3700    .12   .0041 - - - - error (invalid witness file) 0 .70 .44 42 0   0      error (2) 0 .026 .027 5.6 0     0     
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call probably out of memory (killed (signal 9, verification)) 0 350     360     15000 4900    .11   0      - - - - error (invalid witness file) 0 .79 .48 40 0   0      error (2) 0 .021 .022 5.7 0     0     
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call true 2 2.1   2.1   100 23    0      0      - - - - timeout 0 900    890    4800 0   0      timeout 0 960     930     820   .66  0     
array-examples/standard_compare_true-unreach-call_ground.i unreach-call true 2 1.3   1.3   63 17    0      0      - - - - timeout 0 900    880    4600 0   0      timeout 0 960     900     1300   1.6   0     
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call true 2 2.9   2.9   230 38    0      0      - - - - timeout 0 900    890    4200 0   0      timeout 0 960     930     790   .84  0     
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call true 2 3.3   3.3   250 41    0      0      - - - - timeout 0 900    890    4000 0   0      timeout 0 960     930     740   .74  0     
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call true 2 3.9   3.9   280 45    0      0      - - - - timeout 0 900    890    3600 0   .041  timeout 0 960     940     820   .82  0     
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call true 2 4.3   4.4   300 55    0      0      - - - - timeout 0 900    890    3800 0   0      timeout 0 960     930     830   1.3   0     
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call true 2 4.9   4.9   330 67    0      0      - - - - timeout 0 900    890    3900 0   .70   timeout 0 960     940     840   .74  0     
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call true 2 5.3   5.3   350 75    0      0      - - - - timeout 0 900    890    4400 0   0      timeout 0 960     940     710   1.7   0     
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call true 2 5.8   5.8   380 79    0      0      - - - - timeout 0 900    890    4000 0   0      timeout 0 960     940     840   .63  0     
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call true 2 6.4   6.4   400 94    0      0      - - - - timeout 0 900    890    4000 0   0      timeout 0 960     940     740   .64  0     
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call true 2 7.0   7.0   430 95    0      0      - - - - timeout 0 900    890    4300 0   0      timeout 0 960     930     870   .64  0     
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call true 2 1.8   1.8   99 26    0      0      - - - - timeout 0 900    890    2900 0   0      timeout 0 960     940     700   .63  0     
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call true 2 2.2   2.2   120 31    0      0      - - - - timeout 0 900    890    2500 0   0      timeout 0 960     940     850   .74  0     
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call true 2 1.8   1.8   140 26    0      0      - - - - timeout 0 900    890    3200 0   0      timeout 0 960     940     730   .63  0     
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call true 2 1.3   1.3   81 20    0      0      - - - - timeout 0 900    890    4100 0   0      timeout 0 960     940     670   .63  0     
array-examples/standard_find_true-unreach-call_ground.i unreach-call error(unknown, verification-finished) 0 350     350     2400 4800    0      0      - - - - error (invalid witness file) 0 .59 .35 40 0   0      error (2) 0 .021 .023 5.7 0     0     
array-examples/standard_init1_true-unreach-call_ground.i unreach-call true 2 .92  .92  63 14    0      0      - - - - timeout 0 900    890    5000 0   0      timeout 0 960     930     680   1.6   0     
array-examples/standard_init2_true-unreach-call_ground.i unreach-call true 2 1.2   1.2   79 17    0      0      - - - - timeout 0 900    890    3900 0   0      timeout 0 960     940     790   .63  0     
array-examples/standard_init3_true-unreach-call_ground.i unreach-call true 2 1.5   1.5   96 20    0      0      - - - - timeout 0 900    890    4700 0   0      timeout 0 960     940     660   .73  0     
array-examples/standard_init4_true-unreach-call_ground.i unreach-call true 2 1.8   1.8   110 25    0      .60   - - - - timeout 0 900    890    4500 0   0      timeout 0 960     940     800   1.5   0     
array-examples/standard_init5_true-unreach-call_ground.i unreach-call true 2 2.0   2.0   130 28    0      0      - - - - timeout 0 900    890    4800 0   .13   timeout 0 960     940     790   .81  0     
array-examples/standard_init6_true-unreach-call_ground.i unreach-call true 2 2.3   2.3   140 33    0      0      - - - - timeout 0 900    890    5100 0   0      timeout 0 960     940     830   .63  0     
array-examples/standard_init7_true-unreach-call_ground.i unreach-call true 2 2.5   2.5   160 38    0      0      - - - - timeout 0 900    890    4700 0   0      timeout 0 960     940     840   1.1   0     
array-examples/standard_init8_true-unreach-call_ground.i unreach-call true 2 2.8   2.8   180 39    0      0      - - - - timeout 0 900    890    4800 0   0      timeout 0 960     940     680   .64  0     
array-examples/standard_init9_true-unreach-call_ground.i unreach-call true 2 3.0   3.0   190 45    0      0      - - - - timeout 0 900    890    5100 0   0      timeout 0 960     940     690   .62  0     
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call true 2 1.0   1.0   64 13    0      0      - - - - timeout 0 900    890    2400 0   0      timeout 0 960     810     2000   .64  0     
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call true 2 1.1   1.1   64 14    0      0      - - - - timeout 0 900    890    3800 0   .57   timeout 0 960     810     2200   .63  0     
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call true 2 .68  .68  39 9.0  0      0      - - - - timeout 0 900    890    6300 0   0      timeout 0 960     930     820   .63  0     
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call true 2 2.0   2.0   120 29    0      0      - - - - timeout 0 900    890    2600 0   0      timeout 0 960     920     850   1.6   0     
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call true 2 1.3   1.3   84 21    0      0      - - - - timeout 0 900    880    4100 0   0      timeout 0 960     930     900   1.7   0     
array-examples/standard_partition_true-unreach-call_ground.i unreach-call true 2 .58  .57  47 9.0  0      0      - - - - timeout 0 900    890    5700 0   0      timeout 0 960     920     2100   .66  0     
array-examples/standard_password_true-unreach-call_ground.i unreach-call true 2 1.3   1.3   63 18    0      0      - - - - timeout 0 900    880    4400 0   0      timeout 0 960     900     1300   1.5   0     
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call true 2 1.2   1.2   64 17    0      0      - - - - timeout 0 910    890    5400 0   0      timeout 0 960     910     870   .67  0     
array-examples/standard_running_true-unreach-call.i unreach-call true 2 1.1   1.1   45 16    0      0      - - - - timeout 0 900    890    3000 0   0      timeout 0 960     940     1500   .62  0     
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call timeout (verification) 0 900     900     2600 4100    .012  0      - - - - error (invalid witness file) 0 .71 .42 41 0   0      error (2) 0 .020 .021 5.6 0     0     
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call true 2 1.1   1.1   64 18    0      0      - - - - timeout 0 900    890    2900 0   0      timeout 0 960     930     660   .68  0     
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call true 2 1.3   1.3   79 22    0      0      - - - - timeout 0 900    880    4400 0   0      timeout 0 960     890     1500   .63  0     
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 170     170     2300 2300    0      0      - - - - error (invalid witness file) 0 .64 .41 42 0   0      error (2) 0 .021 .022 5.6 0     0     
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call error(unknown, verification-finished) 0 160     160     2400 1900    0      0      - - - - error (invalid witness file) 0 .76 .47 42 0   0      error (2) 0 .024 .024 5.6 0     0     
array-examples/standard_two_index_01_true-unreach-call.i unreach-call true 2 .40  .40  34 5.2  0      0      - - - - timeout 0 900    890    4000 0   0      timeout 0 960     930     660   .65  0     
array-examples/standard_two_index_02_true-unreach-call.i unreach-call true 2 2.4   2.4   190 29    0      .0041 - - - - timeout 0 900    890    5100 0   .78   timeout 0 960     930     770   1.6   0     
array-examples/standard_two_index_03_true-unreach-call.i unreach-call true 2 .33  .33  31 4.9  0      0      - - - - timeout 0 900    890    4900 0   0      timeout 0 960     920     830   1.6   0     
array-examples/standard_two_index_04_true-unreach-call.i unreach-call true 2 2.1   2.1   180 24    0      0      - - - - timeout 0 900    890    4900 0   0      timeout 0 960     920     820   1.6   0     
array-examples/standard_two_index_05_true-unreach-call.i unreach-call true 2 1.9   1.9   180 27    0      0      - - - - timeout 0 900    890    5100 0   0      timeout 0 960     920     700   .65  0     
array-examples/standard_two_index_06_true-unreach-call.i unreach-call true 2 .32  .32  29 3.5  0      0      - - - - timeout 0 900    890    4900 0   0      timeout 0 960     910     890   1.5   0     
array-examples/standard_two_index_07_true-unreach-call.i unreach-call true 2 1.9   1.9   180 24    0      0      - - - - timeout 0 900    890    4700 0   .057  timeout 0 960     920     930   .63  0     
array-examples/standard_two_index_08_true-unreach-call.i unreach-call true 2 1.9   1.9   180 25    0      0      - - - - timeout 0 900    890    4700 0   0      timeout 0 960     910     860   1.5   0     
array-examples/standard_two_index_09_true-unreach-call.i unreach-call true 2 1.9   1.9   180 23    0      0      - - - - timeout 0 900    890    5200 0   0      timeout 0 960     920     920   1.2   0     
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call true 2 .14  .14  15 1.5  0      0      - - - - out of memory 0 750    740    7000 0   0      timeout 0 960     920     1200   .63  0     
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call true 2 1.5   1.5   67 20    0      0      - - - - timeout 0 900    900    4000 0   0      timeout 0 960     930     610   1.0   0     
array-examples/standard_sentinel_true-unreach-call.i.v+cfa-reducer.c unreach-call timeout (verification) 0 900     900     2600 4200    .012  0      - - - - error (invalid witness file) 0 .73 .46 42 0   0      error (2) 0 .027 .027 5.6 0     0     
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 .79  .79  110 12    0      0      timeout 0 97    88    1100 0      0      true -32 7.4   4.7   310   .62  0   false(unreach-call) 1 3.5  2.0  240 0      0      false(unreach-call) 1 .56   .56   20    .045 0      - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call false(unreach-call) 1 .78  .77  110 9.8  0      0      timeout 0 97    85    1700 0      0      true -32 9.2   5.2   600   .62  0   false(unreach-call) 1 4.0  2.3  250 0      0      false(unreach-call) 1 .57   .57   20    .045 0      - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 1.7   1.7   200 22    0      0      timeout 0 96    78    2100 0      0      true -32 6.8   3.9   300   .62  0   false(unreach-call) 1 3.7  2.1  240 0      0      false(unreach-call) 1 .58   .58   20    .049 0      - -
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call false(unreach-call) 1 1.0   .99  120 14    0      0      timeout 0 97    86    1700 0      0      true -32 8.9   5.0   600   .62  0   false(unreach-call) 1 4.1  2.4  250 0      0      false(unreach-call) 1 .60   .59   20    .045 0      - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call timeout (verification) 0 900     900     2600 10000    .025  0      error (invalid witness file) 0 .59 .36 42 0      0      error (2) 0 .022 .023 5.6 0     0   error (invalid witness file) 0 .96 .62 48 0      0      error (invalid witness file) 0 .0027 .0035 .53 0     0      - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call false(unreach-call) 1 1.7   1.7   320 23    0      0      timeout 0 97    78    2200 0      0      true -32 7.2   4.1   300   .086 0   false(unreach-call) 1 3.6  2.1  250 0      0      true -32 .58   .58   20    .057 0      - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call timeout (verification) 0 900     900     2600 13000    .025  0      - - - - error (invalid witness file) 0 .66 .40 41 0   0      error (2) 0 .027 .028 5.6 0     0     
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call timeout (verification) 0 900     900     3100 9600    .025  0      - - - - error (invalid witness file) 0 .73 .45 40 0   0      error (2) 0 .021 .022 5.6 0     0     
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call true 2 .95  .95  69 14    0      0      - - - - timeout 0 900    900    3900 0   0      timeout 0 960     920     1800   .64  0     
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call timeout (verification) 0 900     900     3200 14000    .029  0      - - - - error (invalid witness file) 0 .59 .37 40 0   0      error (2) 0 .021 .022 5.6 0     0     
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call true 2 1.2   1.2   100 17    0      0      - - - - timeout 0 900    880    4200 0   0      true 2 16     9.7   510   .66  0     
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call timeout (verification) 0 900     900     4000 12000    .025  0      - - - - error (invalid witness file) 0 .76 .46 41 0   0      error (2) 0 .021 .021 5.6 0     0     
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call timeout (verification) 0 900     900     2800 9400    .025  0      - - - - error (invalid witness file) 0 .68 .41 41 0   0      error (2) 0 .021 .022 5.8 0     0     
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call true 2 1.4   1.4   110 16    0      0      - - - - out of memory 0 550    550    7000 0   0      timeout 0 960     930     1500   1.6   0     
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call true 2 1.1   1.1   82 16    0      0      - - - - timeout 0 900    900    3800 0   0      timeout 0 960     940     1300   .63  0     
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call timeout (verification) 0 900     900     4200 12000    .025  0      - - - - error (invalid witness file) 0 .64 .39 42 0   0      error (2) 0 .021 .023 5.7 0     0     
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call timeout (verification) 0 900     900     1100 10000    .025  0      - - - - error (invalid witness file) 0 .75 .47 40 0   0      error (2) 0 .021 .022 5.6 0     0     
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 .46  .45  62 5.5  0      .28   false(unreach-call) 1 7.4  5.3  350 0      0      true -32 7.0   4.4   310   .62  0   unknown 0 3.5  2.1  250 0      0      false(unreach-call) 1 .60   .60   20    .057 0      - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 .61  .61  61 6.6  0      0      timeout 0 92    90    570 0      0      true -32 7.0   4.0   300   .62  0   unknown 0 3.7  2.2  250 0      0      false(unreach-call) 1 .59   .59   20    .057 0      - -
reducercommutativity/rangesum20_false-unreach-call.i unreach-call false(unreach-call) 1 1.5   1.5   62 21    0      0      timeout 0 92    90    620 0      0      true -32 6.9   3.9   300   .62  0   unknown 0 3.6  2.1  250 0      0      false(unreach-call) 1 .57   .59   20    .057 0      - -
reducercommutativity/rangesum40_false-unreach-call.i unreach-call false(unreach-call) 1 8.4   8.4   69 82    0      0      timeout 0 92    90    790 0      0      true -32 7.3   4.2   310   .62  0   unknown 0 3.9  2.3  240 0      0      false(unreach-call) 1 .58   .58   20    .057 0      - -
reducercommutativity/rangesum60_false-unreach-call.i unreach-call false(unreach-call) 1 66     66     89 800    0      0      false(unreach-call) 1 67    61    1700 0      .0041 true -32 6.9   4.3   300   .62  0   unknown 0 3.5  2.1  250 0      .0041 false(unreach-call) 1 .57   .57   20    .057 0      - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 .76  .76  21 10    0      0      false(unreach-call) 1 5.6  3.6  340 0      .0041 true -32 7.4   4.2   300   .66  0   unknown 0 3.5  2.1  250 0      0      false(unreach-call) 1 .59   .58   20    .057 0      - -
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call true 2 .17  .16  18 1.7  0      0      - - - - timeout 0 900    900    2000 0   0      timeout 0 960     940     910   .75  0     
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call true 2 .17  .17  17 1.8  0      0      - - - - timeout 0 900    890    3300 0   0      timeout 0 960     930     1700   .63  0     
reducercommutativity/avg20_true-unreach-call.i unreach-call true 2 .17  .17  18 1.8  0      0      - - - - timeout 0 900    890    3100 0   0      timeout 0 960     910     4900   .65  0     
reducercommutativity/avg40_true-unreach-call.i unreach-call true 2 .18  .17  18 2.8  0      0      - - - - timeout 0 900    890    4000 0   0      timeout 0 960     920     1000   .84  0     
reducercommutativity/avg60_true-unreach-call.i unreach-call true 2 .20  .19  17 1.9  0      0      - - - - timeout 0 900    890    4200 0   0      timeout 0 960     920     840   .65  0     
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call timeout (verification) 0 900     900     3800 12000    .025  0      - - - - error (invalid witness file) 0 .60 .36 40 0   0      error (2) 0 .022 .022 5.6 0     0     
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call true 2 2.8   2.8   23 36    0      0      - - - - true 2 550    540    1200 0   0      timeout 0 960     920     2400   .71  0     
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call true 2 180     180     64 2900    0      0      - - - - timeout 0 900    890    1700 0   0      timeout 0 960     840     6000   .66  0     
reducercommutativity/max20_true-unreach-call.i unreach-call timeout (verification) 0 900     900     140 11000    .012  4.9    - - - - error (invalid witness file) 0 .74 .45 40 0   0      error (2) 0 .026 .027 5.6 0     0     
reducercommutativity/max40_true-unreach-call.i unreach-call timeout (verification) 0 900     900     200 13000    .012  0      - - - - error (invalid witness file) 0 .78 .48 42 0   0      error (2) 0 .030 .035 5.7 0     0     
reducercommutativity/max60_true-unreach-call.i unreach-call timeout (verification) 0 900     900     210 12000    .012  0      - - - - error (invalid witness file) 0 .72 .44 40 0   0      error (2) 0 .026 .027 5.6 0     0     
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call error(unknown, verification-finished) 0 810     810     3300 9700    0      0      - - - - error (invalid witness file) 0 .62 .37 40 0   0      error (2) 0 .021 .022 5.6 0     0     
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call true 2 .17  .16  17 1.9  0      0      - - - - true 2 390    380    1200 0   0      timeout 0 960     910     4100   .65  0     
reducercommutativity/sep10_true-unreach-call.i unreach-call true 2 .21  .20  16 1.8  0      0      - - - - timeout 0 900    890    1200 0   0      timeout 0 960     820     6800   .65  0     
reducercommutativity/sep20_true-unreach-call.i unreach-call true 2 .22  .21  17 2.0  0      0      - - - - timeout 0 900    890    1100 0   0      timeout 0 960     830     6200   .66  0     
reducercommutativity/sep40_true-unreach-call.i unreach-call true 2 .19  .18  18 1.8  0      0      - - - - timeout 0 900    890    1200 0   0      timeout 0 960     910     1300   .64  0     
reducercommutativity/sep60_true-unreach-call.i unreach-call true 2 .18  .17  18 2.0  0      0      - - - - timeout 0 900    890    1200 0   0      timeout 0 960     920     910   1.3   0     
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call error(unknown, verification-finished) 0 800     800     3100 9200    0      0      - - - - error (invalid witness file) 0 .70 .42 41 0   0      error (2) 0 .027 .028 5.7 0     0     
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call true 2 .17  .16  17 1.9  0      0      - - - - timeout 0 900    890    1300 0   .025  timeout 0 960     940     4600   .71  0     
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call true 2 .19  .19  17 1.6  0      0      - - - - timeout 0 900    890    3400 0   0      true 2 790     750     1100   .62  0     
reducercommutativity/sum20_true-unreach-call.i unreach-call true 2 .17  .17  17 2.2  0      0      - - - - timeout 0 900    890    2800 0   0      timeout 0 960     910     4900   .66  .0041
reducercommutativity/sum40_true-unreach-call.i unreach-call true 2 .18  .18  17 2.0  0      0      - - - - timeout 0 900    890    4400 0   0      timeout 0 960     920     880   .71  0     
reducercommutativity/sum60_true-unreach-call.i unreach-call true 2 .20  .20  17 2.2  0      0      - - - - timeout 0 900    890    4400 0   0      timeout 0 960     920     810   .66  0     
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call error(unknown, verification-finished) 0 890     890     3400 9300    0      0      - - - - error (invalid witness file) 0 .61 .37 40 0   0      error (2) 0 .020 .021 5.6 0     0     
array-tiling/mlceu_false-unreach-call.i unreach-call timeout (verification) 0 900     900     1300 9400    .025  0      error (invalid witness file) 0 .63 .39 40 0      0      error (2) 0 .021 .022 5.6 0     0   error (invalid witness file) 0 .95 .62 48 0      0      error (invalid witness file) 0 .0045 .0056 .41 0     0      - -
array-tiling/skippedu_false-unreach-call.i unreach-call timeout (verification) 0 900     900     420 15000    .025  0      error (invalid witness file) 0 .60 .36 42 0      0      error (2) 0 .021 .023 5.6 0     0   error (invalid witness file) 0 .93 .60 47 0      0      error (invalid witness file) 0 .0036 .0072 .53 0     0      - -
array-tiling/mbpr2_true-unreach-call.i unreach-call timeout (verification) 0 900     900     380 11000    .025  0      - - - - error (invalid witness file) 0 .70 .43 40 0   0      error (2) 0 .026 .028 5.6 0     0     
array-tiling/mbpr3_true-unreach-call.i unreach-call timeout (verification) 0 900     900     280 13000    .025  0      - - - - error (invalid witness file) 0 .62 .38 41 0   0      error (2) 0 .022 .023 5.7 0     0     
array-tiling/mbpr4_true-unreach-call.i unreach-call timeout (verification) 0 900     900     350 11000    .025  0      - - - - error (invalid witness file) 0 .66 .42 43 0   0      error (2) 0 .025 .026 5.6 0     0     
array-tiling/mbpr5_true-unreach-call.i unreach-call timeout (verification) 0 900     900     270 12000    .025  0      - - - - error (invalid witness file) 0 .66 .42 43 0   0      error (2) 0 .021 .021 5.6 0     0     
array-tiling/nr2_true-unreach-call.i unreach-call timeout (verification) 0 900     900     410 12000    .025  0      - - - - error (invalid witness file) 0 .74 .45 40 0   0      error (2) 0 .026 .027 5.6 0     0     
array-tiling/nr3_true-unreach-call.i unreach-call timeout (verification) 0 900     900     320 11000    .025  0      - - - - error (invalid witness file) 0 .74 .45 41 0   0      error (2) 0 .028 .029 5.6 0     0     
array-tiling/nr4_true-unreach-call.i unreach-call timeout (verification) 0 900     900     390 12000    .025  0      - - - - error (invalid witness file) 0 .58 .37 40 0   0      error (2) 0 .026 .027 5.6 0     0     
array-tiling/nr5_true-unreach-call.i unreach-call timeout (verification) 0 900     900     290 11000    .025  0      - - - - error (invalid witness file) 0 .69 .42 41 0   0      error (2) 0 .026 .027 5.7 0     0     
array-tiling/pnr2_true-unreach-call.i unreach-call timeout (verification) 0 900     900     400 11000    .025  0      - - - - error (invalid witness file) 0 .59 .36 41 0   0      error (2) 0 .021 .022 5.6 0     0     
array-tiling/pnr3_true-unreach-call.i unreach-call timeout (verification) 0 900     900     310 12000    .025  0      - - - - error (invalid witness file) 0 .76 .47 41 0   0      error (2) 0 .026 .026 5.6 0     0     
array-tiling/pnr4_true-unreach-call.i unreach-call timeout (verification) 0 900     900     380 14000    .025  0      - - - - error (invalid witness file) 0 .75 .46 42 0   0      error (2) 0 .021 .022 5.6 0     0     
array-tiling/pnr5_true-unreach-call.i unreach-call timeout (verification) 0 900     900     280 14000    .025  0      - - - - error (invalid witness file) 0 .70 .42 41 0   0      error (2) 0 .021 .021 5.6 0     0     
array-tiling/poly1_true-unreach-call.i unreach-call timeout (verification) 0 900     900     580 11000    .025  0      - - - - error (invalid witness file) 0 .72 .44 41 0   0      error (2) 0 .021 .022 5.6 0     0     
array-tiling/poly2_true-unreach-call.i unreach-call timeout (verification) 0 900     900     500 12000    .025  0      - - - - error (invalid witness file) 0 .96 .58 41 0   0      error (2) 0 .026 .027 5.7 0     0     
array-tiling/pr2_true-unreach-call.i unreach-call timeout (verification) 0 900     900     1500 12000    .025  0      - - - - error (invalid witness file) 0 .60 .36 41 0   0      error (2) 0 .022 .023 5.6 0     0     
array-tiling/pr3_true-unreach-call.i unreach-call timeout (verification) 0 900     900     1400 13000    .020  0      - - - - error (invalid witness file) 0 .73 .44 40 0   0      error (2) 0 .026 .027 5.7 0     0     
array-tiling/pr4_true-unreach-call.i unreach-call timeout (verification) 0 900     900     1700 10000    .025  0      - - - - error (invalid witness file) 0 .72 .44 41 0   0      error (2) 0 .027 .027 5.6 0     0     
array-tiling/pr5_true-unreach-call.i unreach-call timeout (verification) 0 900     900     1400 10000    .020  0      - - - - error (invalid witness file) 0 .72 .44 42 0   0      error (2) 0 .020 .021 5.6 0     0     
array-tiling/revcpyswp2_true-unreach-call.i unreach-call timeout (verification) 0 900     900     140 13000    .025  0      - - - - error (invalid witness file) 0 .77 .46 41 0   0      error (2) 0 .021 .022 5.6 0     0     
array-tiling/rew_true-unreach-call.i unreach-call timeout (verification) 0 900     900     920 11000    .025  0      - - - - error (invalid witness file) 0 .60 .37 42 0   0      error (2) 0 .020 .020 5.6 0     0     
array-tiling/rewnif_true-unreach-call.i unreach-call timeout (verification) 0 900     900     920 12000    .025  0      - - - - error (invalid witness file) 0 .66 .41 42 0   0      error (2) 0 .024 .024 5.6 0     0     
array-tiling/rewnifrev2_true-unreach-call.i unreach-call timeout (verification) 0 900     900     570 12000    .020  0      - - - - error (invalid witness file) 0 .62 .37 42 0   0      error (2) 0 .021 .021 5.6 0     0     
array-tiling/rewnifrev_true-unreach-call.i unreach-call timeout (verification) 0 900     900     600 13000    .025  0      - - - - error (invalid witness file) 0 .60 .37 40 0   0      error (2) 0 .023 .023 5.6 0     0     
array-tiling/rewrev_true-unreach-call.i unreach-call timeout (verification) 0 900     900     660 11000    .025  0      - - - - error (invalid witness file) 0 .58 .37 41 0   0      error (2) 0 .023 .024 5.6 0     0     
array-tiling/skipped_true-unreach-call.i unreach-call timeout (verification) 0 900     900     420 13000    .025  0      - - - - error (invalid witness file) 0 .59 .38 40 0   0      error (2) 0 .026 .027 5.6 0     0     
array-tiling/tcpy_true-unreach-call.i unreach-call timeout (verification) 0 900     900     690 12000    .020  4.7    - - - - error (invalid witness file) 0 .77 .46 40 0   0      error (2) 0 .020 .020 5.6 0     0     
array-programs/copysome1_false-unreach-call.i unreach-call false(unreach-call) 0 25     25     1200 240    0      0      timeout 0 97    86    2000 0      0      true -32 7.0   4.4   310   .62  0   true -32 3.5  2.1  250 0      0      true -32 .58   .58   20    .049 .0041 - -
array-programs/copysome2_false-unreach-call.i unreach-call false(unreach-call) 0 42     42     1500 370    0      0      timeout 0 97    81    2100 0      .0041 true -32 7.5   4.2   300   .62  0   true -32 3.5  2.1  250 0      0      true -32 .58   .60   20    .049 0      - -
array-programs/copysome1_true-unreach-call.i unreach-call true 2 17     17     770 130    0      0      - - - - timeout 0 900    890    5000 0   0      timeout 0 960     930     2300   .64  0     
array-programs/copysome2_true-unreach-call.i unreach-call true 2 31     31     1100 220    0      0      - - - - timeout 0 900    890    4100 0   0      timeout 0 960     930     1400   .64  0     
array-crafted/bAnd1_true-unreach-call.i unreach-call true 2 .18  .18  18 2.0  0      0      - - - - timeout 0 900    890    3700 0   0      timeout 0 960     920     750   .65  0     
array-crafted/bAnd2_true-unreach-call.i unreach-call true 2 23     23     180 200    0      0      - - - - timeout 0 900    890    3900 0   0      timeout 0 960     910     970   1.6   0     
array-crafted/bAnd3_true-unreach-call.i unreach-call timeout (verification) 0 900     900     1700 6700    .012  0      - - - - error (invalid witness file) 0 .76 .45 41 0   0      error (2) 0 .028 .029 5.6 0     0     
array-crafted/bAnd4_true-unreach-call.i unreach-call out of memory (killed (signal 9, verification)) 0 560     550     15000 3300    .0041 0      - - - - error (invalid witness file) 0 .75 .46 40 0   0      error (2) 0 .027 .027 5.6 0     0     
array-crafted/bAnd5_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 860     860     3400 10000    0      0      - - - - error (invalid witness file) 0 .64 .40 41 0   0      error (2) 0 .023 .024 5.6 0     0     
array-crafted/bor1_true-unreach-call.i unreach-call true 2 .17  .17  18 2.7  0      0      - - - - timeout 0 910    890    4700 0   0      timeout 0 960     920     760   .65  0     
array-crafted/bor2_true-unreach-call.i unreach-call true 2 10     10     110 120    0      0      - - - - timeout 0 900    890    4700 0   0      timeout 0 960     920     910   .63  0     
array-crafted/bor3_true-unreach-call.i unreach-call true 2 520     520     1300 5000    0      0      - - - - timeout 0 900    890    4300 0   0      timeout 0 960     910     870   .63  0     
array-crafted/bor4_true-unreach-call.i unreach-call out of memory (killed (signal 9, verification)) 0 180     180     15000 1500    .0041 0      - - - - error (invalid witness file) 0 .60 .37 41 0   0      error (2) 0 .021 .021 5.6 0     0     
array-crafted/bor5_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 870     870     3500 10000    0      0      - - - - error (invalid witness file) 0 .74 .45 41 0   0      error (2) 0 .023 .023 5.6 0     0     
array-crafted/mapavg1_true-unreach-call.i unreach-call true 2 .19  .19  17 2.2  0      0      - - - - timeout 0 900    890    3900 0   0      timeout 0 960     920     900   1.6   0     
array-crafted/mapavg2_true-unreach-call.i unreach-call timeout (verification) 0 900     900     710 8900    .012  0      - - - - error (invalid witness file) 0 .72 .44 40 0   0      error (2) 0 .025 .026 5.6 0     0     
array-crafted/mapavg3_true-unreach-call.i unreach-call timeout (verification) 0 900     900     4700 5500    .012  0      - - - - error (invalid witness file) 0 .65 .41 40 0   0      error (2) 0 .021 .022 5.6 0     0     
array-crafted/mapavg4_true-unreach-call.i unreach-call timeout (verification) 0 900     900     300 7800    .025  0      - - - - error (invalid witness file) 0 .74 .45 40 0   0      error (2) 0 .022 .023 5.6 0     0     
array-crafted/mapavg5_true-unreach-call.i unreach-call timeout (verification) 0 900     900     3700 11000    .029  0      - - - - error (invalid witness file) 0 .73 .45 41 0   0      error (2) 0 .025 .026 5.6 0     0     
array-crafted/mapsum1_true-unreach-call.i unreach-call true 2 .18  .17  17 2.1  0      0      - - - - timeout 0 900    890    4200 0   0      timeout 0 960     920     920   .97  0     
array-crafted/mapsum2_true-unreach-call.i unreach-call true 2 .66  .65  36 11    0      0      - - - - timeout 0 900    890    4700 0   0      timeout 0 960     920     830   .67  0     
array-crafted/mapsum3_true-unreach-call.i unreach-call true 2 56     56     1300 870    0      0      - - - - timeout 0 900    890    4000 0   0      timeout 0 960     920     920   .63  0     
array-crafted/mapsum4_true-unreach-call.i unreach-call timeout (verification) 0 900     900     370 8100    .025  0      - - - - error (invalid witness file) 0 .62 .38 43 0   0      error (2) 0 .021 .022 5.6 0     0     
array-crafted/mapsum5_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 840     840     3300 9000    0      0      - - - - error (invalid witness file) 0 .60 .37 41 0   0      error (2) 0 .021 .022 5.6 0     0     
array-crafted/xor1_true-unreach-call.i unreach-call true 2 .17  .17  18 2.1  0      0      - - - - timeout 0 900    890    4800 0   0      timeout 0 960     910     910   .63  .0041
array-crafted/xor2_true-unreach-call.i unreach-call timeout (verification) 0 900     900     340 9200    .012  0      - - - - error (invalid witness file) 0 .67 .41 42 0   0      error (2) 0 .021 .022 5.6 0     0     
array-crafted/xor3_true-unreach-call.i unreach-call timeout (verification) 0 900     900     2000 7700    .012  0      - - - - error (invalid witness file) 0 .72 .45 41 0   0      error (2) 0 .029 .029 5.6 0     0     
array-crafted/xor4_true-unreach-call.i unreach-call out of memory (killed (signal 9, verification)) 0 200     200     15000 1700    .0041 0      - - - - error (invalid witness file) 0 .70 .43 40 0   0      error (2) 0 .026 .027 5.6 0     0     
array-crafted/xor5_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 880     880     3500 8900    0      0      - - - - error (invalid witness file) 0 .63 .38 40 0   0      error (2) 0 .025 .026 5.6 0     0     
array-crafted/zero_sum1_true-unreach-call.c unreach-call timeout (verification) 0 900     900     560 11000    .025  0      - - - - error (invalid witness file) 0 .61 .37 40 0   0      error (2) 0 .021 .021 5.6 0     0     
array-crafted/zero_sum2_true-unreach-call.c unreach-call timeout (verification) 0 900     900     800 9800    .025  0      - - - - error (invalid witness file) 0 .76 .46 40 0   0      error (2) 0 .025 .026 5.6 0     0     
array-crafted/zero_sum3_true-unreach-call.c unreach-call timeout (verification) 0 900     900     910 11000    .029  0      - - - - error (invalid witness file) 0 .74 .46 41 0   0      error (2) 0 .024 .025 5.6 0     0     
array-crafted/zero_sum4_true-unreach-call.c unreach-call timeout (verification) 0 900     900     970 11000    .029  0      - - - - error (invalid witness file) 0 .57 .37 41 0   0      error (2) 0 .022 .023 5.6 0     0     
array-crafted/zero_sum5_true-unreach-call.c unreach-call timeout (verification) 0 900     900     1000 11000    .029  .0041 - - - - error (invalid witness file) 0 .74 .46 40 0   0      error (2) 0 .028 .030 5.6 0     0     
array-crafted/zero_sum_const1_true-unreach-call.c unreach-call timeout (verification) 0 900     900     1100 12000    .025  0      - - - - error (invalid witness file) 0 .60 .38 41 0   0      error (2) 0 .022 .023 5.7 0     0     
array-crafted/zero_sum_const2_true-unreach-call.c unreach-call timeout (verification) 0 900     900     1200 13000    .025  0      - - - - error (invalid witness file) 0 .59 .36 40 0   0      error (2) 0 .027 .028 5.6 0     0     
array-crafted/zero_sum_const3_true-unreach-call.c unreach-call timeout (verification) 0 900     900     1300 11000    .025  0      - - - - error (invalid witness file) 0 .64 .40 42 0   0      error (2) 0 .021 .022 5.6 0     0     
array-crafted/zero_sum_const4_true-unreach-call.c unreach-call timeout (verification) 0 900     900     1300 12000    .025  0      - - - - error (invalid witness file) 0 .73 .45 41 0   0      error (2) 0 .022 .023 5.7 0     0     
array-crafted/zero_sum_const5_true-unreach-call.c unreach-call timeout (verification) 0 900     900     1300 10000    .025  0      - - - - error (invalid witness file) 0 .78 .48 41 0   0      error (2) 0 .023 .025 5.7 0     0     
array-crafted/zero_sum_const_m2_true-unreach-call.c unreach-call timeout (verification) 0 900     900     1100 9800    .025  0      - - - - error (invalid witness file) 0 .59 .36 40 0   0      error (2) 0 .022 .022 5.6 0     0     
array-crafted/zero_sum_const_m3_true-unreach-call.c unreach-call timeout (verification) 0 900     900     1200 11000    .025  0      - - - - error (invalid witness file) 0 .78 .47 42 0   0      error (2) 0 .023 .023 5.6 0     0     
array-crafted/zero_sum_const_m4_true-unreach-call.c unreach-call timeout (verification) 0 900     900     1300 13000    .025  0      - - - - error (invalid witness file) 0 .76 .47 41 0   0      error (2) 0 .023 .023 5.6 0     0     
array-crafted/zero_sum_const_m5_true-unreach-call.c unreach-call timeout (verification) 0 900     900     1300 11000    .025  0      - - - - error (invalid witness file) 0 .78 .47 42 0   0      error (2) 0 .021 .022 5.6 0     0     
array-crafted/zero_sum_m2_true-unreach-call.c unreach-call timeout (verification) 0 900     900     810 11000    .041  0      - - - - error (invalid witness file) 0 .74 .44 42 0   0      error (2) 0 .025 .026 5.6 0     0     
array-crafted/zero_sum_m3_true-unreach-call.c unreach-call timeout (verification) 0 900     900     920 12000    .029  0      - - - - error (invalid witness file) 0 .73 .45 40 0   0      error (2) 0 .026 .027 5.6 0     0     
array-crafted/zero_sum_m4_true-unreach-call.c unreach-call timeout (verification) 0 900     900     980 12000    .029  0      - - - - error (invalid witness file) 0 .60 .36 40 0   0      error (2) 0 .022 .023 5.6 0     0     
array-crafted/zero_sum_m5_true-unreach-call.c unreach-call timeout (verification) 0 900     900     1000 13000    .029  0      - - - - error (invalid witness file) 0 .74 .46 40 0   0      error (2) 0 .022 .023 5.6 0     0     
array-multidimensional/add-2-n-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 34     34     2300 420    0      0      - - - - error (invalid witness file) 0 .77 .48 40 0   0      error (2) 0 .022 .023 5.6 0     0     
array-multidimensional/add-3-n-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 29     29     2300 340    0      0      - - - - error (invalid witness file) 0 .81 .50 41 0   0      error (2) 0 .023 .025 5.6 0     0     
array-multidimensional/copy-2-u_true-unreach-call.i unreach-call true 2 34     34     2300 400    0      0      - - - - out of memory 0 890    850    7000 0   0      timeout 0 960     950     970   .63  0     
array-multidimensional/copy-3-n-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 32     32     2400 350    0      0      - - - - error (invalid witness file) 0 .76 .47 40 0   0      error (2) 0 .021 .021 5.6 0     0     
array-multidimensional/copy-partial-2-n-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 35     35     2500 430    0      0      - - - - error (invalid witness file) 0 .74 .45 40 0   0      error (2) 0 .023 .024 5.6 0     0     
array-multidimensional/copy-partial-3-u_true-unreach-call.i unreach-call probably out of memory (killed (signal 9, verification)) 0 170     180     15000 2600    .15   0      - - - - error (invalid witness file) 0 .76 .47 41 0   0      error (2) 0 .021 .022 5.6 0     0     
array-multidimensional/diff-2-n-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 34     34     2300 360    0      0      - - - - error (invalid witness file) 0 .77 .47 40 0   0      error (2) 0 .022 .023 5.7 0     0     
array-multidimensional/diff-3-n-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 29     29     2300 430    0      0      - - - - error (invalid witness file) 0 .61 .38 41 0   0      error (2) 0 .021 .022 5.6 0     0     
array-multidimensional/init-2-n-u_true-unreach-call.i unreach-call true 2 13     13     990 210    0      .28   - - - - timeout 0 900    880    7000 0   0      timeout 0 960     950     930   .63  0     
array-multidimensional/init-3-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 36     36     4000 490    0      0      - - - - error (invalid witness file) 0 .76 .46 42 0   0      error (2) 0 .020 .021 5.6 0     0     
array-multidimensional/init-4-n-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 41     42     4200 580    0      0      - - - - error (invalid witness file) 0 .57 .35 40 0   0      error (2) 0 .023 .025 5.6 0     0     
array-multidimensional/init-non-constant-2-n-u_true-unreach-call.i unreach-call timeout (verification) 0 900     900     5700 12000    .033  0      - - - - error (invalid witness file) 0 .64 .38 41 0   0      error (2) 0 .020 .021 5.6 0     0     
array-multidimensional/init-non-constant-3-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 19     19     2900 250    0      0      - - - - error (invalid witness file) 0 .59 .37 41 0   0      error (2) 0 .021 .022 5.6 0     0     
array-multidimensional/max-2-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 35     35     2400 390    0      0      - - - - error (invalid witness file) 0 .58 .35 40 0   0      error (2) 0 .026 .026 5.6 0     0     
array-multidimensional/max-3-n-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 32     32     2400 370    0      0      - - - - error (invalid witness file) 0 .64 .39 42 0   0      error (2) 0 .023 .023 5.6 0     0     
array-multidimensional/min-2-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 35     35     2400 430    0      0      - - - - error (invalid witness file) 0 .70 .44 42 0   0      error (2) 0 .022 .023 5.6 0     0     
array-multidimensional/min-3-n-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 31     31     2400 430    0      0      - - - - error (invalid witness file) 0 .75 .46 42 0   0      error (2) 0 .021 .022 5.6 0     0     
array-multidimensional/rev-2-n-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 35     35     2400 400    0      0      - - - - error (invalid witness file) 0 .58 .36 40 0   0      error (2) 0 .024 .025 5.5 0     0     
array-multidimensional/rev-3-u_true-unreach-call.i unreach-call error(unknown, verification-finished) 0 30     30     2400 350    0      0      - - - - error (invalid witness file) 0 .72 .43 40 0   0      error (2) 0 .022 .022 5.6 0     0     
array-multidimensional/transpose-u_true-unreach-call.i unreach-call true 2 36     36     2300 500    0      0      - - - - out of memory 0 700    670    7000 0   .52   timeout 0 960     950     480   .63  0     
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i unreach-call false(unreach-call) 1 .35  .34  19 4.1  0      0      false(unreach-call) 1 4.6  2.5  250 0      0      true -32 7.7   4.8   300   .62  0   false(unreach-call) 1 3.9  2.3  250 0      0      false(unreach-call) 1 .59   .59   20    .057 0      - -
bitvector/sum02_false-unreach-call_true-no-overflow.i unreach-call timeout (verification) 0 900     900     370 11000    .025  0      error (invalid witness file) 0 .55 .34 40 0      0      error (2) 0 .025 .027 5.6 0     0   error (invalid witness file) 0 .93 .60 47 0      0      error (invalid witness file) 0 .0065 .0083 .52 0     0      - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i unreach-call true 2 .37  .36  18 4.5  0      0      - - - - true 2 12    6.2  370 0   0      timeout 0 960     920     1000   .78  0     
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i unreach-call true 2 .36  .35  18 4.3  0      0      - - - - true 2 9.8  5.4  370 0   0      timeout 0 960     920     1000   1.5   0     
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unreach-call true 2 .51  .50  21 7.2  0      .28   - - - - true 2 11    8.6  320 0   0      timeout 0 960     950     540   .63  0     
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unreach-call true 2 26     26     42 350    0      0      - - - - true 2 170    160    560 0   0      timeout 0 960     950     640   1.5   0     
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unreach-call true 2 33     33     42 530    0      0      - - - - true 2 120    120    560 0   0      timeout 0 960     950     950   .65  0     
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i unreach-call true 2 .16  .16  15 1.5  0      0      - - - - true 2 7.2  4.7  320 0   .0041 true 2 42     32     590   .62  0     
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i unreach-call true 2 .17  .17  18 2.1  0      0      - - - - true 2 14    9.1  380 0   0      true 2 220     200     660   .71  0     
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i unreach-call timeout (verification) 0 900     900     340 8100    .025  0      - - - - error (invalid witness file) 0 .70 .43 40 0   0      error (2) 0 .027 .028 5.6 0     0     
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i unreach-call timeout (verification) 0 900     900     440 7300    .016  0      - - - - error (invalid witness file) 0 .77 .46 41 0   0      error (2) 0 .027 .027 5.6 0     0     
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i unreach-call probably out of memory (killed (signal 9, verification)) 0 170     180     15000 2400    .21   0      - - - - error (invalid witness file) 0 .70 .43 40 0   0      error (2) 0 .022 .023 5.6 0     0     
bitvector/jain_5_true-unreach-call_true-no-overflow.i unreach-call probably out of memory (killed (signal 9, verification)) 0 180     180     15000 2400    .16   0      - - - - error (invalid witness file) 0 .59 .37 40 0   0      error (2) 0 .026 .027 5.6 0     0     
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i unreach-call probably out of memory (killed (signal 9, verification)) 0 170     180     15000 2700    .17   0      - - - - error (invalid witness file) 0 .60 .36 40 0   0      error (2) 0 .026 .028 5.6 0     0     
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i unreach-call probably out of memory (killed (signal 9, verification)) 0 170     180     15000 3000    .094  .0041 - - - - error (invalid witness file) 0 .74 .47 41 0   0      error (2) 0 .024 .025 5.6 0     0     
bitvector/modulus_true-unreach-call_true-no-overflow.i unreach-call timeout (verification) 0 900     900     150 11000    .029  0      - - - - error (invalid witness file) 0 .68 .42 40 0   0      error (2) 0 .028 .028 5.5 0     0     
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i unreach-call true 2 .15  .15  15 1.7  0      0      - - - - true 2 6.0  3.2  280 0   0      true 2 37     24     560   .71  0     
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i unreach-call true 2 .19  .19  17 2.2  0      .0041 - - - - true 2 6.4  3.5  290 0   0      timeout 0 960     930     2200   .72  0     
bitvector/parity_true-unreach-call_true-no-overflow.i unreach-call true 2 26     26     25 360    0      0      - - - - true 2 36    27    470 0   0      timeout 0 960     950     1100   .75  .074 
bitvector/sum02_true-unreach-call_true-no-overflow.i unreach-call timeout (verification) 0 900     900     380 10000    .025  0      - - - - error (invalid witness file) 0 .71 .43 40 0   0      error (2) 0 .022 .022 5.6 0     0     
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c unreach-call false(unreach-call) 1 1.3   1.3   20 18    0      0      false(unreach-call) 1 15    8.5  430 0      .041  true -32 8.4   5.2   310   .62  0   unknown 0 4.3  2.4  250 0      0      true -32 .62   .62   20    .12  0      - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c unreach-call false(unreach-call) 1 1.8   1.8   20 23    0      0      false(unreach-call) 1 29    21    480 0      0      true -32 8.4   4.7   310   .66  0   unknown 0 5.6  3.2  260 0      0      true -32 .65   .65   20    .11  0      - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c unreach-call false(unreach-call) 1 .52  .52  18 6.5  0      0      false(unreach-call) 1 9.6  5.1  420 0      0      true -32 8.4   4.8   310   .62  0   unknown 0 5.6  3.1  250 0      0      true -32 .63   .63   20    .11  0      - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call true 2 .96  .96  18 12    0      0      - - - - true 2 84    73    1000 0   0      true 2 45     27     780   .68  0     
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call true 2 .91  .91  18 14    0      0      - - - - true 2 17    10    600 0   0      true 2 58     33     970   .71  0     
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call true 2 .92  .91  18 12    0      0      - - - - true 2 15    8.3  550 0   0      true 2 31     18     820   .62  0     
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call timeout (verification) 0 900     900     540 9900    .025  0      - - - - error (invalid witness file) 0 .77 .47 41 0   0      error (2) 0 .021 .022 5.7 0     0     
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call timeout (verification) 0 900     900     880 9400    .025  0      - - - - error (invalid witness file) 0 .63 .40 41 0   0      error (2) 0 .021 .022 5.6 0     0     
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c unreach-call timeout (verification) 0 900     900     150 8600    .025  0      - - - - error (invalid witness file) 0 .59 .36 41 0   0      error (2) 0 .027 .028 5.6 0     0     
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c unreach-call timeout (verification) 0 900     900     160 9100    .020  0      - - - - error (invalid witness file) 0 .78 .47 40 0   0      error (2) 0 .025 .026 5.6 0     0     
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call timeout (verification) 0 900     900     230 11000    .025  0      - - - - error (invalid witness file) 0 .74 .45 40 0   0      error (2) 0 .021 .022 5.6 0     0     
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call timeout (verification) 0 900     900     220 11000    .025  0      - - - - error (invalid witness file) 0 .79 .49 42 0   0      error (2) 0 .025 .025 5.6 0     0     
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c unreach-call timeout (verification) 0 900     900     160 11000    .020  0      - - - - error (invalid witness file) 0 .78 .47 42 0   0      error (2) 0 .022 .022 5.6 0     0     
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c unreach-call true 2 2.8   2.8   24 39    0      0      - - - - out of memory 0 760    690    7000 0   0      true 2 41     26     540   .66  0     
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c unreach-call true 1 9.1   9.1   31 130    0      0      - - - - out of memory 0 800    740    7000 0   0      timeout 0 960     900     830   .79  .0041
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c unreach-call timeout (verification) 0 900     900     41 11000    .025  0      - - - - error (invalid witness file) 0 .58 .36 40 0   0      error (2) 0 .021 .022 5.6 0     0     
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c unreach-call true 2 2.8   2.8   24 34    0      0      - - - - out of memory 0 710    650    7000 0   0      true 2 27     16     590   .66  0     
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c unreach-call false(unreach-call) 1 .18  .18  16 1.6  0      0      false(unreach-call) 1 4.0  2.2  250 0      0      false(unreach-call) 1 12     7.4   300   .68  0   false(unreach-call) 1 3.8  2.2  250 0      0      false(unreach-call) 1 .57   .57   20    .041 .0041 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c unreach-call false(unreach-call) 1 .17  .17  16 2.7  0      0      false(unreach-call) 1 4.0  2.3  250 0      .0041 false(unreach-call) 1 6.7   3.8   300   .66  0   false(unreach-call) 1 4.3  2.5  250 0      0      false(unreach-call) 1 .56   .56   20    .041 0      - -
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c unreach-call false(unreach-call) 1 .16  .15  16 2.2  0      0      false(unreach-call) 1 4.4  2.4  250 0      0      false(unreach-call) 1 13     7.8   300   .71  0   false(unreach-call) 1 3.5  2.0  250 0      0      false(unreach-call) 1 .56   .56   20    .041 .0041 - -
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c unreach-call timeout (verification) 0 900     900     660 11000    .025  0      error (invalid witness file) 0 .56 .34 40 0      0      error (2) 0 .021 .021 5.6 0     0   error (invalid witness file) 0 .92 .60 49 0      0      error (invalid witness file) 0 .0020 .0025 .52 0     0      - -
bitvector-regression/signextension2_false-unreach-call_true-termination.c unreach-call false(unreach-call) 1 .16  .15  16 1.7  0      0      false(unreach-call) 1 4.4  2.5  250 0      0      false(unreach-call) 1 6.8   4.4   300   .62  0   false(unreach-call) 1 3.4  2.0  250 0      0      false(unreach-call) 1 .56   .56   20    .045 0      - -
bitvector-regression/signextension_false-unreach-call_true-termination.c unreach-call false(unreach-call) 1 .21  .20  16 1.7  0      0      false(unreach-call) 1 3.9  2.2  250 0      0      false(unreach-call) 1 6.8   3.9   310   .62  0   false(unreach-call) 1 3.4  1.9  250 0      .0041 false(unreach-call) 1 .56   .57   20    .045 0      - -
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c unreach-call true 2 .14  .14  16 1.4  0      0      - - - - true 2 3.7  2.1  250 0   0      true 2 8.0   4.8   310   .66  0     
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c unreach-call true 2 .14  .14  15 1.4  0      0      - - - - true 2 4.3  2.4  250 0   0      true 2 12     7.5   300   .75  .13  
bitvector-regression/signextension2_true-unreach-call_true-termination.c unreach-call true 2 .17  .16  16 1.6  0      0      - - - - true 2 3.9  2.2  250 0   0      true 2 7.8   4.4   310   .66  0     
bitvector-regression/signextension_true-unreach-call_true-termination.c unreach-call true 2 .14  .13  17 1.5  0      0      - - - - true 2 5.0  2.7  250 0   0      true 2 7.3   4.5   310   .62  0     
bitvector-loops/diamond_false-unreach-call2.i unreach-call false(unreach-call) 1 .20  .20  17 2.6  0      0      false(unreach-call) 1 4.6  2.6  250 0      0      true -32 6.9   4.3   300   .62  0   false(unreach-call) 1 4.0  2.3  250 0      0      false(unreach-call) 1 .60   .60   20    .049 0      - -
bitvector-loops/overflow_false-unreach-call1.i unreach-call false(unreach-call) 1 .16  .16  16 2.2  0      0      timeout 0 98    84    1800 0      0      true -32 7.9   4.9   310   .62  0   false(unreach-call) 1 6.8  5.4  240 0      0      false(unreach-call) 1 4.1    4.1    20    .045 0      - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i unreach-call false(unreach-call) 0 .52  .52  18 7.4  0      0      timeout 0 92    88    740 0      0      true -32 7.0   4.1   310   .62  0   true -32 3.9  2.2  250 0      0      true -32 .57   .58   20    .049 0      - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call false(unreach-call) 1 1.0   1.0   29 15    0      0      false(unreach-call) 1 11    5.9  480 0      0      true -32 12     7.3   390   .62  0   unknown 0 4.8  2.7  260 0      0      true -32 .78   .78   20    .29  0      - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call false(unreach-call) 1 .49  .48  20 6.0  0      0      false(unreach-call) 1 11    5.8  390 0      0      true -32 9.8   5.6   320   .62  0   unknown 0 4.5  2.6  260 0      0      true -32 .69   .69   20    .19  .033  - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call false(unreach-call) 1 .76  .76  26 11    0      0      false(unreach-call) 1 11    6.0  400 0      0      true -32 12     7.0   360   .62  0   unknown 0 4.9  2.8  260 0      .049  true -32 .73   .75   20    .24  0      - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call false(unreach-call) 1 .45  .45  18 4.8  0      0      false(unreach-call) 1 6.0  3.3  270 0      0      true -32 9.8   5.5   320   .62  0   unknown 0 5.2  2.9  260 0      0      true -32 .67   .66   20    .16  .033  - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call true 2 .98  .98  28 12    0      0      - - - - true 2 12    6.5  520 0   0      true 2 110     62     1000   .62  0     
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call true 2 .53  .53  22 7.3  0      0      - - - - out of memory 0 480    460    7000 0   0      true 2 66     38     850   .62  0     
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call true 2 .46  .45  21 5.5  0      0      - - - - true 2 9.3  5.1  350 0   0      true 2 77     43     810   .62  0     
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call true 2 .71  .71  26 11    0      0      - - - - true 2 11    5.7  440 0   0      true 2 120     66     870   .62  0     
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call true 2 .26  .26  17 3.5  0      0      - - - - true 2 5.3  2.8  270 0   0      true 2 20     11     530   .55  0     
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call true 2 .38  .38  18 4.1  0      0      - - - - true 2 7.1  3.8  270 0   0      true 2 23     13     490   .12  0     
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c unreach-call false(unreach-call) 1 .56  .55  17 7.6  0      0      false(unreach-call) 1 7.1  3.8  370 0      0      true -32 8.1   4.7   310   .62  0   unknown 0 4.3  2.5  260 0      0      true -32 .64   .63   20    .12  0      - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c unreach-call false(unreach-call) 1 .56  .55  18 6.6  0      0      false(unreach-call) 1 8.9  4.7  370 0      0      true -32 8.3   5.1   320   .62  0   unknown 0 4.2  2.4  260 0      .037  true -32 .64   .64   20    .12  0      - -
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c unreach-call false(unreach-call) 1 .62  .61  18 9.3  0      0      false(unreach-call) 1 8.7  4.7  380 0      0      true -32 8.6   5.3   320   .62  0   unknown 0 4.3  2.5  250 0      0      true -32 .65   .65