Tool ULTIMATE Taipan 0.1.23-3204b741 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-02 17:23:13 CET; 2017-12-03 07:53:44 CET; 2017-12-03 08:41:41 CET; 2017-12-03 08:43:49 CET; 2017-12-03 09:20:08 CET] [2017-12-03 07:22:17 CET; 2017-12-03 08:20:31 CET; 2017-12-03 08:42:28 CET; 2017-12-03 08:58:51 CET; 2017-12-03 09:21:20 CET] [2017-12-03 07:45:29 CET; 2017-12-03 08:37:50 CET; 2017-12-03 09:15:45 CET; 2017-12-03 09:21:50 CET] 2017-12-03 07:47:53 CET [2017-12-03 07:50:34 CET; 2017-12-03 08:38:58 CET; 2017-12-03 09:17:25 CET] 2017-12-03 06:47:45 CET [2017-12-03 07:25:40 CET; 2017-12-03 08:21:58 CET; 2017-12-03 09:00:18 CET]
Run set utaipan.[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-utaipan.[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-utaipan.[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-utaipan.[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-utaipan.[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-utaipan.[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-utaipan.[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 --full-output [-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-03_0753.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/utaipan.2017-12-03_0841.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/utaipan.2017-12-03_0843.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/utaipan.2017-12-03_0920.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/utaipan.2017-12-03_0753.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/utaipan.2017-12-03_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/utaipan.2017-12-03_0920.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/utaipan.2017-12-03_0753.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/utaipan.2017-12-03_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true [--full-output --validate ../../results-verified/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/utaipan.2017-12-03_0753.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/utaipan.2017-12-03_0843.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     4100   12000     error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .039 4.9 error (invalid witness file) 0 wit inspect .80 51 error (invalid witness file) 0 wit inspect .0041 .32 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call timeout 0 wit inspect 900     2900   14000     error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .045 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     2800   12000     error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0033 .34 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call timeout 0 wit inspect 900     2000   11000     error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .047 5.0 error (invalid witness file) 0 wit inspect .81 50 error (invalid witness file) 0 wit inspect .0046 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     2600   12000     error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .045 4.8 error (invalid witness file) 0 wit inspect .79 50 error (invalid witness file) 0 wit inspect .0041 .29 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5500   12000     error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0039 .34 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1700   12000     error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .84 51 error (invalid witness file) 0 wit inspect .0035 .35 - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1000   10000     error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0012 .33 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1100   11000     error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .91 49 error (invalid witness file) 0 wit inspect .0042 .30 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1400   12000     error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0038 .34 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1500   12000     error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .052 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0042 .26 - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1600   9400     error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .045 5.0 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0016 .33 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1700   7700     error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0013 .35 - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1800   11000     error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .050 4.9 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0045 .29 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     2000   10000     error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0046 .26 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     880   10000     error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .050 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0046 .29 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1100   11000     error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .027 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0015 .31 - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     760   13000     error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .89 50 error (invalid witness file) 0 wit inspect .0035 .31 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     780   10000     error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .050 4.8 error (invalid witness file) 0 wit inspect .80 48 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     730   12000     error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0041 .30 - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     720   11000     error (invalid witness file) 0 wit inspect .51 45 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .79 47 error (invalid witness file) 0 wit inspect .0019 .29 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     770   12000     error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .043 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0040 .34 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     840   11000     error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .048 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0041 .30 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     920   10000     error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .051 5.0 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0035 .32 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     930   11000     error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0047 .26 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     2900   15000     error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0042 .26 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     2800   12000     error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0018 .32 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i unreach-call timeout 0 wit inspect 900     6300   11000     error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .043 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0041 .34 - 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 6.2   300   48     - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 true 2 wit inspect 8.0   270  
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     2500   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .046 4.9
array-examples/relax_true-unreach-call.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 .53 41 error (2) 0 wit inspect .018 4.9
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     3300   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .022 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1100   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .051 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 6.5   300   59     - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  490 true 2 wit inspect 6.8   270  
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     3000   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .049 4.9
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call true 2 wit inspect 4.5   250   35     - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 4.4   220  
array-examples/sorting_bubblesort_true-unreach-call_ground.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 .56 45 error (2) 0 wit inspect .024 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     2500   14000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     2700   9500     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.9
array-examples/standard_compare_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     3900   15000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .023 4.8
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1000   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .019 4.8
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     940   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .018 4.9
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1000   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .049 5.0
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1100   9200     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .039 4.8
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1300   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .026 5.0
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1500   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .025 4.8
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1500   9300     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .018 4.9
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1900   7700     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.9
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     2100   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 4.9
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     780   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     780   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 45 error (2) 0 wit inspect .018 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1000   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.8
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     910   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .023 4.9
array-examples/standard_find_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1300   12000     - 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-examples/standard_init1_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     890   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.8
array-examples/standard_init2_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     790   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .048 4.9
array-examples/standard_init3_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     890   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_init4_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     770   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.8
array-examples/standard_init5_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     850   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .045 5.0
array-examples/standard_init6_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     790   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.9
array-examples/standard_init7_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     800   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_init8_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     910   9800     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9
array-examples/standard_init9_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     910   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .018 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 910     4300   9700     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 5.0
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4400   9200     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .024 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     850   9900     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .048 4.8
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     2100   9400     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .020 4.9
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 910     15000   3400     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .042 4.9
array-examples/standard_partition_true-unreach-call_ground.i unreach-call error (7) 0 wit inspect 32     720   310     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .048 4.8
array-examples/standard_password_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     3500   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .050 4.8
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     980   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_running_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1000   8300     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .029 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 7.6   440   58     - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    990 true 2 wit inspect 5.3   260  
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     790   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .048 4.9
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     3500   7700     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1300   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .023 4.9
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     1400   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_two_index_01_true-unreach-call.i unreach-call timeout 0 wit inspect 900     970   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.9
array-examples/standard_two_index_02_true-unreach-call.i unreach-call timeout 0 wit inspect 900     870   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.8
array-examples/standard_two_index_03_true-unreach-call.i unreach-call timeout 0 wit inspect 900     880   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .045 4.8
array-examples/standard_two_index_04_true-unreach-call.i unreach-call timeout 0 wit inspect 900     960   9900     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .017 4.9
array-examples/standard_two_index_05_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1100   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 45 error (2) 0 wit inspect .049 4.9
array-examples/standard_two_index_06_true-unreach-call.i unreach-call timeout 0 wit inspect 900     980   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .017 4.8
array-examples/standard_two_index_07_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1100   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 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     1300   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_two_index_09_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1300   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .024 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call timeout 0 wit inspect 900     2900   14000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .019 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     850   9300     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .047 4.9
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     1100   12000     error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0037 .29 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call timeout 0 wit inspect 900     5200   7100     error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0042 .28 - 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     2000   9900     error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0043 .26 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call timeout 0 wit inspect 900     5000   8700     error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0041 .30 - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     1800   11000     error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .042 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0035 .34 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call timeout 0 wit inspect 900     4400   12000     error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0040 .28 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     910   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 5.0
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     1900   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .048 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call timeout 0 wit inspect 900     5300   8700     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900     5800   8100     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call true 2 wit inspect 14     640   110     - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    7000 true 2 wit inspect 10     450  
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call timeout 0 wit inspect 900     5800   7000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 5.0
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900     6100   8700     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900     5900   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .020 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900     6000   9700     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 4.9
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900     5900   8000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .018 5.0
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     1400   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.9
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect 25     840   230     true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 7.4   340   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 31     1000   240     true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 44     4100   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .61   20    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i unreach-call unknown 0 wit inspect 90     1400   890     error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .80 47 error (invalid witness file) 0 wit inspect .0036 .31 - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i unreach-call unknown 0 wit inspect 55     1900   530     error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .042 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0039 .29 - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i unreach-call unknown 0 wit inspect 600     2400   8100     error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .034 4.9 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0045 .26 - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect 39     760   350     timeout 0 wit inspect 92    1900 false(unreach-call) 1 wit inspect 6.7   300   unknown 0 wit inspect 2.9  180 true -32 wit inspect .60   19    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     6300   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.9
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     7400   8100     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .037 4.9
reducercommutativity/avg20_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1800   9600     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .020 4.9
reducercommutativity/avg40_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1800   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .023 4.9
reducercommutativity/avg60_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1700   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .039 4.8
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     2900   9900     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .048 5.0
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 910     8000   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 45 error (2) 0 wit inspect .018 4.8
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     2000   14000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .018 4.9
reducercommutativity/max20_true-unreach-call.i unreach-call timeout 0 wit inspect 900     2300   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .027 4.9
reducercommutativity/max40_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1900   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/max60_true-unreach-call.i unreach-call timeout 0 wit inspect 900     2100   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .044 4.8
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     3200   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .021 4.8
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     1600   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .047 4.8
reducercommutativity/sep10_true-unreach-call.i unreach-call timeout 0 wit inspect 900     2000   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .047 4.9
reducercommutativity/sep20_true-unreach-call.i unreach-call timeout 0 wit inspect 900     2600   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 4.9
reducercommutativity/sep40_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1800   14000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .033 4.9
reducercommutativity/sep60_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1900   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .039 4.8
reducercommutativity/sep_true-unreach-call_true-termination.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 .68 44 error (2) 0 wit inspect .046 4.8
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     6000   6600     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .022 4.8
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     5100   6800     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8
reducercommutativity/sum20_true-unreach-call.i unreach-call timeout 0 wit inspect 900     4700   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 4.9
reducercommutativity/sum40_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1700   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .050 4.9
reducercommutativity/sum60_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1700   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .044 4.9
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     4700   6400     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .017 5.0
array-tiling/mlceu_false-unreach-call.i unreach-call timeout 0 wit inspect 900     1100   12000     error (invalid witness file) 0 wit inspect .39 41 error (2) 0 wit inspect .040 4.9 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0013 .31 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect 7.5   370   62     timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 6.8   270   unknown 0 wit inspect 2.7  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i unreach-call error (7) 0 wit inspect 23     360   240     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 5.0
array-tiling/mbpr3_true-unreach-call.i unreach-call error (7) 0 wit inspect 29     560   280     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 45 error (2) 0 wit inspect .049 4.9
array-tiling/mbpr4_true-unreach-call.i unreach-call timeout 0 wit inspect 900     830   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .024 4.9
array-tiling/mbpr5_true-unreach-call.i unreach-call error (7) 0 wit inspect 26     550   220     - wit