Tool 2LS 0.6.0 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution [2017-11-30 11:20:26 CET; 2017-12-01 08:19:20 CET; 2017-12-01 09:00:44 CET; 2017-12-01 10:20:37 CET; 2017-12-01 11:41:06 CET] [2017-12-01 07:32:03 CET; 2017-12-01 08:41:15 CET; 2017-12-01 10:18:17 CET; 2017-12-01 11:18:40 CET; 2017-12-01 17:31:39 CET] [2017-12-01 08:01:50 CET; 2017-12-01 08:58:15 CET; 2017-12-01 11:36:11 CET; 2017-12-01 17:38:09 CET] 2017-12-01 08:11:41 CET [2017-12-01 08:15:34 CET; 2017-12-01 08:59:36 CET; 2017-12-01 11:38:17 CET] 2017-12-01 04:23:32 CET [2017-12-01 07:36:49 CET; 2017-12-01 08:42:37 CET; 2017-12-01 11:21:10 CET]
Run set 2ls.[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-2ls.[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-2ls.[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-2ls.[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-2ls.[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-2ls.[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-2ls.[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 --graphml-witness witness.graphml [-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.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/2ls.2017-12-01_0819.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/2ls.2017-12-01_0900.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/2ls.2017-12-01_1020.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/2ls.2017-12-01_1141.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/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/2ls.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/2ls.2017-12-01_1020.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/2ls.2017-12-01_1141.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.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/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/2ls.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/2ls.2017-12-01_1020.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true [--full-output --validate ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/2ls.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/2ls.2017-12-01_1020.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 error (134) 0 wit inspect .093 22 .78 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0012  .30 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call out of memory 0 wit inspect 31     15000 440    error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0013  .33 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 490    error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0015  .30 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call out of memory 0 wit inspect 33     15000 470    error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0014  .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 470    error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0013  .27 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 290     15000 2000    error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .92 47 error (invalid witness file) 0 wit inspect .0015  .28 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 360    error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0015  .27 - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 400    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .96 49 error (invalid witness file) 0 wit inspect .0013  .26 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 430    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .91 49 error (invalid witness file) 0 wit inspect .0016  .26 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 460    error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0013  .30 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 390    error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0011  .35 - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 380    error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .91 49 error (invalid witness file) 0 wit inspect .0014  .30 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 420    error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  52 error (invalid witness file) 0 wit inspect .0013  .26 - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 390    error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0011  .33 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 490    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0011  .30 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 440    error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.2  51 error (invalid witness file) 0 wit inspect .0018  .29 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i unreach-call true -32 wit inspect 32     12000 400    timeout 0 wit inspect 92    1900 timeout 0 wit inspect 96     940   unknown 0 wit inspect .96 51 error (1) 0 wit inspect .068   9.0  - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 410    error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0015  .26 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 400    error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0015  .30 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 390    error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017  .30 - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 460    error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0015  .30 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 410    error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0012  .32 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 470    error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .96 49 error (invalid witness file) 0 wit inspect .0013  .29 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 470    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0013  .30 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 480    error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0013  .26 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 320     15000 2200    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0012  .35 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 380    error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0012  .30 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i unreach-call out of memory 0 wit inspect 31     15000 370    error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0011  .34 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call error (134) 0 wit inspect .11  22 .62 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .026 4.8
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call error (134) 0 wit inspect .078 22 .71 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.9
array-examples/relax_true-unreach-call.i unreach-call error (134) 0 wit inspect .18  26 1.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 180     15000 1400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 5.0
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 34     15000 390    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .022 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 17     5700 190    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  510 true 2 wit inspect 7.5   270  
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 270     15000 2100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 5.0
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call error (134) 0 wit inspect .074 22 .82 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 5.0
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 370    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .019 4.9
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 520    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .032 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 32     15000 450    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_compare_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 150     15000 1300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .035 4.9
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 440    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .024 4.8
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 34     15000 430    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .024 4.9
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 430    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 470    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .044 4.8
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 440    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 480    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 450    - 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_copy8_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 520    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .024 5.0
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 390    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 32     15000 500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .018 5.0
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 32     15000 420    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .023 4.9
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 32     15000 460    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .020 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 32     15000 390    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9
array-examples/standard_find_true-unreach-call_ground.i unreach-call true 2 wit inspect 40     15000 500    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 timeout 0 wit inspect 960     4700  
array-examples/standard_init1_true-unreach-call_ground.i unreach-call true 2 wit inspect 32     12000 390    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 timeout 0 wit inspect 960     2000  
array-examples/standard_init2_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 380    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .024 4.8
array-examples/standard_init3_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 410    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .023 4.9
array-examples/standard_init4_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 470    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .021 5.0
array-examples/standard_init5_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .050 4.9
array-examples/standard_init6_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .025 4.9
array-examples/standard_init7_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 490    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .020 5.0
array-examples/standard_init8_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 440    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_init9_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 450    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 260     15000 1900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .024 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 310     15000 2100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .024 4.9
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 34     15000 420    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 29     15000 370    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .018 5.0
array-examples/standard_partition_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 31     15000 400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_password_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 150     15000 1400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.9
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 510    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.9
array-examples/standard_running_true-unreach-call.i unreach-call out of memory 0 wit inspect 31     15000 510    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .048 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call out of memory 0 wit inspect 110     15000 880    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .048 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 34     15000 420    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call false(unreach-call) -16 wit inspect 75     11000 870    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2300 true 2 wit inspect 5.6   290  
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call out of memory 0 wit inspect 33     15000 410    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 33     15000 420    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_two_index_01_true-unreach-call.i unreach-call out of memory 0 wit inspect 250     15000 1600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_two_index_02_true-unreach-call.i unreach-call out of memory 0 wit inspect 34     15000 440    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .019 4.8
array-examples/standard_two_index_03_true-unreach-call.i unreach-call out of memory 0 wit inspect 240     15000 1800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .035 4.8
array-examples/standard_two_index_04_true-unreach-call.i unreach-call out of memory 0 wit inspect 33     15000 480    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_05_true-unreach-call.i unreach-call out of memory 0 wit inspect 34     15000 430    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .023 5.0
array-examples/standard_two_index_06_true-unreach-call.i unreach-call out of memory 0 wit inspect 240     15000 1700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .021 4.9
array-examples/standard_two_index_07_true-unreach-call.i unreach-call out of memory 0 wit inspect 34     15000 420    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .024 4.8
array-examples/standard_two_index_08_true-unreach-call.i unreach-call out of memory 0 wit inspect 34     15000 420    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 5.0
array-examples/standard_two_index_09_true-unreach-call.i unreach-call out of memory 0 wit inspect 34     15000 430    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .048 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call out of memory 0 wit inspect 170     15000 1200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 46 error (2) 0 wit inspect .020 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 32     15000 400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call out of memory 0 wit inspect 32     15000 380    error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .83 48 error (invalid witness file) 0 wit inspect .0016  .26 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call out of memory 0 wit inspect 34     15000 500    error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0011  .35 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call out of memory 0 wit inspect 26     15000 330    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0016  .26 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call true -32 wit inspect 38     15000 460    timeout 0 wit inspect 92    2500 timeout 0 wit inspect 97     4800   unknown 0 wit inspect .95 51 error (1) 0 wit inspect .066   9.0  - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call out of memory 0 wit inspect 26     15000 340    error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .93 51 error (invalid witness file) 0 wit inspect .0013  .26 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call error (134) 0 wit inspect .079 23 .65 error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016  .28 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call out of memory 0 wit inspect 29     15000 370    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 5.0
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call out of memory 0 wit inspect 30     15000 370    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 46 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call true 2 wit inspect 36     13000 390    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 timeout 0 wit inspect 960     4900  
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call error (5) 0 wit inspect 110     7000 820    - 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
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call error (134) 0 wit inspect .16  24 1.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call error (5) 0 wit inspect 100     7000 830    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .024 4.9
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call out of memory 0 wit inspect 34     15000 440    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 5.0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call out of memory 0 wit inspect 26     15000 320    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 45 error (2) 0 wit inspect .020 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call error (5) 0 wit inspect 130     11000 1200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .024 4.9
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call true 2 wit inspect 29     12000 360    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 timeout 0 wit inspect 960     5900  
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     14000 3700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .019 4.8
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call error (134) 0 wit inspect .089 22 .64 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0014  .31 - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call error (134) 0 wit inspect .11  22 .64 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .99 49 error (invalid witness file) 0 wit inspect .0030  .26 - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i unreach-call error (134) 0 wit inspect .092 22 .76 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0015  .27 - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i unreach-call error (134) 0 wit inspect .094 22 .82 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0013  .27 - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i unreach-call error (134) 0 wit inspect .11  23 .63 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .81 48 error (invalid witness file) 0 wit inspect .0014  .28 - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call error (134) 0 wit inspect .097 22 .63 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0017  .27 - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 110     360 1300    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 860    7000 timeout 0 wit inspect 960     4600  
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     710 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .019 4.8
reducercommutativity/avg20_true-unreach-call.i unreach-call timeout 0 wit inspect 900     810 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .021 5.0
reducercommutativity/avg40_true-unreach-call.i unreach-call timeout 0 wit inspect 900     890 7700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/avg60_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1000 8800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     1600 7200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 46 error (2) 0 wit inspect .020 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 6.0   89 85    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     4100  
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 300     480 3800    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     3400  
reducercommutativity/max20_true-unreach-call.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 .54 41 error (2) 0 wit inspect .019 4.9
reducercommutativity/max40_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1400 9000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .031 4.8
reducercommutativity/max60_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1900 5600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.9
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     2500 3700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .019 4.9
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 2.1   69 24    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 timeout 0 wit inspect 960     1700  
reducercommutativity/sep10_true-unreach-call.i unreach-call true 2 wit inspect 3.3   100 41    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 920     7000  
reducercommutativity/sep20_true-unreach-call.i unreach-call true 2 wit inspect 12     280 120    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3000 timeout 0 wit inspect 910     7000  
reducercommutativity/sep40_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1400 9300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 5.0
reducercommutativity/sep60_true-unreach-call.i unreach-call timeout 0 wit inspect 900     2200 9400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     10000 7000    - 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
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 20     170 270    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 380     3200  
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     760 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .020 4.9
reducercommutativity/sum20_true-unreach-call.i unreach-call timeout 0 wit inspect 900     720 8100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9
reducercommutativity/sum40_true-unreach-call.i unreach-call timeout 0 wit inspect 900     860 8600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.8
reducercommutativity/sum60_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1000 6100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .020 5.0
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     1900 8000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.8
array-tiling/mlceu_false-unreach-call.i unreach-call out of memory 0 wit inspect 670     15000 3200    error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0012  .34 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect .33  38 3.4  false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 15     300   unknown 0 wit inspect 2.9  190 true -32 wit inspect .77    18    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i unreach-call out of memory 0 wit inspect 510     15000 2500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .021 4.8
array-tiling/mbpr3_true-unreach-call.i unreach-call out of memory 0 wit inspect 410     15000 2000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .022 4.8
array-tiling/mbpr4_true-unreach-call.i unreach-call out of memory 0 wit inspect 440     15000 2600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 5.0
array-tiling/mbpr5_true-unreach-call.i unreach-call timeout 0 wit inspect 900     12000 4400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 42 error (2) 0 wit inspect .019 4.8
array-tiling/nr2_true-unreach-call.i unreach-call out of memory 0 wit insp