Tool CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution [2017-11-30 11:20:26 CET; 2017-12-01 08:43:39 CET; 2017-12-01 08:46:10 CET; 2017-12-01 08:51:01 CET; 2017-12-01 09:26:34 CET] [2017-12-01 07:36:48 CET; 2017-12-01 08:43:53 CET; 2017-12-01 08:48:17 CET; 2017-12-01 09:22:15 CET; 2017-12-01 12:49:42 CET] [2017-12-01 08:27:40 CET; 2017-12-01 08:44:11 CET; 2017-12-01 09:24:12 CET; 2017-12-01 12:51:16 CET] 2017-12-01 08:32:13 CET [2017-12-01 08:39:14 CET; 2017-12-01 08:45:03 CET; 2017-12-01 09:24:48 CET] 2017-12-01 04:24:39 CET [2017-12-01 07:43:13 CET; 2017-12-01 08:44:01 CET; 2017-12-01 09:23:17 CET]
Run set cpa-bam-slicing.[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-cpa-bam-slicing.[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-cpa-bam-slicing.[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-cpa-bam-slicing.[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-cpa-bam-slicing.[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-cpa-bam-slicing.[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-cpa-bam-slicing.[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 -ldv-bam-svcomp -disable-java-assertions -heap 10000m [-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const; -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-12-01_0843.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/cpa-bam-slicing.2017-12-01_0846.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/cpa-bam-slicing.2017-12-01_0851.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/cpa-bam-slicing.2017-12-01_0926.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cpa-bam-slicing.2017-12-01_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cpa-bam-slicing.2017-12-01_0851.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cpa-bam-slicing.2017-12-01_0926.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true [--graphml-witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/cpa-bam-slicing.2017-12-01_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/cpa-bam-slicing.2017-12-01_0851.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true [--full-output --validate ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cpa-bam-slicing.2017-12-01_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cpa-bam-slicing.2017-12-01_0851.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 2.5  260 25   0 .56 44 0 .020 4.9 0 .89 49 0 .0012  .26 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call 0 2.5  260 22   0 .56 45 0 .019 4.9 0 .85 49 0 .0013  .26 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call 0 2.5  270 23   0 .55 43 0 .017 5.0 0 .88 49 0 .0013  .26 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call 0 2.6  260 22   0 .53 41 0 .019 4.8 0 .84 49 0 .0013  .26 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call 0 2.5  260 21   0 .59 42 0 .020 4.9 0 .88 49 0 .0013  .27 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call 0 2.5  270 21   0 .53 41 0 .019 4.8 0 .83 49 0 .0013  .26 - -
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call 0 2.5  270 19   0 .58 42 0 .019 4.9 0 .88 49 0 .0013  .26 - -
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call 0 2.5  270 22   0 .57 43 0 .021 4.8 0 .66 50 0 .0014  .26 - -
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call 0 2.6  270 26   0 .58 44 0 .020 5.0 0 .90 49 0 .0014  .27 - -
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call 0 2.5  270 21   0 .59 44 0 .024 4.9 0 .85 49 0 .0013  .27 - -
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call 0 2.7  270 24   0 .57 41 0 .020 4.9 0 .85 50 0 .0013  .26 - -
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call 0 2.6  270 24   0 .56 41 0 .018 4.9 0 .84 49 0 .0012  .26 - -
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call 0 2.6  260 23   0 .52 41 0 .018 4.9 0 .85 47 0 .0013  .26 - -
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call 0 2.6  260 25   0 .60 44 0 .019 4.8 0 .88 49 0 .0016  .26 - -
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call 0 2.5  260 26   0 .59 44 0 .020 4.9 0 .85 49 0 .0017  .30 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call 0 2.7  270 26   0 .54 43 0 .020 4.9 0 .87 50 0 .0016  .27 - -
array-examples/standard_init1_false-unreach-call_ground.i unreach-call 0 2.5  260 21   0 .54 41 0 .024 4.8 0 .90 49 0 .0015  .26 - -
array-examples/standard_init2_false-unreach-call_ground.i unreach-call 0 2.6  270 25   0 .58 43 0 .019 4.9 0 .87 49 0 .0014  .26 - -
array-examples/standard_init3_false-unreach-call_ground.i unreach-call 0 2.5  270 23   0 .55 43 0 .020 4.9 0 .87 49 0 .0011  .33 - -
array-examples/standard_init4_false-unreach-call_ground.i unreach-call 0 2.5  270 23   0 .52 41 0 .018 5.0 0 .88 49 0 .0013  .26 - -
array-examples/standard_init5_false-unreach-call_ground.i unreach-call 0 2.4  270 22   0 .57 46 0 .020 4.9 0 .83 49 0 .0013  .27 - -
array-examples/standard_init6_false-unreach-call_ground.i unreach-call 0 2.6  260 25   0 .55 43 0 .019 4.8 0 .82 49 0 .0012  .26 - -
array-examples/standard_init7_false-unreach-call_ground.i unreach-call 0 2.7  270 21   0 .55 43 0 .020 4.8 0 .86 49 0 .0014  .28 - -
array-examples/standard_init8_false-unreach-call_ground.i unreach-call 0 2.5  270 22   0 .54 41 0 .020 5.0 0 .87 50 0 .0014  .28 - -
array-examples/standard_init9_false-unreach-call_ground.i unreach-call 0 2.5  270 22   0 .54 43 0 .019 4.9 0 .89 49 0 .0013  .28 - -
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call 0 2.6  270 24   0 .57 42 0 .019 4.9 0 .85 49 0 .0013  .29 - -
array-examples/standard_partition_false-unreach-call_ground.i unreach-call 0 2.5  270 21   0 .65 43 0 .018 4.9 0 .81 50 0 .0013  .30 - -
array-examples/standard_running_false-unreach-call.i unreach-call 0 2.5  270 21   0 .55 43 0 .020 4.8 0 .85 49 0 .0013  .26 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call 0 2.6  260 26   - - - - 0 .67 45 0 .021 4.8
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call 0 2.6  270 22   - - - - 0 .64 41 0 .019 4.8
array-examples/relax_true-unreach-call.i unreach-call 0 5.7  310 48   - - - - 0 .55 43 0 .024 4.9
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call 0 2.6  260 25   - - - - 0 .53 43 0 .018 4.8
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call 0 900    4100 11000   - - - - 0 .53 41 0 .018 4.9
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call 0 2.5  260 21   - - - - 0 .66 44 0 .019 4.9
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call 0 2.5  270 22   - - - - 0 .55 41 0 .018 4.8
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call 2 2.7  270 25   - - - - 2 3.7  260 2 7.2   290  
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call 0 2.6  260 23   - - - - 0 .68 43 0 .022 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call 0 2.5  270 24   - - - - 0 .56 44 0 .018 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call 0 2.5  270 21   - - - - 0 .53 41 0 .024 4.8
array-examples/standard_compare_true-unreach-call_ground.i unreach-call 0 2.5  260 23   - - - - 0 .67 43 0 .023 4.9
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call 0 2.5  260 23   - - - - 0 .52 43 0 .022 4.8
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call 0 2.5  260 25   - - - - 0 .70 44 0 .017 4.9
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call 0 2.5  260 24   - - - - 0 .55 45 0 .020 5.0
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call 0 2.6  260 23   - - - - 0 .52 41 0 .020 5.0
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call 0 2.6  270 24   - - - - 0 .54 43 0 .023 4.8
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call 0 2.6  270 23   - - - - 0 .69 41 0 .020 4.8
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call 0 2.5  270 22   - - - - 0 .58 43 0 .018 5.0
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call 0 2.6  270 24   - - - - 0 .66 44 0 .021 4.9
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call 0 2.5  270 23   - - - - 0 .54 45 0 .018 4.9
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call 0 2.5  270 23   - - - - 0 .54 41 0 .019 4.8
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call 0 2.5  270 21   - - - - 0 .57 41 0 .019 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call 0 2.6  270 21   - - - - 0 .65 45 0 .023 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call 0 2.6  270 25   - - - - 0 .53 43 0 .018 4.8
array-examples/standard_find_true-unreach-call_ground.i unreach-call 0 2.6  270 24   - - - - 0 .70 44 0 .021 4.8
array-examples/standard_init1_true-unreach-call_ground.i unreach-call 0 2.5  260 25   - - - - 0 .52 42 0 .018 4.8
array-examples/standard_init2_true-unreach-call_ground.i unreach-call 0 2.5  270 22   - - - - 0 .61 44 0 .021 4.9
array-examples/standard_init3_true-unreach-call_ground.i unreach-call 0 2.6  260 27   - - - - 0 .59 42 0 .020 4.8
array-examples/standard_init4_true-unreach-call_ground.i unreach-call 0 2.6  270 23   - - - - 0 .52 44 0 .018 4.9
array-examples/standard_init5_true-unreach-call_ground.i unreach-call 0 2.5  260 23   - - - - 0 .54 43 0 .019 4.8
array-examples/standard_init6_true-unreach-call_ground.i unreach-call 0 2.5  260 25   - - - - 0 .54 43 0 .025 4.8
array-examples/standard_init7_true-unreach-call_ground.i unreach-call 0 2.6  270 26   - - - - 0 .54 41 0 .018 4.9
array-examples/standard_init8_true-unreach-call_ground.i unreach-call 0 2.7  270 24   - - - - 0 .52 44 0 .019 5.0
array-examples/standard_init9_true-unreach-call_ground.i unreach-call 0 2.6  270 24   - - - - 0 .57 44 0 .019 5.0
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call 0 2.5  270 21   - - - - 0 .65 43 0 .019 5.0
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call 0 2.4  260 21   - - - - 0 .56 41 0 .019 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call 0 2.4  260 21   - - - - 0 .53 41 0 .019 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call 0 2.6  270 23   - - - - 0 .89 43 0 .024 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call 0 2.6  270 24   - - - - 0 .72 43 0 .026 5.0
array-examples/standard_partition_true-unreach-call_ground.i unreach-call 0 2.5  270 23   - - - - 0 .67 41 0 .019 4.8
array-examples/standard_password_true-unreach-call_ground.i unreach-call 0 2.5  260 21   - - - - 0 .54 43 0 .021 5.0
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call 0 2.5  270 22   - - - - 0 .67 41 0 .018 5.0
array-examples/standard_running_true-unreach-call.i unreach-call 0 2.5  270 22   - - - - 0 .66 44 0 .023 4.9
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call 0 2.5  270 26   - - - - 0 .65 43 0 .024 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call 0 2.5  270 24   - - - - 0 .54 43 0 .019 4.8
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call 0 2.6  270 23   - - - - 0 .56 42 0 .023 4.8
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call 0 2.7  270 22   - - - - 0 .57 43 0 .025 5.0
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call 0 2.5  270 22   - - - - 0 .54 43 0 .023 4.8
array-examples/standard_two_index_01_true-unreach-call.i unreach-call 0 2.5  260 23   - - - - 0 .54 43 0 .024 5.0
array-examples/standard_two_index_02_true-unreach-call.i unreach-call 0 2.5  270 25   - - - - 0 .70 43 0 .018 4.8
array-examples/standard_two_index_03_true-unreach-call.i unreach-call 0 2.5  270 23   - - - - 0 .54 41 0 .023 4.8
array-examples/standard_two_index_04_true-unreach-call.i unreach-call 0 2.4  270 24   - - - - 0 .72 41 0 .021 4.9
array-examples/standard_two_index_05_true-unreach-call.i unreach-call 0 2.6  270 24   - - - - 0 .55 42 0 .019 4.8
array-examples/standard_two_index_06_true-unreach-call.i unreach-call 0 2.5  260 23   - - - - 0 .74 43 0 .025 4.8
array-examples/standard_two_index_07_true-unreach-call.i unreach-call 0 2.5  260 24   - - - - 0 .54 43 0 .023 4.8
array-examples/standard_two_index_08_true-unreach-call.i unreach-call 0 2.5  270 21   - - - - 0 .53 41 0 .023 4.9
array-examples/standard_two_index_09_true-unreach-call.i unreach-call 0 2.6  270 25   - - - - 0 .69 41 0 .018 4.9
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call 0 2.5  270 22   - - - - 0 .53 42 0 .024 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call 0 2.5  260 22   - - - - 0 .54 41 0 .022 4.8
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call 0 2.7  270 24   0 .58 42 0 .019 4.9 0 .86 48 0 .0012  .33 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call 0 900    4200 11000   0 .57 43 0 .019 4.8 0 .80 48 0 .0016  .26 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call 0 2.5  270 22   0 .55 42 0 .019 4.8 0 .83 47 0 .0011  .29 - -
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call 0 2.5  260 22   0 .58 42 0 .019 5.0 0 .81 49 0 .0011  .29 - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call 0 2.5  270 23   0 .54 41 0 .018 5.0 0 .85 49 0 .0013  .28 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call 0 900    6400 11000   0 .56 41 0 .019 4.9 0 .88 50 0 .0013  .26 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call 0 2.7  260 23   - - - - 0 .52 41 0 .026 4.8
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call 0 2.7  270 22   - - - - 0 .62 41 0 .020 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call 0 900    4200 9900   - - - - 0 .55 44 0 .022 5.0
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call 0 900    4200 9300   - - - - 0 .52 42 0 .019 4.9
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call 0 910    11000 4400   - - - - 0 .61 41 0 .024 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call 0 900    4200 9200   - - - - 0 .52 42 0 .021 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call 0 900    5100 11000   - - - - 0 .69 41 0 .018 4.8
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call 0 900    3800 10000   - - - - 0 .67 44 0 .026 4.8
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call 0 900    3900 10000   - - - - 0 .55 43 0 .018 5.0
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call 0 900    7800 6400   - - - - 0 .55 41 0 .024 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call -16 3.9  290 33   - - - - 0 900    2600 2 4.8   230  
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call 1 6.5  410 60   -32 4.5  260 -32 5.1   240   0 3.2  220 1 .60    19    - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call 1 7.7  530 58   -32 4.4  290 -32 5.0   230   0 3.6  230 1 .59    20    - -
reducercommutativity/rangesum20_false-unreach-call.i unreach-call 1 13    740 120   -32 5.2  270 -32 5.3   260   0 4.0  220 1 .65    21    - -
reducercommutativity/rangesum40_false-unreach-call.i unreach-call 1 92    3700 900   -32 5.6  270 -32 5.6   250   0 3.8  210 1 .65    23    - -
reducercommutativity/rangesum60_false-unreach-call.i unreach-call 1 210    4600 2200   -32 6.2  270 -32 5.6   260   0 4.1  210 1 .67    26    - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call 0 15    650 110   0 92    1900 -32 5.0   230   0 3.3  190 -32 .61    19    - -
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call -16 5.5  380 52   - - - - 2 3.4  260 0 960     5400  
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call -16 7.4  450 57   - - - - 2 4.0  260 0 60     7000  
reducercommutativity/avg20_true-unreach-call.i unreach-call -16 10    680 89   - - - - 2 4.7  270 0 58     7000  
reducercommutativity/avg40_true-unreach-call.i unreach-call -16 180    3200 1500   - - - - 2 6.0  270 0 67     7000  
reducercommutativity/avg60_true-unreach-call.i unreach-call -16 630    4600 7000   - - - - 2 5.6  270 0 74     7000  
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call -16 5.8  410 50   - - - - 0 900    2300 2 6.3   230  
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call -16 5.6  300 51   - - - - 2 4.8  260 0 61     7000  
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call -16 7.2  430 64   - - - - 2 5.3  270 0 68     7000  
reducercommutativity/max20_true-unreach-call.i unreach-call -16 11    540 93   - - - - 2 4.6  270 0 57     7000  
reducercommutativity/max40_true-unreach-call.i unreach-call -16 370    3000 4800   - - - - 2 5.8  270 0 68     7000  
reducercommutativity/max60_true-unreach-call.i unreach-call 0 900    4000 12000   - - - - 0 .67 43 0 .023 4.8
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call -16 9.2  470 75   - - - - 0 900    2500 2 5.0   230  
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call -16 6.5  360 56   - - - - 2 4.1  260 0 370     7000  
reducercommutativity/sep10_true-unreach-call.i unreach-call -16 14    660 100   - - - - 2 5.4  270 0 74     7000  
reducercommutativity/sep20_true-unreach-call.i unreach-call -16 63    3200 670   - - - - 2 6.0  270 0 55     7000  
reducercommutativity/sep40_true-unreach-call.i unreach-call -16 850    9200 7100   - - - - 2 5.8  270 0 66     7000  
reducercommutativity/sep60_true-unreach-call.i unreach-call 0 910    9700 7300   - - - - 0 .62 41 0 .019 4.8
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call -16 880    6700 12000   - - - - 0 900    2800 2 6.2   230  
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call -16 5.2  320 37   - - - - 2 4.6  260 0 960     4900  
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call -16 7.3  430 59   - - - - 2 3.9  260 0 56     7000  
reducercommutativity/sum20_true-unreach-call.i unreach-call -16 11    620 110   - - - - 2 5.2  270 0 56     7000  
reducercommutativity/sum40_true-unreach-call.i unreach-call -16 160    3500 1800   - - - - 2 5.5  270 0 66     7000  
reducercommutativity/sum60_true-unreach-call.i unreach-call -16 630    4500 7200   - - - - 2 5.6  270 0 68     7000  
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call -16 4.9  310 41   - - - - 0 900    2300 2 5.0   230  
array-tiling/mlceu_false-unreach-call.i unreach-call 0 3.4  280 31   0 92    2000 -32 7.6   260   0 2.8  180 -32 .60    19    - -
array-tiling/skippedu_false-unreach-call.i unreach-call 1 3.6  290 30   0 92    2000 1 7.9   280   0 2.9  210 -32 .59    19    - -
array-tiling/mbpr2_true-unreach-call.i unreach-call -16 4.0  300 36   - - - - 0 900    2800 2 6.3   260  
array-tiling/mbpr3_true-unreach-call.i unreach-call -16 4.5  310 38   - - - - 0 900    2800 2 7.5   270  
array-tiling/mbpr4_true-unreach-call.i unreach-call -16 5.0  310 48   -