Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution [2017-12-01 22:41:19 CET; 2017-12-02 23:08:57 CET; 2017-12-03 01:39:21 CET; 2017-12-03 04:09:48 CET; 2017-12-03 05:53:57 CET] [2017-12-02 21:10:50 CET; 2017-12-03 00:45:11 CET; 2017-12-03 03:55:46 CET; 2017-12-03 05:12:06 CET; 2017-12-03 06:31:42 CET] [2017-12-02 22:39:24 CET; 2017-12-03 01:25:52 CET; 2017-12-03 05:44:30 CET; 2017-12-03 06:32:20 CET] 2017-12-02 22:51:52 CET [2017-12-02 23:01:21 CET; 2017-12-03 01:32:11 CET; 2017-12-03 05:48:14 CET] 2017-12-02 19:44:15 CET [2017-12-02 21:36:25 CET; 2017-12-03 00:52:42 CET; 2017-12-03 05:20:50 CET]
Run set symbiotic.[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-symbiotic.[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-symbiotic.[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-symbiotic.[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-symbiotic.[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-symbiotic.[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-symbiotic.[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 --witness witness.graphml [-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-02_2308.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/symbiotic.2017-12-03_0139.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/symbiotic.2017-12-03_0409.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/symbiotic.2017-12-03_0553.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/symbiotic.2017-12-03_0409.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/symbiotic.2017-12-03_0553.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --graphml-witness ../../results-verified/symbiotic.2017-12-03_0409.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml] -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true [--full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml; --full-output --validate ../../results-verified/symbiotic.2017-12-03_0409.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 1 1.6   200   17    0 92    2600 -32 3.3   240   0 2.0  210 1 .66   18    - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call 0 900     4000   9800    0 .50 44 0 .017 4.8 0 .66 49 0 .0011 .29 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call 0 900     4100   12000    0 .62 44 0 .018 4.8 0 .67 49 0 .0011 .26 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call 0 900     100   8500    0 .63 44 0 .019 4.8 0 .67 49 0 .0036 .26 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call 0 900     100   9900    0 .74 43 0 .019 4.9 0 .84 49 0 .0011 .26 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call 1 1.1   140   15    0 91    2000 -32 3.4   220   0 2.8  210 1 12      18    - -
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call 1 3.4   300   45    0 91    1900 -32 4.4   240   0 1.9  180 1 .58   18    - -
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call 1 4.2   350   59    0 92    2000 -32 3.4   220   0 2.0  210 1 .56   18    - -
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call 1 4.5   370   66    0 92    2000 -32 4.7   230   0 2.1  210 1 .60   18    - -
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call 1 5.0   400   69    0 91    2000 -32 3.4   230   0 2.9  210 1 .59   18    - -
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call 1 5.3   430   59    0 92    2000 -32 3.3   240   0 2.0  210 1 .57   18    - -
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call 1 5.8   470   67    0 92    2100 -32 5.0   230   0 3.0  210 1 .61   18    - -
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call 1 6.1   500   71    0 92    2100 -32 3.3   220   0 3.0  210 1 .62   18    - -
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call 1 6.5   530   82    0 91    2100 -32 3.4   230   0 2.0  210 1 .57   18    - -
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call 1 7.0   560   88    0 92    2100 -32 3.8   240   0 2.1  210 1 .61   18    - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call 1 .80  71   11    0 92    850 -32 3.1   230   0 2.7  200 1 .56   18    - -
array-examples/standard_init1_false-unreach-call_ground.i unreach-call 1 .42  39   5.7  0 91    720 -32 3.1   230   0 2.0  180 1 .57   18    - -
array-examples/standard_init2_false-unreach-call_ground.i unreach-call 1 .64  68   8.5  0 92    760 -32 3.1   230   0 2.7  210 1 .56   18    - -
array-examples/standard_init3_false-unreach-call_ground.i unreach-call 1 .88  95   12    0 92    820 -32 3.5   230   0 2.1  210 1 .56   18    - -
array-examples/standard_init4_false-unreach-call_ground.i unreach-call 1 1.1   120   15    0 92    840 -32 3.5   240   0 2.8  210 1 .56   18    - -
array-examples/standard_init5_false-unreach-call_ground.i unreach-call 1 1.3   150   18    0 92    760 -32 4.9   230   0 2.9  210 1 .56   18    - -
array-examples/standard_init6_false-unreach-call_ground.i unreach-call 1 1.5   180   23    0 92    660 -32 4.7   230   0 2.0  210 1 .60   18    - -
array-examples/standard_init7_false-unreach-call_ground.i unreach-call 1 1.8   200   24    0 91    730 -32 3.3   230   0 2.1  210 1 .56   18    - -
array-examples/standard_init8_false-unreach-call_ground.i unreach-call 1 2.0   230   28    0 92    690 -32 4.9   230   0 2.8  210 1 .59   18    - -
array-examples/standard_init9_false-unreach-call_ground.i unreach-call 1 2.2   260   31    0 91    690 -32 3.3   230   0 2.1  210 1 .56   18    - -
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call 0 100     15000   1200    0 .42 44 0 .018 4.8 0 .85 49 0 .0011 .29 - -
array-examples/standard_partition_false-unreach-call_ground.i unreach-call 0 900     12000   9400    0 .70 43 0 .018 4.8 0 .65 51 0 .0011 .26 - -
array-examples/standard_running_false-unreach-call.i unreach-call 0 900     11000   13000    0 .56 44 0 .020 5.0 0 .86 49 0 .0013 .26 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call 2 .15  11   1.8  - - - - 0 920    6100 2 7.2   280  
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call 0 900     1300   10000    - - - - 0 .54 43 0 .018 4.9
array-examples/relax_true-unreach-call.i unreach-call 0 370     180   1900    - - - - 0 .63 43 0 .020 4.9
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call 0 460     15000   3900    - - - - 0 .54 43 0 .020 5.0
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call 0 900     830   11000    - - - - 0 .55 43 0 .019 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call 0 900     5400   8400    - - - - 0 .70 43 0 .019 4.8
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call 0 100     15000   990    - - - - 0 .55 41 0 .032 4.9
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call 2 .15  11   1.3  - - - - 2 3.5  260 2 5.0   230  
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call 0 900     3900   9800    - - - - 0 .59 44 0 .019 4.9
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call 0 900     100   8100    - - - - 0 .60 44 0 .024 4.8
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call 0 900     10000   10000    - - - - 0 .53 43 0 .024 4.8
array-examples/standard_compare_true-unreach-call_ground.i unreach-call 0 900     11000   11000    - - - - 0 .56 41 0 .018 4.8
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call 2 2.2   130   29    - - - - 0 900    5400 0 960     4600  
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call 2 2.5   150   32    - - - - 0 690    7000 0 960     4800  
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call 2 2.9   160   34    - - - - 0 900    6100 0 960     4800  
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call 2 3.2   170   38    - - - - 0 910    5900 0 960     4800  
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call 2 3.5   180   45    - - - - 0 900    6100 0 960     4900  
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call 2 3.9   190   49    - - - - 0 900    6000 0 960     4800  
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call 2 4.1   200   50    - - - - 0 770    7000 0 960     4900  
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call 2 4.6   210   71    - - - - 0 890    7000 0 960     4900  
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call 2 5.1   220   61    - - - - 0 900    6700 0 960     5000  
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call 2 1.4   51   18    - - - - 0 900    3000 0 960     4800  
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call 2 1.8   59   27    - - - - 0 900    4000 0 960     5000  
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call 2 1.5   82   20    - - - - 0 900    3600 0 960     4800  
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call 2 1.1   41   16    - - - - 0 900    4700 0 960     4400  
array-examples/standard_find_true-unreach-call_ground.i unreach-call 0 530     2400   8300    - - - - 0 .69 45 0 .020 4.9
array-examples/standard_init1_true-unreach-call_ground.i unreach-call 2 .80  32   10    - - - - 0 910    5000 0 960     2000  
array-examples/standard_init2_true-unreach-call_ground.i unreach-call 2 .97  39   14    - - - - 0 900    4700 0 960     2900  
array-examples/standard_init3_true-unreach-call_ground.i unreach-call 2 1.2   47   17    - - - - 0 900    4500 0 960     4800  
array-examples/standard_init4_true-unreach-call_ground.i unreach-call 2 1.4   54   21    - - - - 0 900    4800 0 960     5100  
array-examples/standard_init5_true-unreach-call_ground.i unreach-call 2 1.6   61   23    - - - - 0 900    4500 0 960     5200  
array-examples/standard_init6_true-unreach-call_ground.i unreach-call 2 1.8   68   27    - - - - 0 900    4800 0 960     5200  
array-examples/standard_init7_true-unreach-call_ground.i unreach-call 2 2.0   75   27    - - - - 0 900    5000 0 960     4900  
array-examples/standard_init8_true-unreach-call_ground.i unreach-call 2 2.2   83   30    - - - - 0 900    5000 0 960     5000  
array-examples/standard_init9_true-unreach-call_ground.i unreach-call 2 2.4   90   38    - - - - 0 900    4400 0 960     5600  
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call 0 100     15000   940    - - - - 0 .56 42 0 .018 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call 0 100     15000   1000    - - - - 0 .57 41 0 .020 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call 2 .69  45   8.6  - - - - 0 900    5300 0 960     1600  
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call 0 900     3800   8200    - - - - 0 .66 44 0 .018 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call 0 16     15000   180    - - - - 0 .66 44 0 .019 4.9
array-examples/standard_partition_true-unreach-call_ground.i unreach-call 0 900     12000   8700    - - - - 0 .53 42 0 .017 4.8
array-examples/standard_password_true-unreach-call_ground.i unreach-call 0 900     10000   10000    - - - - 0 .53 44 0 .021 4.9
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call 2 1.1   75   13    - - - - 0 900    4700 0 960     1800  
array-examples/standard_running_true-unreach-call.i unreach-call 0 900     7400   11000    - - - - 0 .59 44 0 .023 4.9
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call 0 900     410   9100    - - - - 0 .64 41 0 .020 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call 2 .93  33   11    - - - - 0 900    2600 0 960     2400  
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call 0 900     640   9600    - - - - 0 .62 44 0 .018 4.8
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call 0 28     2200   250    - - - - 0 .70 45 0 .019 4.8
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call 0 26     2200   180    - - - - 0 .57 43 0 .018 4.8
array-examples/standard_two_index_01_true-unreach-call.i unreach-call 2 .38  22   4.2  - - - - 0 900    4100 0 960     2900  
array-examples/standard_two_index_02_true-unreach-call.i unreach-call 2 1.9   120   24    - - - - 0 900    4800 0 960     3500  
array-examples/standard_two_index_03_true-unreach-call.i unreach-call 2 .32  20   3.3  - - - - 0 900    5000 0 960     3100  
array-examples/standard_two_index_04_true-unreach-call.i unreach-call 2 1.6   120   22    - - - - 0 900    5100 0 960     3100  
array-examples/standard_two_index_05_true-unreach-call.i unreach-call 2 1.5   120   18    - - - - 0 900    4600 0 960     3000  
array-examples/standard_two_index_06_true-unreach-call.i unreach-call 2 .33  20   3.6  - - - - 0 900    3900 0 960     3400  
array-examples/standard_two_index_07_true-unreach-call.i unreach-call 2 1.5   120   19    - - - - 0 900    4900 0 960     2900  
array-examples/standard_two_index_08_true-unreach-call.i unreach-call 2 1.5   120   19    - - - - 0 900    4000 0 960     3800  
array-examples/standard_two_index_09_true-unreach-call.i unreach-call 2 1.4   120   18    - - - - 0 900    4300 0 960     3700  
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call 0 900     500   11000    - - - - 0 .53 43 0 .019 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call 2 1.6   170   19    - - - - 0 900    3900 0 960     2200  
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call 1 .42  44   6.1  0 92    800 -32 4.4   220   0 1.9  180 1 .57   18    - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call 1 .39  38   4.8  0 92    940 0 97     4900   0 2.0  190 1 .56   18    - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call 1 2.0   200   25    0 91    2100 -32 3.1   230   0 2.0  210 1 .58   18    - -
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call 1 .45  42   5.9  0 93    1100 0 97     4800   0 2.0  210 1 .58   18    - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call 0 900     3900   9400    0 .40 44 0 .019 4.9 0 .88 51 0 .0011 .29 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call 0 900     1200   11000    0 .55 44 0 .018 4.9 0 .86 49 0 .0012 .26 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call 0 20     15000   230    - - - - 0 .54 43 0 .028 4.8
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call 0 14     15000   180    - - - - 0 .56 43 0 .019 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call 2 .86  32   12    - - - - 0 900    3900 0 960     5000  
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call 0 11     360   140    - - - - 0 .55 43 0 .020 4.8
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call 2 3.0   110   41    - - - - 0 910    6300 2 12     460  
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call 0 900     3700   8200    - - - - 0 .54 41 0 .020 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call 0 330     15000   4200    - - - - 0 .50 41 0 .019 4.8
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call 2 2.9   110   34    - - - - 0 690    7000 0 960     5900  
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call 2 1.9   71   25    - - - - 0 900    3800 0 960     5800  
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call 0 900     3700   8000    - - - - 0 .55 43 0 .017 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call 0 .19  11   2.1  - - - - 0 .62 43 0 .017 5.0
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call 1 .21  12   2.4  1 7.5  370 -32 3.6   230   0 2.8  220 1 .61   18    - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call 1 .21  13   2.8  0 92    560 -32 4.9   240   0 2.1  210 1 .57   18    - -
reducercommutativity/rangesum20_false-unreach-call.i unreach-call 1 .52  24   7.1  0 92    680 -32 3.3   240   0 2.1  210 1 .60   18    - -
reducercommutativity/rangesum40_false-unreach-call.i unreach-call 1 .46  27   6.0  0 92    800 -32 5.1   240   0 2.1  210 1 .58   18    - -
reducercommutativity/rangesum60_false-unreach-call.i unreach-call 1 .74  32   10    1 50    1600 -32 3.5   230   0 2.1  210 1 .57   18    - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call 0 .21  12   2.0  0 .45 43 0 .018 4.8 0 .68 49 0 .0024 .35 - -
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call 2 .19  11   1.9  - - - - 0 900    1500 0 960     4800  
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call 2 .19  11   2.0  - - - - 0 900    3900 0 960     7000  
reducercommutativity/avg20_true-unreach-call.i unreach-call 2 .20  11   1.5  - - - - 0 900    4900 0 960     1900  
reducercommutativity/avg40_true-unreach-call.i unreach-call 2 .17  11   1.9  - - - - 0 900    3500 0 960     4300  
reducercommutativity/avg60_true-unreach-call.i unreach-call 2 .18  11   2.6  - - - - 0 900    3700 0 960     3300  
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call 0 .21  12   2.1  - - - - 0 .69 43 0 .019 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call 2 3.9   14   53    - - - - 2 110    910 0 960     4100  
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call 2 200     20   3300    - - - - 0 900    2900 0 960     3300  
reducercommutativity/max20_true-unreach-call.i unreach-call 0 900     58   13000    - - - - 0 .55 43 0 .018 5.0
reducercommutativity/max40_true-unreach-call.i unreach-call 0 900     89   12000    - - - - 0 .72 44 0 .018 4.9
reducercommutativity/max60_true-unreach-call.i unreach-call 0 900     130   12000    - - - - 0 .65 45 0 .019 4.9
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call 0 .21  11   2.3  - - - - 0 .41 45 0 .018 4.8
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call 2 .17  11   1.9  - - - - 0 900    1400 0 960     1800  
reducercommutativity/sep10_true-unreach-call.i unreach-call 2 .19  11   1.9  - - - - 0 900    1800 0 920     7000  
reducercommutativity/sep20_true-unreach-call.i unreach-call 2 .19  11   2.1  - - - - 0 900    4800 0 840     7000  
reducercommutativity/sep40_true-unreach-call.i unreach-call 2 .18  11   2.3  - - - - 0 900    1700 0 960     4600  
reducercommutativity/sep60_true-unreach-call.i unreach-call 2 .21  11   2.2  - - - - 0 900    2900 0 960     3200  
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call 0 .20  12   2.4  - - - - 0 .59 43 0 .019 4.8
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call 2 .19  11   2.1  - - - - 0 900    970 2 380     3200  
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call 2 .19  11   2.2  - - - - 0 900    2200 0 960     5000  
reducercommutativity/sum20_true-unreach-call.i unreach-call 2 .20  11   2.0  - - - - 0 900    4200 0 960     4600  
reducercommutativity/sum40_true-unreach-call.i unreach-call 2 .19  11   2.2  - - - - 0 900    2600 0 960     4600  
reducercommutativity/sum60_true-unreach-call.i unreach-call 2 .19  11   2.1  - - - - 0 900    3300 0 960     3300  
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call 0 .20  12   2.2  - - - - 0 .68 43 0 .024 4.8
array-tiling/mlceu_false-unreach-call.i unreach-call 0 .17  12   2.2  0 .40 41 0 .019 4.9 0 .69 49 0 .0011 .27 - -
array-tiling/skippedu_false-unreach-call.i unreach-call 0 .21  12   2.4  0 .52 42 0 .019 4.8 0 .66 49 0 .0011 .32 - -
array-tiling/mbpr2_true-unreach-call.i unreach-call 0 .21  11   2.0  - - - -