Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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-01 12:59:33 CET; 2017-12-02 11:31:00 CET; 2017-12-02 13:45:39 CET; 2017-12-02 18:23:42 CET; 2017-12-02 20:38:57 CET] [2017-12-02 09:20:19 CET; 2017-12-02 13:19:03 CET; 2017-12-02 18:18:09 CET; 2017-12-02 20:05:51 CET; 2017-12-03 03:39:33 CET] [2017-12-02 10:53:45 CET; 2017-12-02 13:40:51 CET; 2017-12-02 20:31:31 CET; 2017-12-03 03:40:31 CET] 2017-12-02 11:06:16 CET [2017-12-02 11:21:21 CET; 2017-12-02 13:42:37 CET; 2017-12-02 20:34:26 CET] 2017-12-02 06:57:43 CET [2017-12-02 09:56:59 CET; 2017-12-02 13:21:13 CET; 2017-12-02 20:11:47 CET]
Run set esbmc-kind.[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-esbmc-kind.[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-esbmc-kind.[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-esbmc-kind.[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-esbmc-kind.[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-esbmc-kind.[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-esbmc-kind.[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 -s kinduction [-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-02_1131.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/esbmc-kind.2017-12-02_1345.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const; -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-02_1823.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/esbmc-kind.2017-12-02_2038.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/esbmc-kind.2017-12-02_1131.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/esbmc-kind.2017-12-02_1823.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/esbmc-kind.2017-12-02_2038.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/esbmc-kind.2017-12-02_1131.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/esbmc-kind.2017-12-02_1823.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true [--full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/esbmc-kind.2017-12-02_1131.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/esbmc-kind.2017-12-02_1823.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 0 900     3900 8500    0 .55 43 0 .020 5.0 0 .65 49 0 .0011 .26 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call 0 900     2800 12000    0 .43 41 0 .019 5.0 0 .84 50 0 .0012 .29 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call 0 900     2800 12000    0 .55 43 0 .019 5.0 0 .66 49 0 .0016 .26 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call 0 900     7500 12000    0 .58 44 0 .018 4.8 0 .81 49 0 .0012 .26 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call 0 900     7300 10000    0 .40 43 0 .020 4.9 0 .69 50 0 .0013 .29 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call 0 900     3000 6800    0 .56 43 0 .018 4.9 0 .65 49 0 .0030 .34 - -
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call 0 900     9500 12000    0 .39 41 0 .018 5.0 0 .87 50 0 .0022 .28 - -
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call 0 900     9300 10000    0 .41 41 0 .019 4.9 0 .84 49 0 .0013 .26 - -
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call 0 900     9300 8400    0 .60 43 0 .020 4.9 0 .69 49 0 .0030 .26 - -
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call 0 900     9500 12000    0 .58 43 0 .019 4.8 0 .84 49 0 .0011 .29 - -
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call 0 900     9300 11000    0 .42 44 0 .018 4.9 0 .68 49 0 .0015 .27 - -
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call 0 900     9400 9700    0 .57 43 0 .023 4.9 0 .67 50 0 .0036 .26 - -
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call 0 900     9600 9400    0 .67 44 0 .021 4.9 0 .67 50 0 .0029 .26 - -
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call 0 900     9600 11000    0 .55 43 0 .018 4.8 0 .66 49 0 .0010 .34 - -
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call 0 900     9300 9800    0 .55 42 0 .021 4.9 0 .67 50 0 .0013 .27 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call 0 900     6100 11000    0 .42 43 0 .019 4.8 0 .65 49 0 .0011 .26 - -
array-examples/standard_init1_false-unreach-call_ground.i unreach-call 0 900     5800 10000    0 .56 43 0 .019 4.9 0 .65 49 0 .0037 .26 - -
array-examples/standard_init2_false-unreach-call_ground.i unreach-call 0 900     6000 10000    0 .60 44 0 .020 4.9 0 .83 49 0 .0011 .26 - -
array-examples/standard_init3_false-unreach-call_ground.i unreach-call 0 900     5900 10000    0 .58 44 0 .019 4.9 0 .66 49 0 .0015 .29 - -
array-examples/standard_init4_false-unreach-call_ground.i unreach-call 0 900     6000 10000    0 .41 41 0 .019 4.8 0 .84 49 0 .0022 .26 - -
array-examples/standard_init5_false-unreach-call_ground.i unreach-call 0 900     6100 9600    0 .39 43 0 .019 4.8 0 .66 49 0 .0011 .26 - -
array-examples/standard_init6_false-unreach-call_ground.i unreach-call 0 900     6100 9900    0 .55 43 0 .020 4.9 0 .88 50 0 .0035 .28 - -
array-examples/standard_init7_false-unreach-call_ground.i unreach-call 0 900     6100 10000    0 .56 43 0 .018 5.0 0 .67 49 0 .0011 .30 - -
array-examples/standard_init8_false-unreach-call_ground.i unreach-call 0 900     6100 12000    0 .71 43 0 .020 4.9 0 .68 49 0 .0026 .26 - -
array-examples/standard_init9_false-unreach-call_ground.i unreach-call 0 900     6100 9700    0 .69 43 0 .018 4.9 0 .67 49 0 .0011 .26 - -
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call 0 900     7100 9800    0 .41 41 0 .021 4.8 0 .66 49 0 .0011 .26 - -
array-examples/standard_partition_false-unreach-call_ground.i unreach-call 0 900     4300 11000    0 .41 41 0 .018 4.9 0 .66 49 0 .0032 .26 - -
array-examples/standard_running_false-unreach-call.i unreach-call 0 430     15000 5600    0 .61 43 0 .019 4.9 0 .66 49 0 .0011 .30 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call 0 900     9100 10000    - - - - 0 .57 43 0 .019 4.9
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call 0 900     3600 11000    - - - - 0 .69 44 0 .018 4.9
array-examples/relax_true-unreach-call.i unreach-call 0 900     360 13000    - - - - 0 .71 43 0 .019 4.9
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call 0 900     10000 10000    - - - - 0 .57 44 0 .019 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call 0 900     520 10000    - - - - 0 .68 42 0 .025 5.0
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call 2 .10  26 .80 - - - - 2 7.9  380 2 8.0   270  
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call 0 900     7000 9800    - - - - 0 .52 41 0 .018 4.9
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call 2 .10  26 .87 - - - - 2 3.6  260 2 4.4   230  
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call 0 900     2800 10000    - - - - 0 .58 44 0 .019 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call 0 900     7300 8600    - - - - 0 .75 43 0 .026 4.8
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call 0 900     5700 9500    - - - - 0 .69 41 0 .018 4.9
array-examples/standard_compare_true-unreach-call_ground.i unreach-call 0 900     7500 10000    - - - - 0 .63 43 0 .018 4.8
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call 0 900     10000 11000    - - - - 0 .59 42 0 .021 4.9
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call 0 900     10000 9100    - - - - 0 .67 41 0 .022 5.0
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call 0 900     10000 11000    - - - - 0 .67 41 0 .025 4.8
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call 0 900     10000 10000    - - - - 0 .58 44 0 .022 4.8
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call 0 900     10000 11000    - - - - 0 .53 41 0 .025 4.9
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call 0 900     10000 9800    - - - - 0 .55 43 0 .017 4.8
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call 0 900     10000 9700    - - - - 0 .68 43 0 .020 4.9
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call 0 900     10000 11000    - - - - 0 .70 43 0 .018 4.8
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call 0 900     10000 11000    - - - - 0 .73 41 0 .017 4.8
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call 0 900     6100 10000    - - - - 0 .67 44 0 .019 4.9
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call 0 900     6000 10000    - - - - 0 .56 41 0 .025 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call 0 900     6000 10000    - - - - 0 .66 43 0 .023 4.8
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call 0 900     5900 9800    - - - - 0 .51 41 0 .020 4.9
array-examples/standard_find_true-unreach-call_ground.i unreach-call 0 900     10000 9600    - - - - 0 .66 42 0 .023 4.9
array-examples/standard_init1_true-unreach-call_ground.i unreach-call 0 900     5900 11000    - - - - 0 .53 44 0 .023 5.0
array-examples/standard_init2_true-unreach-call_ground.i unreach-call 0 900     5900 9900    - - - - 0 .68 43 0 .019 4.9
array-examples/standard_init3_true-unreach-call_ground.i unreach-call 0 900     5900 9300    - - - - 0 .60 43 0 .019 4.9
array-examples/standard_init4_true-unreach-call_ground.i unreach-call 0 900     5900 11000    - - - - 0 .61 43 0 .018 4.9
array-examples/standard_init5_true-unreach-call_ground.i unreach-call 0 900     6000 9700    - - - - 0 .60 43 0 .022 4.9
array-examples/standard_init6_true-unreach-call_ground.i unreach-call 0 900     6000 10000    - - - - 0 .68 42 0 .018 4.8
array-examples/standard_init7_true-unreach-call_ground.i unreach-call 0 900     6000 11000    - - - - 0 .54 44 0 .025 4.8
array-examples/standard_init8_true-unreach-call_ground.i unreach-call 0 900     6000 13000    - - - - 0 .41 44 0 .024 4.8
array-examples/standard_init9_true-unreach-call_ground.i unreach-call 0 900     6000 11000    - - - - 0 .53 41 0 .021 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call 0 900     7100 9800    - - - - 0 .54 41 0 .022 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call 0 900     7200 9700    - - - - 0 .56 45 0 .020 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call 0 900     10000 11000    - - - - 0 .54 44 0 .023 4.8
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call 0 900     4200 11000    - - - - 0 .57 42 0 .021 4.9
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call 0 470     15000 5200    - - - - 0 .71 43 0 .020 5.0
array-examples/standard_partition_true-unreach-call_ground.i unreach-call 0 900     4300 12000    - - - - 0 .54 42 0 .018 5.0
array-examples/standard_password_true-unreach-call_ground.i unreach-call 0 900     7500 9500    - - - - 0 .52 41 0 .024 5.0
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call 0 900     8600 11000    - - - - 0 .63 41 0 .026 4.8
array-examples/standard_running_true-unreach-call.i unreach-call 0 430     15000 6200    - - - - 0 .52 41 0 .018 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call 0 900     300 11000    - - - - 0 .73 43 0 .018 4.9
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call 0 900     6200 12000    - - - - 0 .66 41 0 .018 4.8
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call 0 900     7300 11000    - - - - 0 .69 41 0 .025 4.8
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call 0 900     10000 11000    - - - - 0 .71 44 0 .023 4.8
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call 0 900     10000 12000    - - - - 0 .62 43 0 .039 4.8
array-examples/standard_two_index_01_true-unreach-call.i unreach-call 0 900     10000 9600    - - - - 0 .51 41 0 .022 4.9
array-examples/standard_two_index_02_true-unreach-call.i unreach-call 0 900     10000 12000    - - - - 0 .51 44 0 .024 4.8
array-examples/standard_two_index_03_true-unreach-call.i unreach-call 0 900     10000 10000    - - - - 0 .55 41 0 .020 4.8
array-examples/standard_two_index_04_true-unreach-call.i unreach-call 0 900     10000 9700    - - - - 0 .60 41 0 .020 4.9
array-examples/standard_two_index_05_true-unreach-call.i unreach-call 0 900     10000 12000    - - - - 0 .48 43 0 .024 4.8
array-examples/standard_two_index_06_true-unreach-call.i unreach-call 0 900     10000 10000    - - - - 0 .53 43 0 .024 4.8
array-examples/standard_two_index_07_true-unreach-call.i unreach-call 0 900     10000 11000    - - - - 0 .68 44 0 .020 4.8
array-examples/standard_two_index_08_true-unreach-call.i unreach-call 0 900     9900 11000    - - - - 0 .66 44 0 .019 4.9
array-examples/standard_two_index_09_true-unreach-call.i unreach-call 0 900     10000 10000    - - - - 0 .53 43 0 .017 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call 0 900     830 11000    - - - - 0 .55 41 0 .018 5.0
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call 0 900     4500 9700    - - - - 0 .56 41 0 .024 4.8
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call 0 900     6400 9600    0 .55 44 0 .018 4.9 0 .64 49 0 .0012 .29 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call 0 900     5200 10000    0 .56 45 0 .019 4.9 0 .67 49 0 .0032 .28 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call 0 900     5000 13000    0 .73 43 0 .019 4.9 0 .86 49 0 .0026 .34 - -
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call 0 900     4600 10000    0 .71 43 0 .019 4.8 0 .82 49 0 .0011 .27 - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call 0 900     5000 11000    0 .74 44 0 .018 5.0 0 .86 49 0 .0011 .30 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call 0 900     3500 7600    0 .41 43 0 .047 4.8 0 .86 49 0 .0011 .28 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call 0 900     4200 10000    - - - - 0 .56 41 0 .018 4.9
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call 0 900     4100 8700    - - - - 0 .69 45 0 .020 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call 0 670     15000 4800    - - - - 0 .64 42 0 .023 5.0
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call 0 900     6400 9800    - - - - 0 .62 42 0 .019 4.8
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call 0 900     8400 13000    - - - - 0 .70 43 0 .023 4.9
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call 0 900     4900 9900    - - - - 0 .64 41 0 .019 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call 0 900     2400 9300    - - - - 0 .69 44 0 .019 4.8
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call 0 900     1600 11000    - - - - 0 .54 41 0 .024 4.8
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call 0 900     7300 9500    - - - - 0 .72 45 0 .020 4.8
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call 0 900     4400 9700    - - - - 0 .54 41 0 .019 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call 0 900     180 11000    - - - - 0 .57 41 0 .019 4.8
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call 1 1.8   55 22    1 4.1  350 -32 6.4   290   0 2.3  210 -32 .58   18    - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call 1 2.5   57 23    1 6.9  380 -32 6.3   290   0 2.4  210 -32 .59   19    - -
reducercommutativity/rangesum20_false-unreach-call.i unreach-call 1 4.5   55 49    1 9.6  440 -32 4.5   310   0 2.5  220 -32 .60   18    - -
reducercommutativity/rangesum40_false-unreach-call.i unreach-call 1 16     57 160    1 33    750 -32 7.2   370   0 3.4  220 -32 .62   19    - -
reducercommutativity/rangesum60_false-unreach-call.i unreach-call 0 180     170 2500    0 92    1300 -32 8.4   460   0 3.1  220 -32 .64   20    - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call 1 2.2   57 23    1 3.5  360 -32 4.2   270   0 2.2  210 -32 .58   19    - -
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call 2 43     75 480    - - - - 0 900    1400 0 960     5100  
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call 2 490     190 6000    - - - - 0 900    3500 0 960     6900  
reducercommutativity/avg20_true-unreach-call.i unreach-call 0 900     290 11000    - - - - 0 .65 41 0 .018 4.8
reducercommutativity/avg40_true-unreach-call.i unreach-call 0 900     380 13000    - - - - 0 .55 41 0 .018 4.9
reducercommutativity/avg60_true-unreach-call.i unreach-call 0 900     420 10000    - - - - 0 .68 43 0 .024 4.8
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call 0 900     140 13000    - - - - 0 .52 41 0 .024 4.8
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call 2 .70  28 9.1  - - - - 2 110    910 0 960     4300  
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call 2 17     42 200    - - - - 0 900    3600 0 960     3200  
reducercommutativity/max20_true-unreach-call.i unreach-call 0 900     140 10000    - - - - 0 .40 45 0 .020 4.8
reducercommutativity/max40_true-unreach-call.i unreach-call 0 900     190 13000    - - - - 0 .67 41 0 .021 5.0
reducercommutativity/max60_true-unreach-call.i unreach-call 0 900     250 12000    - - - - 0 .70 41 0 .021 4.9
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call 0 900     100 13000    - - - - 0 .70 41 0 .024 5.0
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call 2 .17  27 1.7  - - - - 0 900    1500 0 960     1900  
reducercommutativity/sep10_true-unreach-call.i unreach-call 2 .19  27 1.8  - - - - 0 900    1800 0 960     6400  
reducercommutativity/sep20_true-unreach-call.i unreach-call 2 .23  27 2.2  - - - - 0 900    4800 0 900     7000  
reducercommutativity/sep40_true-unreach-call.i unreach-call 2 .30  27 3.3  - - - - 0 900    1800 0 960     4600  
reducercommutativity/sep60_true-unreach-call.i unreach-call 2 .39  28 4.2  - - - - 0 900    3200 0 960     3400  
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call 0 900     130 10000    - - - - 0 .59 44 0 .020 4.8
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call 2 .14  27 1.8  - - - - 0 900    860 2 400     3200  
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call 2 .15  27 1.9  - - - - 0 900    2100 0 960     4800  
reducercommutativity/sum20_true-unreach-call.i unreach-call 2 .20  27 2.4  - - - - 0 900    4600 0 960     4600  
reducercommutativity/sum40_true-unreach-call.i unreach-call 2 .23  27 2.6  - - - - 0 900    2500 0 960     4600  
reducercommutativity/sum60_true-unreach-call.i unreach-call 2 .32  27 3.2  - - - - 0 900    3300 0 960     3000  
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call 0 900     130 11000    - - - - 0 .72 44 0 .022 4.8
array-tiling/mlceu_false-unreach-call.i unreach-call 0 900     180 13000    0 .67 43 0 .019 4.9 0 .66 49 0 .0013 .29 - -
array-tiling/skippedu_false-unreach-call.i unreach-call 1 .14  28 1.4  1 2.3  260 -32 5.9   280   0 2.0  180 -32 .57   18    - -
array-tiling/mbpr2_true-unreach-call.i unreach-call 0 900     180 13000    - - - - 0 .54 41 0 .023 4.9
array-tiling/mbpr3_true-unreach-call.i unreach-call 0 900     180 11000    - - - - 0 .53 41 0 .021 4.9
array-tiling/mbpr4_true-unreach-call.i unreach-call 0 900     210 10000    - - - - 0 .64 43