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]
Date of execution [2017-12-01 08:49:27 CET; 2017-12-02 00:00:31 CET; 2017-12-02 01:45:33 CET; 2017-12-02 06:23:16 CET; 2017-12-02 08:45:19 CET] [2017-12-01 22:53:44 CET; 2017-12-02 01:15:07 CET; 2017-12-02 06:17:30 CET; 2017-12-02 08:10:39 CET; 2017-12-02 17:16:42 CET] [2017-12-01 23:38:04 CET; 2017-12-02 01:40:08 CET; 2017-12-02 08:34:53 CET; 2017-12-02 17:21:25 CET] 2017-12-01 23:47:42 CET [2017-12-01 23:55:24 CET; 2017-12-02 01:42:26 CET; 2017-12-02 08:39:22 CET] 2017-12-01 22:20:30 CET [2017-12-01 23:01:53 CET; 2017-12-02 01:17:53 CET; 2017-12-02 08:15:43 CET]
Run set esbmc-incr.[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-incr.[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-incr.[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-incr.[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-incr.[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-incr.[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-incr.[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 incr [-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-02_0000.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-incr.2017-12-02_0145.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-incr.2017-12-02_0623.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-incr.2017-12-02_0845.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/esbmc-incr.2017-12-02_0623.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/esbmc-incr.2017-12-02_0845.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/esbmc-incr.2017-12-02_0623.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true [--full-output --validate ../../results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/esbmc-incr.2017-12-02_0623.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     3800 8400    0 .61 41 0 .019 4.8 0 .67 49 0 .0013 .28 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call 0 900     2800 10000    0 .62 44 0 .020 4.9 0 .87 50 0 .0011 .26 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call 0 900     2800 10000    0 .69 44 0 .019 5.0 0 .87 49 0 .0011 .32 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call 0 900     7400 9800    0 .65 43 0 .023 4.9 0 .67 49 0 .0013 .26 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call 0 900     7400 12000    0 .54 43 0 .019 4.8 0 .86 49 0 .0012 .29 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call 0 900     3000 7000    0 .68 45 0 .019 4.8 0 .85 51 0 .0013 .30 - -
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call 0 900     9300 10000    0 .55 41 0 .019 4.8 0 .88 49 0 .0037 .26 - -
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call 0 900     9400 9300    0 .55 41 0 .037 4.8 0 .65 49 0 .0011 .26 - -
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call 0 900     9500 10000    0 .59 43 0 .019 4.8 0 .84 50 0 .0010 .27 - -
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call 0 900     9300 8800    0 .57 44 0 .018 4.8 0 .87 49 0 .0012 .30 - -
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call 0 900     9500 10000    0 .58 43 0 .018 4.9 0 .84 49 0 .0012 .26 - -
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call 0 900     9400 9900    0 .52 41 0 .019 5.0 0 .89 49 0 .0030 .29 - -
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call 0 900     9600 8700    0 .66 44 0 .019 4.9 0 .67 50 0 .0012 .26 - -
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call 0 900     9900 9700    0 .58 46 0 .020 4.9 0 .90 50 0 .0012 .27 - -
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call 0 900     9200 9500    0 .55 41 0 .019 4.8 0 .65 50 0 .0011 .26 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call 0 900     6200 12000    0 .55 44 0 .018 4.9 0 .68 50 0 .0011 .29 - -
array-examples/standard_init1_false-unreach-call_ground.i unreach-call 0 900     5900 9600    0 .59 44 0 .018 4.9 0 .88 49 0 .0011 .32 - -
array-examples/standard_init2_false-unreach-call_ground.i unreach-call 0 900     5900 10000    0 .56 41 0 .019 4.9 0 .90 50 0 .0012 .28 - -
array-examples/standard_init3_false-unreach-call_ground.i unreach-call 0 900     5900 10000    0 .65 42 0 .019 5.0 0 .86 50 0 .0011 .26 - -
array-examples/standard_init4_false-unreach-call_ground.i unreach-call 0 900     6000 9000    0 .61 44 0 .019 4.9 0 .71 49 0 .0012 .26 - -
array-examples/standard_init5_false-unreach-call_ground.i unreach-call 0 900     5900 9700    0 .57 43 0 .018 4.9 0 .84 49 0 .0011 .26 - -
array-examples/standard_init6_false-unreach-call_ground.i unreach-call 0 900     6100 11000    0 .51 41 0 .018 4.8 0 .67 49 0 .0012 .26 - -
array-examples/standard_init7_false-unreach-call_ground.i unreach-call 0 900     6000 11000    0 .54 41 0 .020 4.9 0 .64 50 0 .0013 .26 - -
array-examples/standard_init8_false-unreach-call_ground.i unreach-call 0 900     6100 9100    0 .59 42 0 .036 4.8 0 .87 49 0 .0012 .33 - -
array-examples/standard_init9_false-unreach-call_ground.i unreach-call 0 900     6000 11000    0 .58 43 0 .021 5.0 0 .87 49 0 .0011 .26 - -
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call 0 900     7100 11000    0 .53 44 0 .019 4.8 0 .90 49 0 .0011 .28 - -
array-examples/standard_partition_false-unreach-call_ground.i unreach-call 0 900     4200 10000    0 .61 43 0 .022 4.8 0 .67 50 0 .0013 .29 - -
array-examples/standard_running_false-unreach-call.i unreach-call 0 430     15000 5600    0 .53 43 0 .018 4.9 0 .87 49 0 .0011 .26 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call 0 900     9200 10000    - - - - 0 .54 43 0 .019 4.9
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call 0 900     3500 7700    - - - - 0 .52 43 0 .019 5.0
array-examples/relax_true-unreach-call.i unreach-call 0 900     350 10000    - - - - 0 .53 43 0 .021 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call 0 900     10000 12000    - - - - 0 .55 41 0 .018 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call 0 900     360 12000    - - - - 0 .70 44 0 .019 4.9
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call 0 900     1000 12000    - - - - 0 .41 43 0 .024 4.8
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call 0 900     7000 10000    - - - - 0 .70 43 0 .019 4.8
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call 0 900     9700 12000    - - - - 0 .68 44 0 .019 4.9
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call 0 900     2800 9900    - - - - 0 .68 43 0 .019 5.0
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call 0 900     7300 11000    - - - - 0 .60 44 0 .023 5.0
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call 0 900     5800 11000    - - - - 0 .62 43 0 .027 4.8
array-examples/standard_compare_true-unreach-call_ground.i unreach-call 0 900     7500 10000    - - - - 0 .67 42 0 .019 4.8
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call 0 900     10000 10000    - - - - 0 .63 43 0 .019 5.0
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call 0 900     10000 11000    - - - - 0 .67 43 0 .024 4.8
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call 0 900     10000 9900    - - - - 0 .58 42 0 .019 4.8
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call 0 900     10000 9900    - - - - 0 .67 44 0 .020 5.0
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call 0 900     10000 12000    - - - - 0 .69 44 0 .019 4.9
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call 0 900     10000 10000    - - - - 0 .70 42 0 .019 5.0
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call 0 900     10000 12000    - - - - 0 .75 44 0 .024 4.9
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call 0 900     10000 9800    - - - - 0 .68 43 0 .024 4.8
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call 0 900     10000 9900    - - - - 0 .70 44 0 .019 4.8
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call 0 900     6000 9700    - - - - 0 .75 44 0 .022 4.8
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call 0 900     6100 10000    - - - - 0 .74 41 0 .021 4.9
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call 0 900     6000 9600    - - - - 0 .69 41 0 .019 4.8
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call 0 900     6000 9500    - - - - 0 .70 41 0 .019 4.9
array-examples/standard_find_true-unreach-call_ground.i unreach-call 0 900     10000 9800    - - - - 0 .67 44 0 .025 5.0
array-examples/standard_init1_true-unreach-call_ground.i unreach-call 0 900     5800 11000    - - - - 0 .73 43 0 .023 5.0
array-examples/standard_init2_true-unreach-call_ground.i unreach-call 0 900     5900 9600    - - - - 0 .76 44 0 .022 4.8
array-examples/standard_init3_true-unreach-call_ground.i unreach-call 0 900     6000 12000    - - - - 0 .68 43 0 .020 5.0
array-examples/standard_init4_true-unreach-call_ground.i unreach-call 0 900     6000 10000    - - - - 0 .72 43 0 .019 4.9
array-examples/standard_init5_true-unreach-call_ground.i unreach-call 0 900     6000 11000    - - - - 0 .53 43 0 .023 5.0
array-examples/standard_init6_true-unreach-call_ground.i unreach-call 0 900     6000 8600    - - - - 0 .68 45 0 .018 4.8
array-examples/standard_init7_true-unreach-call_ground.i unreach-call 0 900     6000 10000    - - - - 0 .70 42 0 .022 4.8
array-examples/standard_init8_true-unreach-call_ground.i unreach-call 0 900     6000 10000    - - - - 0 .69 43 0 .024 4.8
array-examples/standard_init9_true-unreach-call_ground.i unreach-call 0 900     6000 10000    - - - - 0 .62 42 0 .022 5.0
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call 0 900     7100 10000    - - - - 0 .67 43 0 .020 4.9
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call 0 900     7200 12000    - - - - 0 .69 44 0 .019 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call 0 900     10000 12000    - - - - 0 .67 43 0 .018 4.8
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call 0 900     4200 12000    - - - - 0 .42 44 0 .024 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call 0 480     15000 6600    - - - - 0 .63 44 0 .022 4.8
array-examples/standard_partition_true-unreach-call_ground.i unreach-call 0 900     4200 12000    - - - - 0 .71 44 0 .018 4.8
array-examples/standard_password_true-unreach-call_ground.i unreach-call 0 900     7500 11000    - - - - 0 .69 43 0 .019 4.9
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call 0 900     8700 9700    - - - - 0 .57 42 0 .019 4.8
array-examples/standard_running_true-unreach-call.i unreach-call 0 430     15000 5200    - - - - 0 .59 43 0 .019 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call 0 900     300 11000    - - - - 0 .63 41 0 .023 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call 0 900     6100 9900    - - - - 0 .62 44 0 .019 5.0
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call 0 900     7200 10000    - - - - 0 .56 43 0 .022 4.8
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call 0 900     10000 10000    - - - - 0 .75 43 0 .019 4.9
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call 0 900     10000 11000    - - - - 0 .57 45 0 .023 5.0
array-examples/standard_two_index_01_true-unreach-call.i unreach-call 0 900     10000 12000    - - - - 0 .67 43 0 .019 4.9
array-examples/standard_two_index_02_true-unreach-call.i unreach-call 0 900     10000 10000    - - - - 0 .72 41 0 .023 4.8
array-examples/standard_two_index_03_true-unreach-call.i unreach-call 0 900     10000 10000    - - - - 0 .56 45 0 .019 4.9
array-examples/standard_two_index_04_true-unreach-call.i unreach-call 0 900     10000 12000    - - - - 0 .56 43 0 .019 5.0
array-examples/standard_two_index_05_true-unreach-call.i unreach-call 0 900     9900 9800    - - - - 0 .47 44 0 .019 4.9
array-examples/standard_two_index_06_true-unreach-call.i unreach-call 0 900     10000 9700    - - - - 0 .51 41 0 .018 5.0
array-examples/standard_two_index_07_true-unreach-call.i unreach-call 0 900     10000 10000    - - - - 0 .54 42 0 .019 5.0
array-examples/standard_two_index_08_true-unreach-call.i unreach-call 0 900     10000 8500    - - - - 0 .65 45 0 .018 5.0
array-examples/standard_two_index_09_true-unreach-call.i unreach-call 0 900     10000 10000    - - - - 0 .56 43 0 .018 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call 0 900     830 11000    - - - - 0 .69 44 0 .021 4.8
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call 0 900     4500 9900    - - - - 0 .57 43 0 .025 4.8
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call 0 900     6400 9900    0 .54 42 0 .022 4.8 0 .65 50 0 .0012 .29 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call 0 900     5200 10000    0 .59 41 0 .018 4.9 0 .86 50 0 .0011 .34 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call 0 900     5000 11000    0 .54 41 0 .018 4.8 0 .68 49 0 .0011 .28 - -
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call 0 900     4600 11000    0 .73 41 0 .020 4.8 0 .81 49 0 .0011 .35 - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call 0 900     5000 12000    0 .72 44 0 .019 4.8 0 .67 49 0 .0013 .26 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call 0 900     3500 7700    0 .57 43 0 .020 5.0 0 .88 49 0 .0012 .27 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call 0 900     4200 10000    - - - - 0 .63 43 0 .019 4.9
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call 0 900     4200 11000    - - - - 0 .69 43 0 .024 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call 0 660     15000 5000    - - - - 0 .69 43 0 .018 4.9
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call 0 900     6400 9800    - - - - 0 .57 43 0 .020 4.9
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call 0 900     8400 11000    - - - - 0 .68 41 0 .018 5.0
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call 0 900     4800 8900    - - - - 0 .68 43 0 .020 4.9
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call 0 900     2500 11000    - - - - 0 .55 44 0 .024 4.8
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call 0 900     1600 11000    - - - - 0 .55 41 0 .020 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call 0 900     7300 11000    - - - - 0 .65 44 0 .024 4.8
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call 0 900     4300 10000    - - - - 0 .60 43 0 .024 4.9
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call 0 900     190 13000    - - - - 0 .50 41 0 .018 5.0
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call 1 1.1   28 10    1 5.4  360 -32 6.3   270   0 2.2  210 -32 .60   18    - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call 1 2.0   29 14    1 7.9  380 -32 6.0   280   0 2.3  220 -32 .59   18    - -
reducercommutativity/rangesum20_false-unreach-call.i unreach-call 1 4.1   32 35    1 11    440 -32 6.7   320   0 3.5  220 -32 .60   18    - -
reducercommutativity/rangesum40_false-unreach-call.i unreach-call 1 15     45 170    1 28    750 -32 4.7   380   0 4.1  230 -32 .63   19    - -
reducercommutativity/rangesum60_false-unreach-call.i unreach-call 0 180     170 2600    0 92    1300 -32 5.4   480   0 4.4  220 -32 .66   19    - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call 1 1.2   31 11    1 5.1  360 -32 6.5   270   0 3.1  210 -32 .61   18    - -
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call 2 42     72 630    - - - - 0 900    1400 0 960     4900  
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call 2 490     190 5600    - - - - 0 900    3700 0 930     7000  
reducercommutativity/avg20_true-unreach-call.i unreach-call 0 900     290 11000    - - - - 0 .64 45 0 .020 4.9
reducercommutativity/avg40_true-unreach-call.i unreach-call 0 900     370 11000    - - - - 0 .69 43 0 .019 4.9
reducercommutativity/avg60_true-unreach-call.i unreach-call 0 900     440 10000    - - - - 0 .41 43 0 .021 5.0
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call 0 900     150 12000    - - - - 0 .58 43 0 .019 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call 2 .65  28 8.3  - - - - 2 130    920 0 960     3500  
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call 2 17     44 210    - - - - 0 900    3300 0 960     3500  
reducercommutativity/max20_true-unreach-call.i unreach-call 0 900     140 11000    - - - - 0 .67 42 0 .019 4.9
reducercommutativity/max40_true-unreach-call.i unreach-call 0 900     190 13000    - - - - 0 .63 43 0 .019 4.9
reducercommutativity/max60_true-unreach-call.i unreach-call 0 900     260 11000    - - - - 0 .69 43 0 .036 4.9
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call 0 900     110 11000    - - - - 0 .42 44 0 .019 4.8
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call 2 .11  26 .89 - - - - 0 900    1500 0 960     1700  
reducercommutativity/sep10_true-unreach-call.i unreach-call 2 .10  26 1.2  - - - - 0 900    1900 0 880     7000  
reducercommutativity/sep20_true-unreach-call.i unreach-call 2 .17  26 1.4  - - - - 0 900    5200 0 960     6900  
reducercommutativity/sep40_true-unreach-call.i unreach-call 2 .21  26 2.2  - - - - 0 900    1900 0 960     4600  
reducercommutativity/sep60_true-unreach-call.i unreach-call 2 .33  26 3.5  - - - - 0 900    3100 0 960     3000  
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call 0 900     120 12000    - - - - 0 .68 44 0 .023 4.8
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call 2 .12  26 .88 - - - - 0 900    980 2 420     3500  
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call 2 .099 26 1.0  - - - - 0 900    2200 0 960     5000  
reducercommutativity/sum20_true-unreach-call.i unreach-call 2 .14  26 1.5  - - - - 0 900    4500 0 960     4600  
reducercommutativity/sum40_true-unreach-call.i unreach-call 2 .17  26 2.2  - - - - 0 900    2500 0 960     4000  
reducercommutativity/sum60_true-unreach-call.i unreach-call 2 .25  26 2.7  - - - - 0 900    3100 0 960     3100  
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call 0 900     150 12000    - - - - 0 .65 43 0 .019 4.9
array-tiling/mlceu_false-unreach-call.i unreach-call 0 900     180 11000    0 .68 43 0 .019 4.8 0 .85 49 0 .0030 .26 - -
array-tiling/skippedu_false-unreach-call.i unreach-call 1 .13  28 1.9  1 3.1  260 -32 4.5   260   0 1.9  180 -32 .59   18    - -
array-tiling/mbpr2_true-unreach-call.i unreach-call 0 900     240 13000    - - - - 0 .70 43 0 .022 4.9
array-tiling/mbpr3_true-unreach-call.i unreach-call 0 900     240 11000    - - - - 0 .60 41 0 .024 4.9
array-tiling/mbpr4_true-unreach-call.i unreach-call 0 900     200 12000    - - - - 0 .66 43 0