Tool CBMC 5.8 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:34 CET; 2017-12-01 09:12:30 CET; 2017-12-01 11:16:27 CET; 2017-12-01 13:00:07 CET] [2017-12-01 07:26:01 CET; 2017-12-01 08:48:13 CET; 2017-12-01 10:50:55 CET; 2017-12-01 12:31:21 CET; 2017-12-01 19:39:59 CET] [2017-12-01 07:56:00 CET; 2017-12-01 09:05:59 CET; 2017-12-01 12:51:49 CET; 2017-12-01 19:43:03 CET] 2017-12-01 08:08:00 CET [2017-12-01 08:15:34 CET; 2017-12-01 09:09:10 CET; 2017-12-01 12:54:09 CET] 2017-12-01 04:22:29 CET [2017-12-01 07:31:28 CET; 2017-12-01 08:49:56 CET; 2017-12-01 12:35:01 CET]
Run set cbmc.[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-cbmc.[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-cbmc.[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-cbmc.[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-cbmc.[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-cbmc.[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-cbmc.[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/cbmc.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/cbmc.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/cbmc.2017-12-01_0912.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/cbmc.2017-12-01_1116.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/cbmc.2017-12-01_1300.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cbmc.2017-12-01_1116.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cbmc.2017-12-01_1300.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/cbmc.2017-12-01_1116.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true [--full-output --validate ../../results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cbmc.2017-12-01_1116.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 (6) 0 wit inspect 160    14000 1700   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .84 48 error (invalid witness file) 0 wit inspect .0013 .32 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call out of memory 0 wit inspect 23    15000 370   error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 23    15000 300   error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .90 47 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call error (134) 0 wit inspect 62    13000 780   error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call error (134) 0 wit inspect 77    13000 1000   error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .97 50 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call error (6) 0 wit inspect 420    10000 2500   error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect 1.1  51 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 100    15000 1300   error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 120    15000 1900   error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 130    15000 1800   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .91 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call error (134) 0 wit inspect 95    15000 1300   error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0013 .31 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 100    15000 1200   error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 110    15000 1500   error (invalid witness file) 0 wit inspect .53 45 error (2) 0 wit inspect .025 5.0 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 120    15000 1900   error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call error (134) 0 wit inspect 65    14000 970   error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .91 47 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call error (134) 0 wit inspect 70    15000 910   error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .95 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 72    15000 980   error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .86 51 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 100    15000 1500   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 61    15000 790   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 64    15000 840   error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .86 51 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 67    15000 1100   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .021 5.0 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/standard_init5_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 71    15000 1000   error (invalid witness file) 0 wit inspect .53 46 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .94 49 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 74    15000 980   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .92 51 error (invalid witness file) 0 wit inspect .0042 .26 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 52    15000 790   error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .88 51 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 54    15000 660   error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .026 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i unreach-call out of memory 0 wit inspect 56    15000 680   error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .90 47 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call error (42) 0 wit inspect 870    1400 3800   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.1  47 error (invalid witness file) 0 wit inspect .0012 .31 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i unreach-call error (134) 0 wit inspect 65    14000 710   error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i unreach-call out of memory 0 wit inspect 88    15000 1300   error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call error (42) 0 wit inspect 870    1500 4900   - 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
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call error (134) 0 wit inspect 26    13000 420   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .021 4.9
array-examples/relax_true-unreach-call.i unreach-call error (6) 0 wit inspect 690    14000 3800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .023 4.9
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call error (42) 0 wit inspect 870    2600 4400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call error (134) 0 wit inspect 28    13000 400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .018 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call error (42) 0 wit inspect 870    4200 9100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 4.9
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call error (42) 0 wit inspect 870    1400 4100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 46 error (2) 0 wit inspect .018 4.9
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 93    15000 1200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .026 4.8
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 20    15000 250   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .020 4.9
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call error (134) 0 wit inspect 74    13000 820   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call error (6) 0 wit inspect 120    15000 1800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_compare_true-unreach-call_ground.i unreach-call error (42) 0 wit inspect 870    1500 3800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .052 4.9
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 68    15000 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .048 4.8
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 81    15000 1000   - 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_copy3_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 92    15000 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .047 4.8
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 100    15000 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 46 error (2) 0 wit inspect .025 4.8
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call error (134) 0 wit inspect 82    15000 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 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 91    15000 1200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 5.0
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 99    15000 1200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call error (134) 0 wit inspect 82    15000 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .042 4.9
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call error (134) 0 wit inspect 62    14000 730   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .023 5.0
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 72    15000 900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .025 4.8
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 75    15000 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .025 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 72    15000 1000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .019 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 69    15000 900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .021 4.9
array-examples/standard_find_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 100    15000 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 45 error (2) 0 wit inspect .023 5.0
array-examples/standard_init1_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 100    15000 1400   - 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-examples/standard_init2_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 61    15000 860   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .050 5.0
array-examples/standard_init3_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 64    15000 880   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_init4_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 67    15000 910   - 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-examples/standard_init5_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 71    15000 1000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_init6_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 74    15000 990   - 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-examples/standard_init7_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 52    15000 700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .023 4.8
array-examples/standard_init8_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 54    15000 730   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.9
array-examples/standard_init9_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 56    15000 730   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .021 4.9
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call error (42) 0 wit inspect 870    1400 4900   - 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-examples/standard_minInArray_true-unreach-call_ground.i unreach-call error (42) 0 wit inspect 870    1400 3900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .021 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 100    15000 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .018 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call error (134) 0 wit inspect 90    13000 870   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .020 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call error (134) 0 wit inspect 74    14000 880   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.9
array-examples/standard_partition_true-unreach-call_ground.i unreach-call error (134) 0 wit inspect 66    14000 810   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 5.0
array-examples/standard_password_true-unreach-call_ground.i unreach-call error (42) 0 wit inspect 870    1500 3500   - 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_reverse_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 110    15000 1500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .026 4.8
array-examples/standard_running_true-unreach-call.i unreach-call out of memory 0 wit inspect 88    15000 1100   - 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-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call error (42) 0 wit inspect 870    3900 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 100    15000 1400   - 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-examples/standard_strcmp_true-unreach-call_ground.i unreach-call error (42) 0 wit inspect 870    3500 5500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 46 error (2) 0 wit inspect .018 4.8
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call out of memory 0 wit inspect 73    15000 940   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .020 4.8
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call out of memory 0 wit inspect 73    15000 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_01_true-unreach-call.i unreach-call out of memory 0 wit inspect 96    15000 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.9
array-examples/standard_two_index_02_true-unreach-call.i unreach-call out of memory 0 wit inspect 68    15000 890   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_03_true-unreach-call.i unreach-call out of memory 0 wit inspect 96    15000 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_two_index_04_true-unreach-call.i unreach-call out of memory 0 wit inspect 68    15000 890   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .017 4.9
array-examples/standard_two_index_05_true-unreach-call.i unreach-call out of memory 0 wit inspect 68    15000 950   - 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-examples/standard_two_index_06_true-unreach-call.i unreach-call out of memory 0 wit inspect 96    15000 1400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .023 4.8
array-examples/standard_two_index_07_true-unreach-call.i unreach-call out of memory 0 wit inspect 68    15000 860   - 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-examples/standard_two_index_08_true-unreach-call.i unreach-call out of memory 0 wit inspect 68    15000 880   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.8
array-examples/standard_two_index_09_true-unreach-call.i unreach-call out of memory 0 wit inspect 68    15000 900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .020 4.9
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call error (42) 0 wit inspect 870    4500 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .022 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call error (6) 0 wit inspect 120    15000 1600   - 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
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call out of memory 0 wit inspect 60    15000 770   error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0015 .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 410    15000 3800   error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0014 .29 - 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 71    15000 930   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .032 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call out of memory 0 wit inspect 440    15000 6400   error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0014 .28 - 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 71    15000 960   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call error (134) 0 wit inspect 23    12000 300   error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call out of memory 0 wit inspect 100    15000 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call out of memory 0 wit inspect 120    15000 1500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call out of memory 0 wit inspect 250    15000 2500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .021 4.8
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call out of memory 0 wit inspect 280    15000 3900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 5.0
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call out of memory 0 wit inspect 150    15000 1800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .026 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call out of memory 0 wit inspect 290    15000 3300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call out of memory 0 wit inspect 560    15000 8100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .024 4.9
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call out of memory 0 wit inspect 130    15000 1700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .018 4.8
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call out of memory 0 wit inspect 430    15000 5200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call out of memory 0 wit inspect 200    15000 2500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call error (42) 0 wit inspect 870    5600 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .020 4.9
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect .67 34 6.4 unknown 0 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 11     340   unknown 0 wit inspect 4.5  220 error (2) 0 wit inspect .67   19    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect 1.1  34 9.8 unknown 0 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 51     4000   unknown 0 wit inspect 4.6  220 error (2) 0 wit inspect .86   19    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i unreach-call false(unreach-call) 0 wit inspect 2.0  35 26   unknown 0 wit inspect 4.3  270 out of memory 0 wit inspect 55     7000   unknown 0 wit inspect 4.7  230 error (2) 0 wit inspect .74   20    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i unreach-call false(unreach-call) 0 wit inspect 4.9  41 61   unknown 0 wit inspect 6.2  280 out of memory 0 wit inspect 84     7000   unknown 0 wit inspect 6.1  300 error (2) 0 wit inspect 1.1    22    - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i unreach-call false(unreach-call) 0 wit inspect 8.9  59 110   unknown 0 wit inspect 5.6  320 out of memory 0 wit inspect 62     7000   unknown 0 wit inspect 7.4  340 error (2) 0 wit inspect 1.2    23    - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect .96 58 12   true -32 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 11     360   unknown 0 wit inspect 3.8  220 true -32 wit inspect .65   19    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 35    51 500   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2300 timeout 0 wit inspect 960     5200  
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 530    180 6000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 timeout 0 wit inspect 960     6400  
reducercommutativity/avg20_true-unreach-call.i unreach-call error (42) 0 wit inspect 870    280 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.9
reducercommutativity/avg40_true-unreach-call.i unreach-call error (42) 0 wit inspect 870    300 11000   - 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
reducercommutativity/avg60_true-unreach-call.i unreach-call error (42) 0 wit inspect 870    350 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .024 5.0
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call error (42) 0 wit inspect 870    220 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .049 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 2.4  35 27   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 6.5  270 timeout 0 wit inspect 960     1500  
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 87    66 970   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 9.0  300 timeout 0 wit inspect 960     3200  
reducercommutativity/max20_true-unreach-call.i unreach-call error (42) 0 wit inspect 870    200 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9
reducercommutativity/max40_true-unreach-call.i unreach-call error (42) 0 wit inspect 870    230 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.9
reducercommutativity/max60_true-unreach-call.i unreach-call error (42) 0 wit inspect 870    260 9500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .023 4.9
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call error (42) 0 wit inspect 870    230 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .021 5.0
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect .93 35 8.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 430    1400 timeout 0 wit inspect 960     1800  
reducercommutativity/sep10_true-unreach-call.i unreach-call true 2 wit inspect 1.5  38 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 out of memory 0 wit inspect 850     7000  
reducercommutativity/sep20_true-unreach-call.i unreach-call true 2 wit inspect 4.8  48 59   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 timeout 0 wit inspect 960     6500  
reducercommutativity/sep40_true-unreach-call.i unreach-call true 2 wit inspect 35    87 490   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2400 timeout 0 wit inspect 960     4600  
reducercommutativity/sep60_true-unreach-call.i unreach-call true 2 wit inspect 150    160 2100   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5800 timeout 0 wit inspect 960     3500  
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call error (42) 0 wit inspect 880    9700 4300   - 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
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 4.7  39 56   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    990 true 2 wit inspect 350     3200  
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 180    130 2200   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     5100  
reducercommutativity/sum20_true-unreach-call.i unreach-call error (42) 0 wit inspect 870    270 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .018 5.0
reducercommutativity/sum40_true-unreach-call.i unreach-call error (42) 0 wit inspect 870    270 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.8
reducercommutativity/sum60_true-unreach-call.i unreach-call error (42) 0 wit inspect 870    270 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .020 5.0
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call error (42) 0 wit inspect 870    220 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 4.8
array-tiling/mlceu_false-unreach-call.i unreach-call error (42) 0 wit inspect 870    5800 8700   error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .91 48 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect .26 33 2.8 false(unreach-call) 1 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 7.9   260   unknown 0 wit inspect 3.0  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i unreach-call error (134) 0 wit inspect 81    13000 690   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.9
array-tiling/mbpr3_true-unreach-call.i unreach-call error (134) 0 wit inspect 230    13000 1400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .019 4.8
array-tiling/mbpr4_true-unreach-call.i unreach-call error (134) 0 wit inspect 210    13000 2000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.8
array-tiling/mbpr5_true-unreach-call.i unreach-call error (134) 0 wit inspect 150    14000 1400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .018 4.8
array-tiling/nr2_true-unreach-call.i unreach-call error (134) 0 wit inspect 60