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