Tool CPAchecker 1.6.1-svn 26725 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:37:17 CET; 2017-12-01 08:39:19 CET; 2017-12-01 08:43:54 CET; 2017-12-01 08:46:20 CET] [2017-12-01 07:36:53 CET; 2017-12-01 08:37:39 CET; 2017-12-01 08:42:37 CET; 2017-12-01 08:44:10 CET; 2017-12-01 08:47:49 CET] [2017-12-01 08:24:12 CET; 2017-12-01 08:38:02 CET; 2017-12-01 08:45:03 CET; 2017-12-01 08:48:04 CET] 2017-12-01 08:27:09 CET [2017-12-01 08:31:26 CET; 2017-12-01 08:38:12 CET; 2017-12-01 08:45:13 CET] 2017-12-01 04:24:37 CET [2017-12-01 07:42:15 CET; 2017-12-01 08:37:53 CET; 2017-12-01 08:44:19 CET]
Run set cpa-bam-bnb.[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-bnb.[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-bnb.[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-bnb.[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-bnb.[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-bnb.[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-bnb.[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 -svcomp18-bam-bnb -disable-java-assertions -heap 10000m [-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.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-bnb.2017-12-01_0837.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-bnb.2017-12-01_0839.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-bnb.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-bnb.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] [--full-output --validate ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cpa-bam-bnb.2017-12-01_0837.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cpa-bam-bnb.2017-12-01_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cpa-bam-bnb.2017-12-01_0846.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.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-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/cpa-bam-bnb.2017-12-01_0837.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/cpa-bam-bnb.2017-12-01_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true [--full-output --validate ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cpa-bam-bnb.2017-12-01_0837.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/cpa-bam-bnb.2017-12-01_0843.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.6  270 21   0 .54 43 0 .023 4.8 0 1.1  49 0 .0012  .30 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call 0 2.5  270 25   0 .55 43 0 .023 4.9 0 1.1  51 0 .0011  .30 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call 0 2.6  270 23   0 .53 41 0 .025 4.8 0 1.0  52 0 .0035  .30 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call 0 2.8  290 26   0 .55 41 0 .023 4.8 0 1.0  51 0 .0012  .32 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call 0 2.8  290 28   0 .53 43 0 .023 5.0 0 .94 47 0 .0012  .34 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call 0 2.5  270 23   0 .66 44 0 .021 4.8 0 1.0  50 0 .0011  .30 - -
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call 0 2.5  270 24   0 .55 41 0 .019 4.9 0 1.1  49 0 .0011  .27 - -
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call 0 2.5  260 20   0 .55 43 0 .022 4.8 0 1.1  48 0 .0012  .33 - -
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call 0 2.6  270 23   0 .53 41 0 .023 4.8 0 .92 49 0 .0032  .26 - -
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call 0 2.6  270 24   0 .55 43 0 .019 4.9 0 .95 48 0 .0013  .26 - -
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call 0 2.6  270 23   0 .55 43 0 .023 4.8 0 .84 49 0 .0012  .34 - -
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call 0 2.5  270 23   0 .69 44 0 .023 4.8 0 .96 49 0 .0027  .29 - -
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call 0 2.5  270 23   0 .54 41 0 .022 5.0 0 1.1  47 0 .0013  .26 - -
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call 0 2.6  270 25   0 .54 43 0 .021 4.9 0 .92 50 0 .0013  .26 - -
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call 0 2.6  270 21   0 .72 44 0 .024 4.9 0 .84 48 0 .0013  .30 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call 0 2.5  270 25   0 .52 43 0 .022 5.0 0 1.1  50 0 .0013  .29 - -
array-examples/standard_init1_false-unreach-call_ground.i unreach-call 0 2.4  270 22   0 .61 41 0 .022 4.9 0 1.0  47 0 .0016  .26 - -
array-examples/standard_init2_false-unreach-call_ground.i unreach-call 0 2.7  290 23   0 .53 41 0 .024 5.0 0 .94 47 0 .0013  .30 - -
array-examples/standard_init3_false-unreach-call_ground.i unreach-call 0 2.6  260 24   0 .54 44 0 .020 4.9 0 .87 47 0 .0012  .34 - -
array-examples/standard_init4_false-unreach-call_ground.i unreach-call 0 2.6  270 25   0 .54 41 0 .023 4.8 0 .87 49 0 .0016  .23 - -
array-examples/standard_init5_false-unreach-call_ground.i unreach-call 0 2.7  290 26   0 .56 41 0 .022 4.8 0 .89 49 0 .0013  .33 - -
array-examples/standard_init6_false-unreach-call_ground.i unreach-call 0 2.7  290 23   0 .52 41 0 .023 4.8 0 .80 49 0 .0014  .30 - -
array-examples/standard_init7_false-unreach-call_ground.i unreach-call 0 2.7  270 22   0 .60 43 0 .022 5.0 0 .71 49 0 .0015  .26 - -
array-examples/standard_init8_false-unreach-call_ground.i unreach-call 0 2.7  270 21   0 .53 43 0 .023 4.9 0 1.0  47 0 .0012  .34 - -
array-examples/standard_init9_false-unreach-call_ground.i unreach-call 0 2.7  270 23   0 .56 42 0 .022 4.8 0 1.0  53 0 .0011  .31 - -
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call 0 2.5  270 22   0 .61 43 0 .020 4.9 0 .96 49 0 .0014  .26 - -
array-examples/standard_partition_false-unreach-call_ground.i unreach-call 0 2.4  270 23   0 .56 43 0 .022 4.9 0 1.0  49 0 .0012  .36 - -
array-examples/standard_running_false-unreach-call.i unreach-call 0 3.0  290 26   0 .53 41 0 .026 4.8 0 .93 47 0 .0012  .29 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call 0 2.5  260 24   - - - - 0 .69 44 0 .024 4.9
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call 0 2.6  270 23   - - - - 0 .59 44 0 .022 4.8
array-examples/relax_true-unreach-call.i unreach-call 0 8.1  440 61   - - - - 0 .54 43 0 .023 4.9
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call 0 2.6  270 25   - - - - 0 .69 44 0 .022 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call 0 900    4100 8100   - - - - 0 .64 43 0 .019 5.0
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call 0 2.7  290 25   - - - - 0 .61 43 0 .020 4.9
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call 0 2.5  270 26   - - - - 0 .53 42 0 .021 4.9
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call 2 2.8  280 29   - - - - 2 3.6  260 2 5.1   230  
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call 0 3.0  290 25   - - - - 0 .58 43 0 .018 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call 0 2.5  270 20   - - - - 0 .56 43 0 .018 4.8
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call 0 2.5  270 21   - - - - 0 .65 43 0 .018 4.8
array-examples/standard_compare_true-unreach-call_ground.i unreach-call 0 2.9  290 24   - - - - 0 .65 42 0 .020 4.8
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call 0 2.5  270 23   - - - - 0 .53 43 0 .018 4.8
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call 0 2.6  270 23   - - - - 0 .54 41 0 .020 4.9
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call 0 2.7  270 20   - - - - 0 .56 42 0 .019 5.0
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call 0 2.6  270 23   - - - - 0 .68 44 0 .017 4.9
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call 0 2.6  270 23   - - - - 0 .51 41 0 .019 4.8
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call 0 2.5  270 25   - - - - 0 .65 43 0 .019 4.9
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call 0 2.5  270 21   - - - - 0 .69 44 0 .024 5.0
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call 0 2.6  270 22   - - - - 0 .51 41 0 .022 4.8
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call 0 2.6  270 22   - - - - 0 .69 41 0 .022 4.8
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call 0 2.5  270 25   - - - - 0 .59 42 0 .019 4.8
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call 0 2.5  270 21   - - - - 0 .55 43 0 .019 5.0
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call 0 2.6  270 24   - - - - 0 .69 43 0 .021 5.0
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call 0 2.5  270 21   - - - - 0 .54 43 0 .022 4.9
array-examples/standard_find_true-unreach-call_ground.i unreach-call 0 2.6  270 25   - - - - 0 .56 44 0 .024 4.8
array-examples/standard_init1_true-unreach-call_ground.i unreach-call 0 2.5  260 22   - - - - 0 .69 44 0 .022 4.9
array-examples/standard_init2_true-unreach-call_ground.i unreach-call 0 2.4  270 21   - - - - 0 .52 44 0 .021 4.9
array-examples/standard_init3_true-unreach-call_ground.i unreach-call 0 2.5  270 22   - - - - 0 .70 44 0 .018 4.8
array-examples/standard_init4_true-unreach-call_ground.i unreach-call 0 2.5  270 25   - - - - 0 .55 44 0 .022 4.8
array-examples/standard_init5_true-unreach-call_ground.i unreach-call 0 2.6  270 23   - - - - 0 .73 44 0 .019 4.9
array-examples/standard_init6_true-unreach-call_ground.i unreach-call 0 2.8  290 23   - - - - 0 .65 44 0 .020 4.8
array-examples/standard_init7_true-unreach-call_ground.i unreach-call 0 2.7  290 24   - - - - 0 .53 41 0 .019 4.8
array-examples/standard_init8_true-unreach-call_ground.i unreach-call 0 2.6  270 21   - - - - 0 .71 43 0 .024 4.8
array-examples/standard_init9_true-unreach-call_ground.i unreach-call 0 2.6  260 22   - - - - 0 .52 43 0 .019 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call 0 2.4  270 22   - - - - 0 .51 41 0 .022 5.0
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call 0 2.6  270 25   - - - - 0 .56 43 0 .020 4.9
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call 0 2.5  270 23   - - - - 0 .60 43 0 .023 4.8
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call 0 2.8  300 24   - - - - 0 .53 44 0 .020 4.9
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call 0 2.6  270 21   - - - - 0 .55 43 0 .019 4.8
array-examples/standard_partition_true-unreach-call_ground.i unreach-call 0 2.8  290 24   - - - - 0 .51 44 0 .018 4.8
array-examples/standard_password_true-unreach-call_ground.i unreach-call 0 2.5  270 21   - - - - 0 .54 41 0 .019 4.9
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call 0 2.4  260 22   - - - - 0 .75 43 0 .019 4.8
array-examples/standard_running_true-unreach-call.i unreach-call 0 2.8  290 26   - - - - 0 .74 41 0 .022 4.9
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call 0 2.5  270 24   - - - - 0 .52 41 0 .018 5.0
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call 0 2.6  270 22   - - - - 0 .58 43 0 .019 4.8
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call 0 2.6  270 26   - - - - 0 .56 44 0 .023 4.9
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call 0 2.7  270 22   - - - - 0 .73 43 0 .020 4.8
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call 0 2.5  260 24   - - - - 0 .53 41 0 .019 4.9
array-examples/standard_two_index_01_true-unreach-call.i unreach-call 0 2.7  270 25   - - - - 0 .53 43 0 .019 4.8
array-examples/standard_two_index_02_true-unreach-call.i unreach-call 0 2.7  300 24   - - - - 0 .67 43 0 .019 4.8
array-examples/standard_two_index_03_true-unreach-call.i unreach-call 0 2.7  290 27   - - - - 0 .57 44 0 .021 5.0
array-examples/standard_two_index_04_true-unreach-call.i unreach-call 0 2.6  270 23   - - - - 0 .53 43 0 .019 5.0
array-examples/standard_two_index_05_true-unreach-call.i unreach-call 0 2.5  270 24   - - - - 0 .55 44 0 .023 5.0
array-examples/standard_two_index_06_true-unreach-call.i unreach-call 0 2.6  270 24   - - - - 0 .57 43 0 .019 5.0
array-examples/standard_two_index_07_true-unreach-call.i unreach-call 0 2.5  270 25   - - - - 0 .58 42 0 .018 4.9
array-examples/standard_two_index_08_true-unreach-call.i unreach-call 0 2.5  270 23   - - - - 0 .55 42 0 .020 4.8
array-examples/standard_two_index_09_true-unreach-call.i unreach-call 0 2.6  270 24   - - - - 0 .55 44 0 .024 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call 0 2.7  290 24   - - - - 0 .53 41 0 .022 4.8
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call 0 2.8  290 26   - - - - 0 .53 41 0 .024 5.0
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call 0 2.6  270 22   0 .52 41 0 .018 4.8 0 .99 49 0 .0012  .26 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call 0 900    4200 8400   0 .51 41 0 .017 4.8 0 .98 49 0 .0014  .26 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call 0 2.5  270 22   0 .55 43 0 .025 4.9 0 .93 49 0 .0012  .32 - -
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call 0 2.6  270 25   0 .53 42 0 .019 4.9 0 .88 50 0 .0012  .30 - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call 0 2.6  270 23   0 .61 43 0 .018 4.9 0 1.0  49 0 .0036  .26 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call 0 900    5600 9300   0 .54 41 0 .020 4.8 0 1.1  50 0 .0011  .29 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call 0 2.5  270 23   - - - - 0 .68 41 0 .023 5.0
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call 0 2.5  270 22   - - - - 0 .69 44 0 .019 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call 0 900    4200 9500   - - - - 0 .65 41 0 .026 5.0
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call 0 900    4000 12000   - - - - 0 .53 41 0 .019 5.0
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call 0 900    5700 8800   - - - - 0 .65 41 0 .019 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call 0 900    3900 11000   - - - - 0 .57 43 0 .018 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call 0 900    4200 7800   - - - - 0 .71 46 0 .019 5.0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call 0 900    4300 8800   - - - - 0 .56 46 0 .019 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call 0 900    4300 12000   - - - - 0 .60 41 0 .019 5.0
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call 0 900    3900 12000   - - - - 0 .66 41 0 .019 4.9
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call 0 900    11000 6600   - - - - 0 .63 45 0 .019 5.0
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call 1 6.2  400 60   -32 3.7  260 1 74     4900   0 3.9  210 1 .62    19    - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call 1 7.6  430 65   -32 4.3  270 0 88     7000   0 3.8  220 1 .61    20    - -
reducercommutativity/rangesum20_false-unreach-call.i unreach-call 1 9.5  580 67   -32 4.6  260 0 88     7000   0 3.8  220 1 .61    21    - -
reducercommutativity/rangesum40_false-unreach-call.i unreach-call 0 900    5400 11000   0 .56 43 0 .018 5.0 0 .95 47 0 .0032  .34 - -
reducercommutativity/rangesum60_false-unreach-call.i unreach-call 0 900    5400 9800   0 .52 41 0 .023 4.8 0 .96 49 0 .0011  .29 - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call 1 17    590 120   0 91    2000 1 16     540   0 3.5  210 -32 .58    19    - -
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call -16 5.8  370 52   - - - - 0 900    2100 0 75     7000  
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call -16 7.2  420 64   - - - - 0 900    3900 0 100     7000  
reducercommutativity/avg20_true-unreach-call.i unreach-call -16 9.1  560 81   - - - - 0 900    2100 0 120     7000  
reducercommutativity/avg40_true-unreach-call.i unreach-call -16 53    2400 530   - - - - 0 900    4900 0 55     7000  
reducercommutativity/avg60_true-unreach-call.i unreach-call -16 120    4000 1200   - - - - 0 600    7000 0 70     7000  
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call 0 900    7800 8000   - - - - 0 .66 43 0 .023 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call -16 8.5  520 72   - - - - 0 3.9  280 0 67     7000  
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call -16 14    520 100   - - - - 0 6.0  350 0 79     7000  
reducercommutativity/max20_true-unreach-call.i unreach-call -16 18    710 140   - - - - 0 14    570 0 63     7000  
reducercommutativity/max40_true-unreach-call.i unreach-call 0 900    4400 12000   - - - - 0 .63 43 0 .019 4.8
reducercommutativity/max60_true-unreach-call.i unreach-call 0 900    4400 11000   - - - - 0 .63 44 0 .026 4.8
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call -16 260    3200 3100   - - - - 0 3.7  280 0 420     7000  
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call -16 13    500 100   - - - - 0 4.3  300 0 76     7000  
reducercommutativity/sep10_true-unreach-call.i unreach-call -16 34    1200 240   - - - - 0 5.4  330 0 81     7000  
reducercommutativity/sep20_true-unreach-call.i unreach-call -16 140    3900 1600   - - - - 0 15    520 0 62     7000  
reducercommutativity/sep40_true-unreach-call.i unreach-call 0 910    9900 6900   - - - - 0 .61 44 0 .019 4.8
reducercommutativity/sep60_true-unreach-call.i unreach-call 0 910    10000 7700   - - - - 0 .65 44 0 .018 4.9
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call 0 900    3900 12000   - - - - 0 .65 43 0 .019 4.9
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call -16 5.3  320 43   - - - - 0 900    2200 0 94     7000  
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call -16 6.5  360 46   - - - - 0 900    2500 0 96     7000  
reducercommutativity/sum20_true-unreach-call.i unreach-call -16 8.1  480 68   - - - - 0 900    3600 0 80     7000  
reducercommutativity/sum40_true-unreach-call.i unreach-call -16 55    2500 480   - - - - 0 900    2700 0 74     7000  
reducercommutativity/sum60_true-unreach-call.i unreach-call -16 120    3900 1100   - - - - 0 290    7000 0 69     7000  
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call -16 93    3600 1000   - - - - 0 7.1  330 0 960     5400  
array-tiling/mlceu_false-unreach-call.i unreach-call 0 58    2900 560   0 .58 41 0 .021 4.9 0 .90 47 0 .0013  .29 - -
array-tiling/skippedu_false-unreach-call.i unreach-call 1 3.9  300 34   -32 3.1  260 1 9.3   280   0 3.0  190 -32 .59    19    - -
array-tiling/mbpr2_true-unreach-call.i unreach-call 0 50    2400 440   - - - - 0 .55 43 0 .024 5.0
array-tiling/mbpr3_true-unreach-call.i unreach-call 0 56    2500 490   - - - - 0 .64 41 0 .018 5.0
array-tiling/mbpr4_true-unreach-call.i unreach-call 0 45    1800 380   - - - - 0 .53 41 0 .019 4.8
array-tiling/mbpr5_true-unreach-call.i unreach-call 0 47    1700 430   -