Tool CPAchecker 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-12-05 07:52:24 CET; 2017-12-05 13:45:25 CET; 2017-12-05 13:47:25 CET] [2017-12-05 13:10:09 CET; 2017-12-05 13:45:41 CET; 2017-12-05 13:47:38 CET] [2017-12-05 13:34:02 CET; 2017-12-05 13:46:04 CET; 2017-12-05 13:48:02 CET] 2017-12-05 13:37:41 CET [2017-12-05 13:41:35 CET; 2017-12-05 13:46:15 CET; 2017-12-05 13:48:17 CET] 2017-12-05 12:37:13 CET [2017-12-05 13:13:01 CET; 2017-12-05 13:45:52 CET; 2017-12-05 13:47:50 CET]
Run set interpchecker.[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; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] cpa-seq-validate-violation-witnesses-interpchecker.[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; sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety] uautomizer-validate-violation-witnesses-interpchecker.[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; sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety] cpa-witness2test-validate-violation-witnesses-interpchecker.[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-interpchecker.[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; sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety] cpa-seq-validate-correctness-witnesses-interpchecker.[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-interpchecker.[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; sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety]
Options -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions [-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_1345.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/interpchecker.2017-12-05_1347.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/interpchecker.2017-12-05_1345.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/interpchecker.2017-12-05_1347.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/interpchecker.2017-12-05_1345.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/interpchecker.2017-12-05_1347.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true [--full-output --validate ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/interpchecker.2017-12-05_1345.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/interpchecker.2017-12-05_1347.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    5100 11000   error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0044 .34 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call timeout 0 wit inspect 900    5000 11000   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .79 47 error (invalid witness file) 0 wit inspect .0034 .29 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 910    5000 12000   error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0039 .29 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call timeout 0 wit inspect 900    4800 10000   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0044 .30 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4900 12000   error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .050 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0048 .35 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 910    4600 11000   error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .043 4.8 error (invalid witness file) 0 wit inspect .86 51 error (invalid witness file) 0 wit inspect .0019 .26 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4500 11000   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .87 51 error (invalid witness file) 0 wit inspect .0045 .29 - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4400 10000   error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0042 .31 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4400 11000   error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0041 .31 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4400 11000   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .042 5.0 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0033 .32 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4300 12000   error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4200 11000   error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4300 12000   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0031 .30 - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4200 11000   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .83 48 error (invalid witness file) 0 wit inspect .0049 .29 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4300 13000   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .81 51 error (invalid witness file) 0 wit inspect .0038 .34 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4200 11000   error (invalid witness file) 0 wit inspect .51 45 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .80 49 error (invalid witness file) 0 wit inspect .0041 .31 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4500 13000   error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0035 .33 - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4400 13000   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .050 4.9 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0035 .32 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4200 11000   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .045 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4000 12000   error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0041 .36 - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4000 13000   error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0040 .30 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    3900 12000   error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0036 .32 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4000 11000   error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .043 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0041 .34 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    3900 13000   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0011 .30 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4000 12000   error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .85 51 error (invalid witness file) 0 wit inspect .0039 .34 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    5100 13000   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 51 error (invalid witness file) 0 wit inspect .0052 .26 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4200 14000   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i unreach-call timeout 0 wit inspect 900    4100 12000   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .040 4.8 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0042 .29 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call timeout 0 wit inspect 900    5000 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .022 4.8
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    5100 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .047 4.9
array-examples/relax_true-unreach-call.i unreach-call timeout 0 wit inspect 900    5300 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    5100 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .019 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4600 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .019 5.0
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    4300 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .018 5.0
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    5100 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call true 2 wit inspect 2.5  270 23   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  280 true 2 wit inspect 4.3   220  
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    5000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .020 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4800 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .046 4.8
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4600 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .023 4.9
array-examples/standard_compare_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    5000 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 4.8
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4500 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4500 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .040 4.9
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4300 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .047 5.0
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4300 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .031 4.8
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4300 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .052 4.9
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4200 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .023 4.8
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4100 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .023 4.9
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4100 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .043 4.8
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4200 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.9
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4200 12000   - 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_copyInitSum3_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4000 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .017 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4200 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .018 5.0
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4300 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .048 4.8
array-examples/standard_find_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4600 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .018 4.9
array-examples/standard_init1_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4500 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 5.0
array-examples/standard_init2_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4400 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.8
array-examples/standard_init3_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4200 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9
array-examples/standard_init4_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .024 4.8
array-examples/standard_init5_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4000 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .048 5.0
array-examples/standard_init6_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    3900 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .049 4.8
array-examples/standard_init7_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 4.9
array-examples/standard_init8_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    3900 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_init9_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    3900 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .050 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    5100 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .019 5.0
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    5100 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .040 4.9
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4700 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .025 5.0
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4800 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .052 4.9
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4600 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .025 4.8
array-examples/standard_partition_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 910    4200 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 46 error (2) 0 wit inspect .018 4.8
array-examples/standard_password_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    5000 11000   - 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/standard_reverse_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4500 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .018 4.8
array-examples/standard_running_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4100 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .052 4.9
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    4800 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 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    4600 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .018 4.8
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 910    5000 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .77 44 error (2) 0 wit inspect .050 4.8
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4500 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 46 error (2) 0 wit inspect .043 4.9
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4500 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .024 4.9
array-examples/standard_two_index_01_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4100 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .050 4.9
array-examples/standard_two_index_02_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4300 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_03_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4300 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .021 4.8
array-examples/standard_two_index_04_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4400 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 4.8
array-examples/standard_two_index_05_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4500 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .047 4.9
array-examples/standard_two_index_06_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4600 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .023 4.8
array-examples/standard_two_index_07_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4500 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .049 5.0
array-examples/standard_two_index_08_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4500 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .022 4.8
array-examples/standard_two_index_09_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4500 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call timeout 0 wit inspect 900    4200 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .019 4.8
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900    4400 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .049 4.9
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    4000 11000   error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .038 5.0 error (invalid witness file) 0 wit inspect .79 51 error (invalid witness file) 0 wit inspect .0039 .31 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call timeout 0 wit inspect 900    4000 12000   error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0041 .30 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    4200 12000   error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call timeout 0 wit inspect 900    4200 11000   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .028 4.9 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    4200 12000   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .90 47 error (invalid witness file) 0 wit inspect .0041 .35 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call timeout 0 wit inspect 900    4800 11000   error (invalid witness file) 0 wit inspect .50 44 error (2) 0 wit inspect .029 5.0 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0037 .30 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    4200 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .025 4.8
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    4300 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .024 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4000 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .048 4.8
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4100 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4500 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4200 11000   - 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-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4300 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 4.9
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4100 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .047 4.9
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4200 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .047 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    5000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .018 4.9
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect 42    1500 380   true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 45     4000   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect 55    2400 490   true -32 wit inspect 4.0  280 out of memory 0 wit inspect 66     7000   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .64   20    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect 360    3900 4500   true -32 wit inspect 4.8  280 out of memory 0 wit inspect 61     7000   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .65   20    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect 220    3900 2900   true -32 wit inspect 5.5  280 out of memory 0 wit inspect 64     7000   unknown 0 wit inspect 4.6  230 false(unreach-call) 1 wit inspect .71   22    - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect 740    4400 8600   true -32 wit inspect 6.4  280 out of memory 0 wit inspect 73     7000   unknown 0 wit inspect 4.5  220 false(unreach-call) 1 wit inspect .80   24    - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call false(unreach-call) 0 wit inspect 19    970 160   timeout 0 wit inspect 91    1900 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.8  210 error (1) 0 wit inspect .57   18    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call false(unreach-call) -16 wit inspect 45    2000 380   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 true 2 wit inspect 6.0   270  
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call false(unreach-call) -16 wit inspect 110    3700 1200   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3300 true 2 wit inspect 5.9   290  
reducercommutativity/avg20_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4400 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .024 5.0
reducercommutativity/avg40_true-unreach-call.i unreach-call false(unreach-call) -16 wit inspect 210    3900 2500   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  300 out of memory 0 wit inspect 61     7000  
reducercommutativity/avg60_true-unreach-call.i unreach-call false(unreach-call) -16 wit inspect 790    4600 9100   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  290 out of memory 0 wit inspect 66     7000  
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call false(unreach-call) -16 wit inspect 13    610 100   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 true 2 wit inspect 4.5   230  
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    4500 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 45 error (2) 0 wit inspect .040 4.9
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900    4300 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .044 5.0
reducercommutativity/max20_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4400 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .018 4.8
reducercommutativity/max40_true-unreach-call.i unreach-call false(unreach-call) -16 wit inspect 540    4100 6600   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  280 out of memory 0 wit inspect 65     7000  
reducercommutativity/max60_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4200 10000   - 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
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call false(unreach-call) -16 wit inspect 31    1500 260   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 true 2 wit inspect 4.5   240  
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 160    3800 1800   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 timeout 0 wit inspect 960     1700  
reducercommutativity/sep10_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4500 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .047 4.8
reducercommutativity/sep20_true-unreach-call.i unreach-call timeout 0 wit inspect 900    4600 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .050 4.9
reducercommutativity/sep40_true-unreach-call.i unreach-call false(unreach-call) -16 wit inspect 640    4500 8500   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0  280 out of memory 0 wit inspect 60     7000  
reducercommutativity/sep60_true-unreach-call.i unreach-call timeout 0 wit inspect 910    4200 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call false(unreach-call) -16 wit inspect 390    4100 4900   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 true 2 wit inspect 6.0   290  
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 46    1600 310   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    970 true 2 wit inspect 340     3100  
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 110    3100 1400   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     5100  
reducercommutativity/sum20_true-unreach-call.i unreach-call true 2 wit inspect 690    4000 9000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 timeout 0 wit inspect 960     4600  
reducercommutativity/sum40_true-unreach-call.i unreach-call false(unreach-call) -16 wit inspect 210    3900 2300   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0  280 out of memory 0 wit inspect 68     7000  
reducercommutativity/sum60_true-unreach-call.i unreach-call false(unreach-call) -16 wit inspect 800    4600 9100   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6  280 out of memory 0 wit inspect 76     7000  
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call false(unreach-call) -16 wit inspect 9.2  470 76   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 true 2 wit inspect 5.0   230  
array-tiling/mlceu_false-unreach-call.i unreach-call timeout 0 wit inspect 900    5100 14000   error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .82 50 error (invalid witness file) 0 wit inspect .0039 .30 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i unreach-call false(unreach-call) 0 wit inspect 160    3700 1900   true -32 wit inspect 4.7  280 out of memory 0 wit inspect 73     7000   unknown 0 wit inspect 3.8  220 true -32 wit inspect .64   20    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i unreach-call false(unreach-call) -16 wit inspect 42    2200 330   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    2600 error (7) 0 wit inspect 100     730  
array-tiling/mbpr3_true-unreach-call.i unreach-call false(unreach-call) -16 wit inspect 380    3900 4300   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  280 out of memory 0 wit inspect 58     7000  
array-tiling/mbpr4_true-unreach-call.i unreach-call false(unreach-call) -16 wit inspect 94    3700 900   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    4000 error (7) 0 wit inspect 100     1100  
array-tiling/mbpr5_true-unreach-call.i unreach-call false(unreach-call) -16 wit