Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution [2017-11-30 16:01:31 CET; 2017-12-01 09:05:19 CET; 2017-12-01 10:24:45 CET; 2017-12-01 13:07:37 CET; 2017-12-01 15:15:10 CET] [2017-12-01 08:31:47 CET; 2017-12-01 09:58:48 CET; 2017-12-01 12:53:33 CET; 2017-12-01 14:46:42 CET; 2017-12-01 21:58:57 CET] [2017-12-01 08:56:50 CET; 2017-12-01 10:19:41 CET; 2017-12-01 15:12:32 CET; 2017-12-01 21:59:47 CET] 2017-12-01 08:59:39 CET [2017-12-01 09:01:39 CET; 2017-12-01 10:22:00 CET; 2017-12-01 15:13:50 CET] 2017-12-01 08:10:33 CET [2017-12-01 08:38:18 CET; 2017-12-01 10:02:39 CET; 2017-12-01 14:48:36 CET]
Run set depthk.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-ECA; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-ProductLines; sv-comp18.ReachSafety-Recursive; sv-comp18.ReachSafety-Sequentialized; sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other; sv-comp18; sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other; sv-comp18.Termination-MainControlFlow; sv-comp18.Termination-MainHeap; sv-comp18.Termination-Other; sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] cpa-seq-validate-violation-witnesses-depthk.[sv-comp18-violation-witness.ReachSafety-Arrays; sv-comp18-violation-witness.ReachSafety-BitVectors; sv-comp18-violation-witness.ReachSafety-ControlFlow; sv-comp18-violation-witness.ReachSafety-ECA; sv-comp18-violation-witness.ReachSafety-Floats; sv-comp18-violation-witness.ReachSafety-Heap; sv-comp18-violation-witness.ReachSafety-Loops; sv-comp18-violation-witness.ReachSafety-ProductLines; sv-comp18-violation-witness.ReachSafety-Recursive; sv-comp18-violation-witness.ReachSafety-Sequentialized; sv-comp18-violation-witness.MemSafety-Arrays; sv-comp18-violation-witness.MemSafety-Heap; sv-comp18-violation-witness.MemSafety-LinkedLists; sv-comp18-violation-witness.MemSafety-Other; sv-comp18-violation-witness; sv-comp18-violation-witness.NoOverflows-BitVectors; sv-comp18-violation-witness.NoOverflows-Other; sv-comp18-violation-witness.Termination-MainControlFlow; sv-comp18-violation-witness.Termination-MainHeap; sv-comp18-violation-witness.Termination-Other; sv-comp18-violation-witness.Systems_BusyBox_MemSafety; sv-comp18-violation-witness.Systems_BusyBox_NoOverflows; sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety] uautomizer-validate-violation-witnesses-depthk.[sv-comp18-violation-witness.ReachSafety-Arrays; sv-comp18-violation-witness.ReachSafety-BitVectors; sv-comp18-violation-witness.ReachSafety-ControlFlow; sv-comp18-violation-witness.ReachSafety-ECA; sv-comp18-violation-witness.ReachSafety-Floats; sv-comp18-violation-witness.ReachSafety-Heap; sv-comp18-violation-witness.ReachSafety-Loops; sv-comp18-violation-witness.ReachSafety-ProductLines; sv-comp18-violation-witness.ReachSafety-Recursive; sv-comp18-violation-witness.ReachSafety-Sequentialized; sv-comp18-violation-witness.MemSafety-Arrays; sv-comp18-violation-witness.MemSafety-Heap; sv-comp18-violation-witness.MemSafety-LinkedLists; sv-comp18-violation-witness.MemSafety-Other; sv-comp18-violation-witness.NoOverflows-BitVectors; sv-comp18-violation-witness.NoOverflows-Other; sv-comp18-violation-witness.Termination-MainControlFlow; sv-comp18-violation-witness.Termination-MainHeap; sv-comp18-violation-witness.Termination-Other; sv-comp18-violation-witness.Systems_BusyBox_MemSafety; sv-comp18-violation-witness.Systems_BusyBox_NoOverflows; sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety] cpa-witness2test-validate-violation-witnesses-depthk.[sv-comp18-violation-witness.ReachSafety-Arrays; sv-comp18-violation-witness.ReachSafety-BitVectors; sv-comp18-violation-witness.ReachSafety-ControlFlow; sv-comp18-violation-witness.ReachSafety-ECA; sv-comp18-violation-witness.ReachSafety-Floats; sv-comp18-violation-witness.ReachSafety-Heap; sv-comp18-violation-witness.ReachSafety-Loops; sv-comp18-violation-witness.ReachSafety-ProductLines; sv-comp18-violation-witness.ReachSafety-Recursive; sv-comp18-violation-witness.ReachSafety-Sequentialized; sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety] fshell-witness2test-validate-violation-witnesses-depthk.[sv-comp18-violation-witness.ReachSafety-Arrays; sv-comp18-violation-witness.ReachSafety-BitVectors; sv-comp18-violation-witness.ReachSafety-ControlFlow; sv-comp18-violation-witness.ReachSafety-ECA; sv-comp18-violation-witness.ReachSafety-Floats; sv-comp18-violation-witness.ReachSafety-Heap; sv-comp18-violation-witness.ReachSafety-Loops; sv-comp18-violation-witness.ReachSafety-ProductLines; sv-comp18-violation-witness.ReachSafety-Recursive; sv-comp18-violation-witness.ReachSafety-Sequentialized; sv-comp18-violation-witness.MemSafety-Arrays; sv-comp18-violation-witness.MemSafety-Heap; sv-comp18-violation-witness.MemSafety-LinkedLists; sv-comp18-violation-witness.MemSafety-Other; sv-comp18-violation-witness.NoOverflows-BitVectors; sv-comp18-violation-witness.NoOverflows-Other; sv-comp18-violation-witness.Systems_BusyBox_MemSafety; sv-comp18-violation-witness.Systems_BusyBox_NoOverflows; sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety] cpa-seq-validate-correctness-witnesses-depthk.[sv-comp18-correctness-witness.ReachSafety-Arrays; sv-comp18-correctness-witness.ReachSafety-BitVectors; sv-comp18-correctness-witness.ReachSafety-ControlFlow; sv-comp18-correctness-witness.ReachSafety-ECA; sv-comp18-correctness-witness.ReachSafety-Floats; sv-comp18-correctness-witness.ReachSafety-Heap; sv-comp18-correctness-witness.ReachSafety-Loops; sv-comp18-correctness-witness.ReachSafety-ProductLines; sv-comp18-correctness-witness.ReachSafety-Recursive; sv-comp18-correctness-witness.ReachSafety-Sequentialized; sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety] uautomizer-validate-correctness-witnesses-depthk.[sv-comp18-correctness-witness.ReachSafety-Arrays; sv-comp18-correctness-witness.ReachSafety-BitVectors; sv-comp18-correctness-witness.ReachSafety-ControlFlow; sv-comp18-correctness-witness.ReachSafety-ECA; sv-comp18-correctness-witness.ReachSafety-Floats; sv-comp18-correctness-witness.ReachSafety-Heap; sv-comp18-correctness-witness.ReachSafety-Loops; sv-comp18-correctness-witness.ReachSafety-ProductLines; sv-comp18-correctness-witness.ReachSafety-Recursive; sv-comp18-correctness-witness.ReachSafety-Sequentialized; sv-comp18-correctness-witness.MemSafety-Arrays; sv-comp18-correctness-witness.MemSafety-Heap; sv-comp18-correctness-witness.MemSafety-LinkedLists; sv-comp18-correctness-witness.MemSafety-Other; sv-comp18-correctness-witness.NoOverflows-BitVectors; sv-comp18-correctness-witness.NoOverflows-Other; sv-comp18-correctness-witness.Systems_BusyBox_MemSafety; sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows; sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety]
Options [-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const; -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const; -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_1024.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const; -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_1307.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const; -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_1515.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const] [--full-output --validate ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/depthk.2017-12-01_1307.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/depthk.2017-12-01_1515.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true [--graphml-witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/depthk.2017-12-01_1307.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true [--full-output --validate ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/depthk.2017-12-01_1307.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml]
/localhome/dbeyer/comp/sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    750 11000   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .89 50 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call unknown 0 wit inspect 46    160 530   error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call unknown 0 wit inspect 46    160 650   error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .93 50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call unknown 0 wit inspect 890    340 12000   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    360 9100   error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0035 .26 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call unknown 0 wit inspect 900    1400 9700   error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2400 13000   timeout 0 wit inspect 92    2200 timeout 0 wit inspect 97     1400   unknown 0 wit inspect .93 51 error (1) 0 wit inspect .078  9.0  - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    1400 12000   timeout 0 wit inspect 92    1800 timeout 0 wit inspect 96     1200   unknown 0 wit inspect 1.1  54 error (1) 0 wit inspect .080  9.0  - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2400 11000   timeout 0 wit inspect 92    2000 timeout 0 wit inspect 96     1800   unknown 0 wit inspect .99 51 error (1) 0 wit inspect .068  9.1  - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2400 11000   timeout 0 wit inspect 92    2000 timeout 0 wit inspect 97     1700   unknown 0 wit inspect .95 51 error (1) 0 wit inspect .068  9.1  - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2500 12000   timeout 0 wit inspect 92    2400 timeout 0 wit inspect 97     2000   unknown 0 wit inspect .94 53 error (1) 0 wit inspect .072  9.0  - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2200 13000   timeout 0 wit inspect 92    2600 timeout 0 wit inspect 97     2700   unknown 0 wit inspect 1.0  51 error (1) 0 wit inspect .067  9.0  - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2200 13000   timeout 0 wit inspect 92    2400 timeout 0 wit inspect 97     2500   unknown 0 wit inspect .97 51 error (1) 0 wit inspect .071  9.1  - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2200 11000   timeout 0 wit inspect 92    3000 timeout 0 wit inspect 97     2900   unknown 0 wit inspect .99 51 error (1) 0 wit inspect .071  9.1  - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2500 11000   timeout 0 wit inspect 92    2700 timeout 0 wit inspect 97     2600   unknown 0 wit inspect .99 54 error (1) 0 wit inspect .070  9.0  - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    220 9100   error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    700 11000   timeout 0 wit inspect 92    1900 timeout 0 wit inspect 97     1100   unknown 0 wit inspect .95 51 error (1) 0 wit inspect .067  9.1  - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    710 13000   timeout 0 wit inspect 92    1700 timeout 0 wit inspect 96     1100   unknown 0 wit inspect .91 51 error (1) 0 wit inspect .071  9.1  - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    730 12000   timeout 0 wit inspect 92    2000 timeout 0 wit inspect 97     1200   unknown 0 wit inspect .71 51 error (1) 0 wit inspect .068  9.1  - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    700 12000   timeout 0 wit inspect 92    2100 timeout 0 wit inspect 97     1300   unknown 0 wit inspect .98 52 error (1) 0 wit inspect .068  9.1  - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    210 9200   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .86 51 error (invalid witness file) 0 wit inspect .0012 .32 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    240 8400   error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i unreach-call unknown 0 wit inspect 900    270 8300   error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .83 51 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    290 8700   error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i unreach-call unknown 0 wit inspect 900    320 10000   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0012 .31 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call unknown 0 wit inspect 98    110 1400   error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2300 12000   timeout 0 wit inspect 92    2000 timeout 0 wit inspect 97     590   unknown 0 wit inspect .99 51 error (1) 0 wit inspect .069  9.1  - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i unreach-call unknown 0 wit inspect 890    340 9300   error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call unknown 0 wit inspect 890    970 7800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .048 4.8
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 900    260 8100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .034 4.8
array-examples/relax_true-unreach-call.i unreach-call unknown 0 wit inspect 890    190 7100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 320    180 4200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 4.8
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    180 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    3900 11000   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  510 true 2 wit inspect 7.3   260  
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 120    120 1500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.9
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 52    100 720   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 5.0
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 46    160 510   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    300 7800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 47 error (2) 0 wit inspect .020 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    190 9500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .019 4.9
array-examples/standard_compare_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 110    170 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    240 9600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.9
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2200 12000   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    7000 timeout 0 wit inspect 960     4800  
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2200 12000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 timeout 0 wit inspect 960     4800  
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    1400 12000   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 850    7000 timeout 0 wit inspect 960     4900  
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2200 11000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 timeout 0 wit inspect 960     4900  
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    1400 11000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    7000 timeout 0 wit inspect 960     5000  
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2200 11000   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 810    7000 timeout 0 wit inspect 960     4900  
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2200 12000   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 730    7000 timeout 0 wit inspect 960     5100  
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2400 13000   - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 830    7000 timeout 0 wit inspect 960     5000  
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    160 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .018 4.9
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 900    210 9800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.9
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    190 8600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    220 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_find_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2300 13000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 timeout 0 wit inspect 960     4800  
array-examples/standard_init1_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    730 13000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 timeout 0 wit inspect 960     2100  
array-examples/standard_init2_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    770 10000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     4000  
array-examples/standard_init3_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    730 10000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 timeout 0 wit inspect 960     4800  
array-examples/standard_init4_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    770 10000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     5200  
array-examples/standard_init5_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    220 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .019 4.9
array-examples/standard_init6_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 900    240 9600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .023 5.0
array-examples/standard_init7_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    270 9800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .036 4.8
array-examples/standard_init8_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    290 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .023 4.9
array-examples/standard_init9_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 900    320 9000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 46 error (2) 0 wit inspect .020 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 120    120 1600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 5.0
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 100    120 1500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .048 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    160 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .035 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2200 13000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 timeout 0 wit inspect 960     3900  
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2500 12000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 out of memory 0 wit inspect 84     7000  
array-examples/standard_partition_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    270 9600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_password_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 120    180 1400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 900    180 8600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_running_true-unreach-call.i unreach-call unknown 0 wit inspect 890    300 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .029 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call unknown 0 wit inspect 100    75 1000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    780 13000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 timeout 0 wit inspect 960     2100  
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 120    120 1800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call timeout 0 wit inspect 900    2300 11000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     4800  
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 890    270 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_01_true-unreach-call.i unreach-call unknown 0 wit inspect 890    250 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_02_true-unreach-call.i unreach-call unknown 0 wit inspect 890    200 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_two_index_03_true-unreach-call.i unreach-call unknown 0 wit inspect 890    180 8600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 46 error (2) 0 wit inspect .020 4.9
array-examples/standard_two_index_04_true-unreach-call.i unreach-call unknown 0 wit inspect 890    230 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 4.9
array-examples/standard_two_index_05_true-unreach-call.i unreach-call unknown 0 wit inspect 890    220 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .020 4.9
array-examples/standard_two_index_06_true-unreach-call.i unreach-call unknown 0 wit inspect 890    180 8600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .034 4.8
array-examples/standard_two_index_07_true-unreach-call.i unreach-call unknown 0 wit inspect 890    230 9200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .020 4.8
array-examples/standard_two_index_08_true-unreach-call.i unreach-call unknown 0 wit inspect 890    190 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_09_true-unreach-call.i unreach-call unknown 0 wit inspect 890    180 8700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call unknown 0 wit inspect 98    100 1400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    2400 12000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     2100  
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call unknown 0 wit inspect 890    330 9300   error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call unknown 0 wit inspect 890    300 9800   error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call unknown 0 wit inspect 890    250 9900   error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0012 .35 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call unknown 0 wit inspect 890    190 9700   error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0035 .28 - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call unknown 0 wit inspect 890    250 9600   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call timeout 0 wit inspect 900    5900 9600   timeout 0 wit inspect 91    2500 timeout 0 wit inspect 97     1300   unknown 0 wit inspect 1.0  52 error (1) 0 wit inspect .073  9.1  - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call unknown 0 wit inspect 890    230 9000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .029 4.8
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call unknown 0 wit inspect 890    1700 9800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call unknown 0 wit inspect 890    220 9400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 44 error (2) 0 wit inspect .020 4.9
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900    3700 7100   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 timeout 0 wit inspect 960     6000  
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call unknown 0 wit inspect 540    650 5000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .023 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4100 8200   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 timeout 0 wit inspect 960     6000  
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call unknown 0 wit inspect 890    230 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .047 5.0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call unknown 0 wit inspect 890    250 9500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call unknown 0 wit inspect 890    430 8600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call unknown 0 wit inspect 890    390 9500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .018 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    4100 8700   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6200 timeout 0 wit inspect 960     4500  
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call false(unreach-call) 0 wit inspect 490    210 5400   true -32 wit inspect 3.7  260 true -32 wit inspect 5.3   260   unknown 0 wit inspect 2.2  210 error (2) 0 wit inspect .61   19    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call false(unreach-call) 0 wit inspect 500    210 6800   true -32 wit inspect 4.1  270 true -32 wit inspect 5.5   270   unknown 0 wit inspect 3.5  220 error (2) 0 wit inspect .62   19    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i unreach-call false(unreach-call) 0 wit inspect 640    210 8400   true -32 wit inspect 3.1  270 true -32 wit inspect 5.7   320   unknown 0 wit inspect 3.8  220 error (2) 0 wit inspect .66   19    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i unreach-call unknown 0 wit inspect 890    250 12000   error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0011 .35 - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i unreach-call unknown 0 wit inspect 890    210 13000   error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect 490    210 6000   timeout 0 wit inspect 92    1900 true -32 wit inspect 5.2   250   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    2200 11000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1500 timeout 0 wit inspect 960     5400  
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    3400 11000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 out of memory 0 wit inspect 900     7000  
reducercommutativity/avg20_true-unreach-call.i unreach-call timeout 0 wit inspect 900    700 6500   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     1700  
reducercommutativity/avg40_true-unreach-call.i unreach-call unknown 0 wit inspect 890    260 7300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8
reducercommutativity/avg60_true-unreach-call.i unreach-call unknown 0 wit inspect 890    260 8300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call unknown 0 wit inspect 890    180 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .023 4.8
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    1500 10000   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 81    870 timeout 0 wit inspect 960     1300  
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    2400 8700   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 timeout 0 wit inspect 960     3300  
reducercommutativity/max20_true-unreach-call.i unreach-call unknown 0 wit inspect 890    190 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
reducercommutativity/max40_true-unreach-call.i unreach-call unknown 0 wit inspect 890    270 7900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.9
reducercommutativity/max60_true-unreach-call.i unreach-call unknown 0 wit inspect 890    230 8900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.9
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call unknown 0 wit inspect 890    250 9400   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 timeout 0 wit inspect 960     880  
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 790    1600 9900   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 830    1500 timeout 0 wit inspect 960     1700  
reducercommutativity/sep10_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4900 9200   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1700 out of memory 0 wit inspect 880     7000  
reducercommutativity/sep20_true-unreach-call.i unreach-call unknown 0 wit inspect 900    190 10000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 900     7000  
reducercommutativity/sep40_true-unreach-call.i unreach-call unknown 0 wit inspect 900    190 9400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 5.0
reducercommutativity/sep60_true-unreach-call.i unreach-call unknown 0 wit inspect 890    190 9400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.8
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call unknown 0 wit inspect 890    190 7500   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 timeout 0 wit inspect 960     3000  
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    4000 10000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    900 true 2 wit inspect 320     3500  
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    1900 13000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     5400  
reducercommutativity/sum20_true-unreach-call.i unreach-call unknown 0 wit inspect 890    240 8100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9
reducercommutativity/sum40_true-unreach-call.i unreach-call unknown 0 wit inspect 890    200 9000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 45 error (2) 0 wit inspect .020 4.8
reducercommutativity/sum60_true-unreach-call.i unreach-call unknown 0 wit inspect 890    230 6900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.8
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call unknown 0 wit inspect 890    200 9000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     4800  
array-tiling/mlceu_false-unreach-call.i unreach-call timeout 0 wit inspect 900    3500 7800   timeout 0 wit inspect 92    1600 timeout 0 wit inspect 96     1000   unknown 0 wit inspect .96 53 error (1) 0 wit inspect .066  9.0  - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i unreach-call false(unreach-call) 0 wit inspect 1.1  100 13   timeout 0 wit inspect 92    2000 true -32 wit inspect 4.9   230   unknown 0 wit inspect 3.2  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i unreach-call unknown 0 wit inspect 890    160 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .018 4.9
array-tiling/mbpr3_true-unreach-call.i unreach-call unknown 0 wit inspect 890    220 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .051 4.9
array-tiling/mbpr4_true-unreach-call.i unreach-call unknown 0 wit inspect 890    300 9100   - wit inspect - wit inspect - wit inspect - wit