Tool ULTIMATE Kojak 0.1.23-3204b741 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution [2017-12-02 02:33:02 CET; 2017-12-03 04:40:15 CET; 2017-12-03 06:11:17 CET; 2017-12-03 11:17:40 CET; 2017-12-03 12:06:01 CET] [2017-12-03 03:22:18 CET; 2017-12-03 05:43:12 CET; 2017-12-03 06:29:55 CET; 2017-12-03 11:52:51 CET; 2017-12-03 12:06:37 CET] [2017-12-03 03:55:21 CET; 2017-12-03 06:07:12 CET; 2017-12-03 12:03:01 CET; 2017-12-03 12:07:27 CET] 2017-12-03 04:22:06 CET [2017-12-03 04:36:43 CET; 2017-12-03 06:08:25 CET; 2017-12-03 12:03:17 CET] 2017-12-03 00:36:56 CET [2017-12-03 03:32:10 CET; 2017-12-03 05:47:35 CET; 2017-12-03 11:54:19 CET]
Run set ukojak.[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-ukojak.[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-ukojak.[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-ukojak.[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-ukojak.[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-ukojak.[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-ukojak.[sv-comp18-correctness-witness.ReachSafety-Arrays; sv-comp18-correctness-witness.ReachSafety-BitVectors; sv-comp18-correctness-witness.ReachSafety-ControlFlow; sv-comp18-correctness-witness.ReachSafety-ECA; sv-comp18-correctness-witness.ReachSafety-Floats; sv-comp18-correctness-witness.ReachSafety-Heap; sv-comp18-correctness-witness.ReachSafety-Loops; sv-comp18-correctness-witness.ReachSafety-ProductLines; sv-comp18-correctness-witness.ReachSafety-Recursive; sv-comp18-correctness-witness.ReachSafety-Sequentialized; sv-comp18-correctness-witness.MemSafety-Arrays; sv-comp18-correctness-witness.MemSafety-Heap; sv-comp18-correctness-witness.MemSafety-LinkedLists; sv-comp18-correctness-witness.MemSafety-Other; sv-comp18-correctness-witness.NoOverflows-BitVectors; sv-comp18-correctness-witness.NoOverflows-Other; sv-comp18-correctness-witness.Systems_BusyBox_MemSafety; sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows; sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety]
Options --full-output [-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-03_0440.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/ukojak.2017-12-03_0611.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/ukojak.2017-12-03_1117.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/ukojak.2017-12-03_1206.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/ukojak.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/ukojak.2017-12-03_1206.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/ukojak.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true [--full-output --validate ../../results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/ukojak.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml]
/localhome/dbeyer/comp/sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5100   11000     error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .74 49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call timeout 0 wit inspect 900     4900   10000     error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .038 5.0 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0021 .28 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4900   14000     error (invalid witness file) 0 wit inspect .53 44 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 .0017 .27 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call timeout 0 wit inspect 900     5100   14000     error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .027 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0041 .31 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5000   14000     error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0018 .27 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5300   12000     error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .94 47 error (invalid witness file) 0 wit inspect .0015 .34 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4900   14000     error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4900   12000     error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .95 49 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   11000     error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   12000     error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0014 .32 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5500   11000     error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0040 .30 - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4900   11000     error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect 1.1  51 error (invalid witness file) 0 wit inspect .0016 .32 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   13000     error (invalid witness file) 0 wit inspect .53 41 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 .0013 .27 - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   11000     error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4900   11000     error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   14000     error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   11000     error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .73 49 error (invalid witness file) 0 wit inspect .0019 .28 - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   12000     error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .79 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   12000     error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect 1.2  49 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   12000     error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect 1.1  48 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   11000     error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .91 47 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   11000     error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .035 4.9 error (invalid witness file) 0 wit inspect .90 48 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   12000     error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   12000     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.1  50 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   11000     error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .98 47 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   11000     error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4900   9300     error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .027 4.8 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i unreach-call timeout 0 wit inspect 900     4800   12000     error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call timeout 0 wit inspect 900     5200   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .018 5.0
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4900   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 4.9
array-examples/relax_true-unreach-call.i unreach-call timeout 0 wit inspect 900     590   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .017 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4900   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .020 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5300   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .020 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 5.8   330   48     - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  510 true 2 wit inspect 7.9   280  
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 5.0
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call true 2 wit inspect 4.3   250   35     - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 4.9   230  
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5200   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .020 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5100   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 5.0
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4900   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 5.0
array-examples/standard_compare_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4900   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .018 5.0
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .020 4.9
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.8
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4900   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .022 5.0
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 47 error (2) 0 wit inspect .018 5.0
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.8
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .017 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 47 error (2) 0 wit inspect .018 4.8
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5000   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .017 4.8
array-examples/standard_find_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5000   12000     - 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-examples/standard_init1_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .023 5.0
array-examples/standard_init2_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .022 4.8
array-examples/standard_init3_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5200   12000     - 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_init4_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5200   14000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_init5_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .019 4.8
array-examples/standard_init6_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .024 4.8
array-examples/standard_init7_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_init8_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 5.0
array-examples/standard_init9_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 5.0
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .023 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   14000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 46 error (2) 0 wit inspect .019 4.9
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     5200   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .80 45 error (2) 0 wit inspect .018 4.9
array-examples/standard_partition_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 48 error (2) 0 wit inspect .019 5.0
array-examples/standard_password_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   9400     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 45 error (2) 0 wit inspect .020 4.9
array-examples/standard_running_true-unreach-call.i unreach-call timeout 0 wit inspect 900     4800   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .020 4.9
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 5.5   310   42     - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    990 true 2 wit inspect 5.3   260  
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     6900   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call timeout 0 wit inspect 900     4800   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .031 4.8
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4700   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_01_true-unreach-call.i unreach-call timeout 0 wit inspect 900     4800   14000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .022 5.0
array-examples/standard_two_index_02_true-unreach-call.i unreach-call timeout 0 wit inspect 900     4800   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_two_index_03_true-unreach-call.i unreach-call timeout 0 wit inspect 900     5000   14000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .020 4.9
array-examples/standard_two_index_04_true-unreach-call.i unreach-call timeout 0 wit inspect 900     4800   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_05_true-unreach-call.i unreach-call timeout 0 wit inspect 900     4800   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_06_true-unreach-call.i unreach-call timeout 0 wit inspect 900     4800   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_two_index_07_true-unreach-call.i unreach-call timeout 0 wit inspect 900     4800   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .021 4.8
array-examples/standard_two_index_08_true-unreach-call.i unreach-call timeout 0 wit inspect 900     5000   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 5.0
array-examples/standard_two_index_09_true-unreach-call.i unreach-call timeout 0 wit inspect 900     4800   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .019 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call timeout 0 wit inspect 900     3000   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call timeout 0 wit inspect 900     4800   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 4.8
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     4900   10000     error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .99 47 error (invalid witness file) 0 wit inspect .0018 .28 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call timeout 0 wit inspect 900     5200   7300     error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     4900   12000     error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call timeout 0 wit inspect 900     5200   7100     error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     5900   9900     error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call timeout 0 wit inspect 900     4900   11000     error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0023 .26 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     4900   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     5200   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call timeout 0 wit inspect 900     5200   7500     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .018 5.0
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900     6000   8800     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900     4900   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 5.0
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call timeout 0 wit inspect 900     6000   8500     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900     6400   7600     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 5.0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900     6400   8600     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 46 error (2) 0 wit inspect .021 5.0
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900     6200   6500     - 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-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call timeout 0 wit inspect 900     6000   8700     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     2700   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 5.0
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect 9.9   480   84     true -32 wit inspect 4.4  260 false(unreach-call) 1 wit inspect 8.8   330   unknown 0 wit inspect 3.9  210 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect 18     700   170     true -32 wit inspect 4.9  270 false(unreach-call) 1 wit inspect 47     3500   unknown 0 wit inspect 3.4  190 false(unreach-call) 1 wit inspect .79   19    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect 39     1000   390     true -32 wit inspect 5.9  270 out of memory 0 wit inspect 41     7000   unknown 0 wit inspect 4.6  220 false(unreach-call) 1 wit inspect .63   20    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i unreach-call timeout 0 wit inspect 900     1900   10000     error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i unreach-call timeout 0 wit inspect 900     3300   8700     error (invalid witness file) 0 wit inspect .53 41 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 .0041 .29 - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call false(unreach-call) 1 wit inspect 17     680   190     timeout 0 wit inspect 92    1900 false(unreach-call) 1 wit inspect 7.5   310   unknown 0 wit inspect 2.2  210 true -32 wit inspect .78   19    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     710   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 45 error (2) 0 wit inspect .020 5.0
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     960   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .022 4.8
reducercommutativity/avg20_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1500   10000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .017 4.9
reducercommutativity/avg40_true-unreach-call.i unreach-call error (7) 0 wit inspect 310     4300   3700     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .020 4.9
reducercommutativity/avg60_true-unreach-call.i unreach-call error (7) 0 wit inspect 800     5000   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .017 4.8
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     510   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     11000   11000     - 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
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     13000   12000     - 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
reducercommutativity/max20_true-unreach-call.i unreach-call timeout 0 wit inspect 900     6200   15000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.8
reducercommutativity/max40_true-unreach-call.i unreach-call timeout 0 wit inspect 900     7400   9400     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.8
reducercommutativity/max60_true-unreach-call.i unreach-call timeout 0 wit inspect 900     6800   7600     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     2900   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     4600   7300     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 4.9
reducercommutativity/sep10_true-unreach-call.i unreach-call timeout 0 wit inspect 900     6100   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.8
reducercommutativity/sep20_true-unreach-call.i unreach-call timeout 0 wit inspect 910     13000   8400     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .018 4.9
reducercommutativity/sep40_true-unreach-call.i unreach-call timeout 0 wit inspect 910     13000   8400     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 44 error (2) 0 wit inspect .018 4.8
reducercommutativity/sep60_true-unreach-call.i unreach-call timeout 0 wit inspect 900     13000   8100     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .019 5.0
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     1800   13000     - 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
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 40     2600   370     - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    980 true 2 wit inspect 340     3100  
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call true 2 wit inspect 230     4500   2700     - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     4800  
reducercommutativity/sum20_true-unreach-call.i unreach-call timeout 0 wit inspect 900     5300   6400     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .019 5.0
reducercommutativity/sum40_true-unreach-call.i unreach-call timeout 0 wit inspect 900     5200   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.9
reducercommutativity/sum60_true-unreach-call.i unreach-call timeout 0 wit inspect 900     5600   8400     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .020 4.9
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call timeout 0 wit inspect 900     2000   13000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 47 error (2) 0 wit inspect .020 4.9
array-tiling/mlceu_false-unreach-call.i unreach-call timeout 0 wit inspect 900     3100   11000     error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i unreach-call false(unreach-call) 1 wit inspect 5.2   290   43     timeout 0 wit inspect 92    1900 false(unreach-call) 1 wit inspect 15     300   unknown 0 wit inspect 3.2  210 true -32 wit inspect .75   18    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i unreach-call timeout 0 wit inspect 900     880   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .020 4.8
array-tiling/mbpr3_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1100   12000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 5.0
array-tiling/mbpr4_true-unreach-call.i unreach-call timeout 0 wit inspect 900     920   11000     - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .021 4.9
array-tiling/mbpr5_true-unreach-call.i unreach-call timeout 0 wit inspect 900     1100   12000     - wit inspect - wit