Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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-12-01 22:41:19 CET; 2017-12-02 23:08:57 CET; 2017-12-03 01:39:21 CET; 2017-12-03 04:09:48 CET; 2017-12-03 05:53:57 CET] [2017-12-02 21:10:50 CET; 2017-12-03 00:45:11 CET; 2017-12-03 03:55:46 CET; 2017-12-03 05:12:06 CET; 2017-12-03 06:31:42 CET] [2017-12-02 22:39:24 CET; 2017-12-03 01:25:52 CET; 2017-12-03 05:44:30 CET; 2017-12-03 06:32:20 CET] 2017-12-02 22:51:52 CET [2017-12-02 23:01:21 CET; 2017-12-03 01:32:11 CET; 2017-12-03 05:48:14 CET] 2017-12-02 19:44:15 CET [2017-12-02 21:36:25 CET; 2017-12-03 00:52:42 CET; 2017-12-03 05:20:50 CET]
Run set symbiotic.[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-symbiotic.[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-symbiotic.[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-symbiotic.[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-symbiotic.[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-symbiotic.[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-symbiotic.[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 --witness witness.graphml [-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-02_2308.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/symbiotic.2017-12-03_0139.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/symbiotic.2017-12-03_0409.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/symbiotic.2017-12-03_0553.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/symbiotic.2017-12-03_0409.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/symbiotic.2017-12-03_0553.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/symbiotic.2017-12-03_0409.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true [--full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/symbiotic.2017-12-03_0409.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 false(unreach-call) 1 wit inspect 1.6   200   17    timeout 0 wit inspect 92    2600 true -32 wit inspect 3.3   240   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call timeout (timeout) 0 wit inspect 900     4000   9800    error (invalid witness file) 0 wit inspect .50 44 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     4100   12000    error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call timeout (timeout) 0 wit inspect 900     100   8500    error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     100   9900    error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 1.1   140   15    timeout 0 wit inspect 91    2000 true -32 wit inspect 3.4   220   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect 12      18    - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 3.4   300   45    timeout 0 wit inspect 91    1900 true -32 wit inspect 4.4   240   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 4.2   350   59    timeout 0 wit inspect 92    2000 true -32 wit inspect 3.4   220   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 4.5   370   66    timeout 0 wit inspect 92    2000 true -32 wit inspect 4.7   230   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 5.0   400   69    timeout 0 wit inspect 91    2000 true -32 wit inspect 3.4   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 5.3   430   59    timeout 0 wit inspect 92    2000 true -32 wit inspect 3.3   240   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 5.8   470   67    timeout 0 wit inspect 92    2100 true -32 wit inspect 5.0   230   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 6.1   500   71    timeout 0 wit inspect 92    2100 true -32 wit inspect 3.3   220   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 6.5   530   82    timeout 0 wit inspect 91    2100 true -32 wit inspect 3.4   230   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 7.0   560   88    timeout 0 wit inspect 92    2100 true -32 wit inspect 3.8   240   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect .80  71   11    timeout 0 wit inspect 92    850 true -32 wit inspect 3.1   230   unknown 0 wit inspect 2.7  200 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect .42  39   5.7  timeout 0 wit inspect 91    720 true -32 wit inspect 3.1   230   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect .64  68   8.5  timeout 0 wit inspect 92    760 true -32 wit inspect 3.1   230   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect .88  95   12    timeout 0 wit inspect 92    820 true -32 wit inspect 3.5   230   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 1.1   120   15    timeout 0 wit inspect 92    840 true -32 wit inspect 3.5   240   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 1.3   150   18    timeout 0 wit inspect 92    760 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 1.5   180   23    timeout 0 wit inspect 92    660 true -32 wit inspect 4.7   230   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 1.8   200   24    timeout 0 wit inspect 91    730 true -32 wit inspect 3.3   230   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 2.0   230   28    timeout 0 wit inspect 92    690 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i unreach-call false(unreach-call) 1 wit inspect 2.2   260   31    timeout 0 wit inspect 91    690 true -32 wit inspect 3.3   230   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 100     15000   1200    error (invalid witness file) 0 wit inspect .42 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 .0011 .29 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     12000   9400    error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .65 51 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i unreach-call timeout (timeout) 0 wit inspect 900     11000   13000    error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call true 2 wit inspect .15  11   1.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6100 true 2 wit inspect 7.2   280  
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     1300   10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9
array-examples/relax_true-unreach-call.i unreach-call unknown 0 wit inspect 370     180   1900    - 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/sanfoundry_02_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 460     15000   3900    - 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
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     830   11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call timeout (timeout) 0 wit inspect 900     5400   8400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.8
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 100     15000   990    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .032 4.9
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call true 2 wit inspect .15  11   1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 5.0   230  
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     3900   9800    - 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/sorting_selectionsort_true-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     100   8100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .024 4.8
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     10000   10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .024 4.8
array-examples/standard_compare_true-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     11000   11000    - 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/standard_copy1_true-unreach-call_ground.i unreach-call true 2 wit inspect 2.2   130   29    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5400 timeout 0 wit inspect 960     4600  
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call true 2 wit inspect 2.5   150   32    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 timeout 0 wit inspect 960     4800  
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call true 2 wit inspect 2.9   160   34    - 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 true 2 wit inspect 3.2   170   38    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5900 timeout 0 wit inspect 960     4800  
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call true 2 wit inspect 3.5   180   45    - 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 true 2 wit inspect 3.9   190   49    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 timeout 0 wit inspect 960     4800  
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call true 2 wit inspect 4.1   200   50    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 770    7000 timeout 0 wit inspect 960     4900  
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call true 2 wit inspect 4.6   210   71    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 890    7000 timeout 0 wit inspect 960     4900  
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call true 2 wit inspect 5.1   220   61    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6700 timeout 0 wit inspect 960     5000  
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call true 2 wit inspect 1.4   51   18    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3000 timeout 0 wit inspect 960     4800  
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call true 2 wit inspect 1.8   59   27    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 timeout 0 wit inspect 960     5000  
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call true 2 wit inspect 1.5   82   20    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 timeout 0 wit inspect 960     4800  
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call true 2 wit inspect 1.1   41   16    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 timeout 0 wit inspect 960     4400  
array-examples/standard_find_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 530     2400   8300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 45 error (2) 0 wit inspect .020 4.9
array-examples/standard_init1_true-unreach-call_ground.i unreach-call true 2 wit inspect .80  32   10    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5000 timeout 0 wit inspect 960     2000  
array-examples/standard_init2_true-unreach-call_ground.i unreach-call true 2 wit inspect .97  39   14    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 timeout 0 wit inspect 960     2900  
array-examples/standard_init3_true-unreach-call_ground.i unreach-call true 2 wit inspect 1.2   47   17    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 timeout 0 wit inspect 960     4800  
array-examples/standard_init4_true-unreach-call_ground.i unreach-call true 2 wit inspect 1.4   54   21    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 timeout 0 wit inspect 960     5100  
array-examples/standard_init5_true-unreach-call_ground.i unreach-call true 2 wit inspect 1.6   61   23    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 timeout 0 wit inspect 960     5200  
array-examples/standard_init6_true-unreach-call_ground.i unreach-call true 2 wit inspect 1.8   68   27    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 timeout 0 wit inspect 960     5200  
array-examples/standard_init7_true-unreach-call_ground.i unreach-call true 2 wit inspect 2.0   75   27    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     4900  
array-examples/standard_init8_true-unreach-call_ground.i unreach-call true 2 wit inspect 2.2   83   30    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     5000  
array-examples/standard_init9_true-unreach-call_ground.i unreach-call true 2 wit inspect 2.4   90   38    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 timeout 0 wit inspect 960     5600  
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 100     15000   940    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .018 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 100     15000   1000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .020 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call true 2 wit inspect .69  45   8.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5300 timeout 0 wit inspect 960     1600  
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     3800   8200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 16     15000   180    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.9
array-examples/standard_partition_true-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     12000   8700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .017 4.8
array-examples/standard_password_true-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     10000   10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .021 4.9
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call true 2 wit inspect 1.1   75   13    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 timeout 0 wit inspect 960     1800  
array-examples/standard_running_true-unreach-call.i unreach-call timeout (timeout) 0 wit inspect 900     7400   11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .023 4.9
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call timeout (timeout) 0 wit inspect 900     410   9100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .020 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call true 2 wit inspect .93  33   11    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 timeout 0 wit inspect 960     2400  
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call timeout (timeout) 0 wit inspect 900     640   9600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call unknown 0 wit inspect 28     2200   250    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .019 4.8
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call unknown 0 wit inspect 26     2200   180    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_01_true-unreach-call.i unreach-call true 2 wit inspect .38  22   4.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 timeout 0 wit inspect 960     2900  
array-examples/standard_two_index_02_true-unreach-call.i unreach-call true 2 wit inspect 1.9   120   24    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 timeout 0 wit inspect 960     3500  
array-examples/standard_two_index_03_true-unreach-call.i unreach-call true 2 wit inspect .32  20   3.3  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     3100  
array-examples/standard_two_index_04_true-unreach-call.i unreach-call true 2 wit inspect 1.6   120   22    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 timeout 0 wit inspect 960     3100  
array-examples/standard_two_index_05_true-unreach-call.i unreach-call true 2 wit inspect 1.5   120   18    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 timeout 0 wit inspect 960     3000  
array-examples/standard_two_index_06_true-unreach-call.i unreach-call true 2 wit inspect .33  20   3.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     3400  
array-examples/standard_two_index_07_true-unreach-call.i unreach-call true 2 wit inspect 1.5   120   19    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 timeout 0 wit inspect 960     2900  
array-examples/standard_two_index_08_true-unreach-call.i unreach-call true 2 wit inspect 1.5   120   19    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 timeout 0 wit inspect 960     3800  
array-examples/standard_two_index_09_true-unreach-call.i unreach-call true 2 wit inspect 1.4   120   18    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 timeout 0 wit inspect 960     3700  
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call timeout (timeout) 0 wit inspect 900     500   11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call true 2 wit inspect 1.6   170   19    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     2200  
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect .42  44   6.1  timeout 0 wit inspect 92    800 true -32 wit inspect 4.4   220   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect .39  38   4.8  timeout 0 wit inspect 92    940 timeout 0 wit inspect 97     4900   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect 2.0   200   25    timeout 0 wit inspect 91    2100 true -32 wit inspect 3.1   230   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect .45  42   5.9  timeout 0 wit inspect 93    1100 timeout 0 wit inspect 97     4800   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call timeout (timeout) 0 wit inspect 900     3900   9400    error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .88 51 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call timeout (timeout) 0 wit inspect 900     1200   11000    error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call out of memory 0 wit inspect 20     15000   230    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .028 4.8
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call out of memory 0 wit inspect 14     15000   180    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call true 2 wit inspect .86  32   12    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     5000  
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call unknown 0 wit inspect 11     360   140    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.8
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call true 2 wit inspect 3.0   110   41    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6300 true 2 wit inspect 12     460  
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call timeout (timeout) 0 wit inspect 900     3700   8200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call out of memory 0 wit inspect 330     15000   4200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call true 2 wit inspect 2.9   110   34    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 timeout 0 wit inspect 960     5900  
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call true 2 wit inspect 1.9   71   25    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 timeout 0 wit inspect 960     5800  
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call timeout (timeout) 0 wit inspect 900     3700   8000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .017 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call unknown 0 wit inspect .19  11   2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .017 5.0
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect .21  12   2.4  false(unreach-call) 1 wit inspect 7.5  370 true -32 wit inspect 3.6   230   unknown 0 wit inspect 2.8  220 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect .21  13   2.8  timeout 0 wit inspect 92    560 true -32 wit inspect 4.9   240   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect .52  24   7.1  timeout 0 wit inspect 92    680 true -32 wit inspect 3.3   240   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect .46  27   6.0  timeout 0 wit inspect 92    800 true -32 wit inspect 5.1   240   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect .74  32   10    false(unreach-call) 1 wit inspect 50    1600 true -32 wit inspect 3.5   230   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call unknown 0 wit inspect .21  12   2.0  error (invalid witness file) 0 wit inspect .45 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0024 .35 - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect .19  11   1.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1500 timeout 0 wit inspect 960     4800  
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call true 2 wit inspect .19  11   2.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     7000  
reducercommutativity/avg20_true-unreach-call.i unreach-call true 2 wit inspect .20  11   1.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 timeout 0 wit inspect 960     1900  
reducercommutativity/avg40_true-unreach-call.i unreach-call true 2 wit inspect .17  11   1.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3500 timeout 0 wit inspect 960     4300  
reducercommutativity/avg60_true-unreach-call.i unreach-call true 2 wit inspect .18  11   2.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 timeout 0 wit inspect 960     3300  
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call unknown 0 wit inspect .21  12   2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 3.9   14   53    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 110    910 timeout 0 wit inspect 960     4100  
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 200     20   3300    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 timeout 0 wit inspect 960     3300  
reducercommutativity/max20_true-unreach-call.i unreach-call timeout (timeout) 0 wit inspect 900     58   13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 5.0
reducercommutativity/max40_true-unreach-call.i unreach-call timeout (timeout) 0 wit inspect 900     89   12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .018 4.9
reducercommutativity/max60_true-unreach-call.i unreach-call timeout (timeout) 0 wit inspect 900     130   12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 45 error (2) 0 wit inspect .019 4.9
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call unknown 0 wit inspect .21  11   2.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 45 error (2) 0 wit inspect .018 4.8
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect .17  11   1.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1400 timeout 0 wit inspect 960     1800  
reducercommutativity/sep10_true-unreach-call.i unreach-call true 2 wit inspect .19  11   1.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 timeout 0 wit inspect 920     7000  
reducercommutativity/sep20_true-unreach-call.i unreach-call true 2 wit inspect .19  11   2.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 out of memory 0 wit inspect 840     7000  
reducercommutativity/sep40_true-unreach-call.i unreach-call true 2 wit inspect .18  11   2.3  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1700 timeout 0 wit inspect 960     4600  
reducercommutativity/sep60_true-unreach-call.i unreach-call true 2 wit inspect .21  11   2.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 timeout 0 wit inspect 960     3200  
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call unknown 0 wit inspect .20  12   2.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect .19  11   2.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    970 true 2 wit inspect 380     3200  
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call true 2 wit inspect .19  11   2.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     5000  
reducercommutativity/sum20_true-unreach-call.i unreach-call true 2 wit inspect .20  11   2.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 timeout 0 wit inspect 960     4600  
reducercommutativity/sum40_true-unreach-call.i unreach-call true 2 wit inspect .19  11   2.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 timeout 0 wit inspect 960     4600  
reducercommutativity/sum60_true-unreach-call.i unreach-call true 2 wit inspect .19  11   2.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3300 timeout 0 wit inspect 960     3300  
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call unknown 0 wit inspect .20  12   2.2  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .024 4.8
array-tiling/mlceu_false-unreach-call.i unreach-call unknown 0 wit inspect .17  12   2.2  error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0011 .27 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i unreach-call unknown 0 wit inspect .21  12   2.4  error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i unreach-call unknown 0 wit inspect .21  11   2.0  - wit inspect - wit inspect - wit inspect - wit inspect