Tool CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
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.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-05 05:46:16 CET 2018-12-06 09:44:44 CET 2018-12-06 10:50:29 CET 2018-12-06 10:57:45 CET 2018-12-12 19:32:16 CET 2018-12-06 08:37:23 CET 2018-12-06 09:52:34 CET
Run set cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Arrays uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Arrays
Options -svcomp19 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i 0 960   880   6200 7100 0     0   0 .65 .39 44 0   0   0 5.3   2.9   260   .65 0   0 1.0  .65 49 0   0   0 .0056 .0075 .53 0     0   - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 960   890   4200 8300 0     0   0 .71 .44 44 0   0   0 5.2   2.9   260   .65 0   0 .99 .65 49 0   0   0 .0018 .0024 .53 0     0   - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 960   900   4400 6600 0     0   0 .61 .40 42 0   0   0 5.2   2.8   260   .65 0   0 .98 .64 49 0   0   0 .0055 .0072 .53 0     0   - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 960   890   4500 10000 0     0   0 .63 .39 43 0   0   0 5.3   2.9   270   .61 0   0 1.0  .65 49 0   0   0 .0022 .0028 .53 0     0   - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 960   900   4200 9500 0     0   0 .67 .41 43 0   0   0 5.5   2.9   270   .61 0   0 1.0  .68 50 0   0   0 .0018 .0024 .53 0     0   - -
array-examples/standard_allDiff2_false-unreach-call_ground.i 0 960   890   4300 7600 0     0   0 .66 .40 42 0   0   0 5.6   3.1   260   .65 0   0 1.0  .64 49 0   0   0 .0051 .0066 .54 0     0   - -
array-examples/standard_copy1_false-unreach-call_ground.i 0 960   890   3400 9600 0     0   0 .72 .45 42 0   0   0 5.0   2.8   250   .65 0   0 .97 .63 48 0   0   0 .0019 .0025 .52 0     0   - -
array-examples/standard_copy2_false-unreach-call_ground.i 0 960   890   3900 9500 0     0   0 .64 .39 45 0   0   0 5.2   2.8   260   .65 0   0 1.0  .65 49 0   0   0 .0061 .0076 .39 0     0   - -
array-examples/standard_copy3_false-unreach-call_ground.i 0 960   890   5000 11000 0     0   0 .76 .46 42 0   0   0 5.2   2.9   270   .65 0   0 .99 .66 48 0   0   0 .0017 .0022 .53 0     0   - -
array-examples/standard_copy4_false-unreach-call_ground.i 0 960   880   3000 11000 0     0   0 .67 .42 44 0   0   0 5.9   3.1   270   .65 0   0 .98 .64 49 0   0   0 .0018 .0024 .52 0     0   - -
array-examples/standard_copy5_false-unreach-call_ground.i 0 970   890   4800 10000 0     0   0 .75 .47 42 0   0   0 5.1   3.2   260   .65 0   0 1.0  .65 49 0   0   0 .0038 .0049 .52 0     0   - -
array-examples/standard_copy6_false-unreach-call_ground.i 0 970   890   4700 8700 0     0   0 .66 .40 44 0   0   0 5.5   3.4   270   .65 0   0 1.0  .66 51 0   0   0 .0051 .0063 .52 0     0   - -
array-examples/standard_copy7_false-unreach-call_ground.i 0 960   890   4500 9800 0     0   0 .64 .40 42 0   0   0 5.2   2.8   260   .61 0   0 1.0  .66 49 0   0   0 .0020 .0030 .53 0     0   - -
array-examples/standard_copy8_false-unreach-call_ground.i 0 960   890   3900 9100 0     0   0 .80 .49 44 0   0   0 5.0   3.2   260   .65 0   0 .99 .65 50 0   0   0 .0017 .0031 .53 0     0   - -
array-examples/standard_copy9_false-unreach-call_ground.i 0 960   890   4400 9500 0     0   0 .66 .42 42 0   0   0 5.3   2.9   260   .65 0   0 1.0  .67 49 0   0   0 .0064 .0091 .52 0     0   - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 0 960   890   3300 9300 0     0   0 .63 .39 43 0   0   0 5.2   2.8   260   .65 0   0 .98 .63 49 0   0   0 .0017 .0022 .53 0     0   - -
array-examples/standard_init1_false-unreach-call_ground.i 0 960   890   3500 11000 0     0   0 .68 .43 42 0   0   0 5.5   2.9   270   .65 0   0 .99 .64 49 0   0   0 .0022 .0025 .39 0     0   - -
array-examples/standard_init2_false-unreach-call_ground.i 0 960   890   2700 9200 0     0   0 .68 .42 42 0   0   0 5.3   3.3   260   .61 0   0 1.1  .67 49 0   0   0 .0022 .0031 .53 0     0   - -
array-examples/standard_init3_false-unreach-call_ground.i 0 970   890   3700 10000 0     0   0 .66 .39 43 0   0   0 5.5   3.4   270   .65 0   0 .99 .65 49 0   0   0 .0019 .0024 .52 0     0   - -
array-examples/standard_init4_false-unreach-call_ground.i 0 960   890   3300 12000 0     0   0 .66 .41 43 0   0   0 5.4   3.0   270   .65 0   0 1.0  .66 49 0   0   0 .0018 .0023 .52 0     0   - -
array-examples/standard_init5_false-unreach-call_ground.i 0 970   890   4200 9800 0     0   0 .69 .43 43 0   0   0 5.5   2.9   260   .65 0   0 .98 .62 48 0   0   0 .0058 .0074 .53 0     0   - -
array-examples/standard_init6_false-unreach-call_ground.i 0 960   890   2700 7800 0     0   0 .67 .41 42 0   0   0 5.4   3.0   270   .65 0   0 .97 .63 49 0   0   0 .0048 .0061 .52 0     0   - -
array-examples/standard_init7_false-unreach-call_ground.i 0 960   890   3200 9200 0     0   0 .80 .49 42 0   0   0 5.1   3.2   260   .65 0   0 1.0  .65 49 0   0   0 .0056 .0070 .52 0     0   - -
array-examples/standard_init8_false-unreach-call_ground.i 0 970   890   4400 9300 0     0   0 .70 .44 43 0   0   0 5.4   3.4   260   .65 0   0 .99 .66 50 0   0   0 .0045 .0055 .53 0     0   - -
array-examples/standard_init9_false-unreach-call_ground.i 0 960   890   3700 10000 0     0   0 .83 .50 44 0   0   0 5.2   2.9   260   .65 0   0 .97 .63 49 0   0   0 .0048 .0058 .52 0     0   - -
array-examples/standard_minInArray_false-unreach-call_ground.i 0 960   900   4300 9300 0     0   0 .66 .41 44 0   0   0 5.6   3.1   270   .61 0   0 .98 .64 49 0   0   0 .0060 .0076 .53 0     0   - -
array-examples/standard_partition_false-unreach-call_ground.i 0 960   900   4300 10000 0     0   0 .63 .39 43 0   0   0 5.8   3.0   280   .65 0   0 1.0  .67 50 0   0   0 .0021 .0026 .53 0     0   - -
array-examples/standard_running_false-unreach-call.i 0 970   890   4600 8500 0     0   0 .62 .37 42 0   0   0 5.2   2.9   260   .61 0   0 .96 .64 48 0   0   0 .0017 .0022 .52 0     0   - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 2 93   87   1300 1100 0     0   - - - - 0 650    570    7000 0   0   2 9.3   5.3   320   .66 0  
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 970   890   5500 11000 0     0   - - - - 0 .68 .42 44 0   0   0 5.3   2.9   260   .65 0  
array-examples/relax_true-unreach-call.i 0 970   440   6800 8400 .025 0   - - - - 0 .64 .39 42 0   0   0 5.8   3.4   260   .65 0  
array-examples/sanfoundry_02_true-unreach-call_ground.i 0 960   890   4400 10000 0     0   - - - - 0 .67 .42 44 0   0   0 5.4   2.9   270   .65 0  
array-examples/sanfoundry_10_true-unreach-call_ground.i 0 910   880   1000 10000 0     0   - - - - 0 910    880    6300 0   0   0 960     840     1300   .69 0  
array-examples/sanfoundry_24_true-unreach-call_true-termination.i 2 14   4.4 630 110 .016 0   - - - - 2 8.7  5.2  530 0   0   -16 65     43     830   .62 0  
array-examples/sanfoundry_27_true-unreach-call_ground.i 0 960   890   4200 12000 0     0   - - - - 0 .67 .40 43 0   0   0 6.1   3.2   270   .65 0  
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 93   88   1100 1100 0     0   - - - - 2 5.6  3.0  290 0   0   2 6.8   3.9   300   .62 0  
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 960   890   4200 7000 0     0   - - - - 0 .82 .50 43 0   0   0 5.9   3.4   260   .65 0  
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 960   890   4200 9400 0     0   - - - - 0 .62 .39 42 0   0   0 6.3   3.6   260   .65 0  
array-examples/standard_compareModified_true-unreach-call_ground.i 0 970   890   4100 7800 0     0   - - - - 0 .69 .41 43 0   0   0 5.8   3.1   260   .65 0  
array-examples/standard_compare_true-unreach-call_ground.i 0 970   890   4500 9700 0     0   - - - - 0 .68 .41 43 0   0   0 5.3   2.9   270   .65 0  
array-examples/standard_copy1_true-unreach-call_ground.i 0 960   900   4700 13000 0     0   - - - - 0 .72 .43 44 0   0   0 5.1   3.2   270   .65 0  
array-examples/standard_copy2_true-unreach-call_ground.i 0 970   890   4600 9500 0     0   - - - - 0 .79 .48 43 0   0   0 5.2   3.3   260   .65 0  
array-examples/standard_copy3_true-unreach-call_ground.i 0 960   890   4200 10000 0     0   - - - - 0 .63 .38 44 0   0   0 5.2   3.2   270   .61 0  
array-examples/standard_copy4_true-unreach-call_ground.i 0 960   890   4100 10000 0     0   - - - - 0 .70 .44 42 0   0   0 5.5   3.0   260   .61 0  
array-examples/standard_copy5_true-unreach-call_ground.i 0 970   890   4900 8800 0     0   - - - - 0 .80 .47 42 0   0   0 6.1   3.3   270   .65 0  
array-examples/standard_copy6_true-unreach-call_ground.i 0 960   890   3800 11000 0     0   - - - - 0 .60 .36 42 0   0   0 6.0   3.5   270   .61 0  
array-examples/standard_copy7_true-unreach-call_ground.i 0 960   890   4700 9200 0     0   - - - - 0 .66 .39 43 0   0   0 5.0   3.2   250   .65 0  
array-examples/standard_copy8_true-unreach-call_ground.i 0 960   890   4300 9100 0     0   - - - - 0 .78 .47 43 0   0   0 5.4   3.4   270   .61 0  
array-examples/standard_copy9_true-unreach-call_ground.i 0 970   890   4300 9500 0     0   - - - - 0 .66 .41 44 0   0   0 6.3   3.5   260   .61 0  
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 0 960   890   2700 7000 0     0   - - - - 0 .71 .44 42 0   0   0 5.6   3.1   270   .65 0  
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 0 960   890   3400 9700 0     0   - - - - 0 .64 .39 43 0   0   0 6.1   3.7   270   .61 0  
array-examples/standard_copyInitSum_true-unreach-call_ground.i 0 960   890   3900 9900 0     0   - - - - 0 .66 .42 43 0   0   0 5.9   3.5   260   .65 0  
array-examples/standard_copyInit_true-unreach-call_ground.i 0 960   890   2600 8900 0     0   - - - - 0 .64 .39 44 0   0   0 6.0   3.1   270   .65 0  
array-examples/standard_find_true-unreach-call_ground.i 0 970   890   4600 11000 0     0   - - - - 0 .72 .46 44 0   0   0 5.3   2.9   260   .65 0  
array-examples/standard_init1_true-unreach-call_ground.i 0 960   890   2800 8300 0     0   - - - - 0 .65 .40 43 0   0   0 5.8   3.1   260   .65 0  
array-examples/standard_init2_true-unreach-call_ground.i 0 960   890   2800 8900 0     0   - - - - 0 .63 .38 42 0   0   0 5.1   3.2   260   .65 0  
array-examples/standard_init3_true-unreach-call_ground.i 0 960   890   3300 8600 0     0   - - - - 0 .79 .48 42 0   0   0 5.3   3.3   270   .65 0  
array-examples/standard_init4_true-unreach-call_ground.i 0 970   900   4500 10000 0     0   - - - - 0 .88 .54 42 0   0   0 6.3   3.4   270   .65 0  
array-examples/standard_init5_true-unreach-call_ground.i 0 970   890   4200 11000 0     0   - - - - 0 .67 .40 43 0   0   0 5.3   2.9   260   .61 0  
array-examples/standard_init6_true-unreach-call_ground.i 0 960   890   3100 9200 0     0   - - - - 0 .80 .49 43 0   0   0 5.7   3.0   270   .65 0  
array-examples/standard_init7_true-unreach-call_ground.i 0 970   890   4400 10000 0     0   - - - - 0 .79 .49 43 0   0   0 5.3   2.9   270   .65 0  
array-examples/standard_init8_true-unreach-call_ground.i 0 960   890   2700 7800 0     0   - - - - 0 .64 .40 43 0   0   0 5.5   2.9   270   .65 0  
array-examples/standard_init9_true-unreach-call_ground.i 0 960   890   3400 9400 0     0   - - - - 0 .68 .42 42 0   0   0 6.3   3.7   260   .65 0  
array-examples/standard_maxInArray_true-unreach-call_ground.i 0 970   900   5000 7600 0     0   - - - - 0 .64 .39 44 0   0   0 6.4   3.5   270   .65 0  
array-examples/standard_minInArray_true-unreach-call_ground.i 0 960   900   4500 8000 0     0   - - - - 0 .65 .39 44 0   0   0 6.0   3.5   270   .65 0  
array-examples/standard_palindrome_true-unreach-call_ground.i 0 960   890   4200 9200 0     0   - - - - 0 .65 .40 43 0   0   0 5.4   3.4   260   .65 0  
array-examples/standard_partial_init_true-unreach-call_ground.i 0 970   890   4500 12000 0     0   - - - - 0 .62 .38 43 0   0   0 5.9   3.1   270   .61 0  
array-examples/standard_partition_original_true-unreach-call_ground.i 0 970   890   4100 11000 0     0   - - - - 0 .65 .40 43 0   0   0 4.9   3.1   260   .65 0  
array-examples/standard_partition_true-unreach-call_ground.i 0 960   890   4400 12000 0     0   - - - - 0 .63 .38 42 0   0   0 6.0   3.2   260   .65 0  
array-examples/standard_password_true-unreach-call_ground.i 0 960   890   4600 9600 0     0   - - - - 0 .70 .43 43 0   0   0 5.8   3.5   270   .65 0  
array-examples/standard_reverse_true-unreach-call_ground.i 0 970   890   4800 8000 0     0   - - - - 0 .80 .47 43 0   0   0 6.3   3.6   270   .65 0  
array-examples/standard_running_true-unreach-call.i 0 960   890   4600 8100 0     0   - - - - 0 .61 .39 42 0   0   0 5.1   2.8   270   .65 0  
array-examples/standard_sentinel_true-unreach-call_true-termination.i 0 960   480   4100 11000 .016 0   - - - - 0 .60 .36 41 0   0   0 .022 .022 5.7 0    0  
array-examples/standard_seq_init_true-unreach-call_ground.i 0 960   890   2500 8500 0     0   - - - - 0 .80 .49 43 0   0   0 5.6   3.0   270   .65 0  
array-examples/standard_strcmp_true-unreach-call_ground.i 0 960   890   4400 8600 0     0   - - - - 0 .81 .48 44 0   0   0 5.3   2.9   260   .65 0  
array-examples/standard_strcpy_original_true-unreach-call.i 0 970   890   4300 8600 0     0   - - - - 0 .81 .50 43 0   0   0 5.0   3.1   260   .65 0  
array-examples/standard_strcpy_true-unreach-call_ground.i 0 960   890   4100 9500 0     0   - - - - 0 .77 .46 43 0   0   0 7.1   4.1   270   .65 0  
array-examples/standard_two_index_01_true-unreach-call.i 0 970   280   9200 6100 60     0   - - - - 0 .59 .36 42 0   0   0 .021 .021 5.6 0    0  
array-examples/standard_two_index_02_true-unreach-call.i 0 970   890   4100 12000 0     0   - - - - 0 .80 .49 43 0   0   0 5.3   3.3   270   .65 0  
array-examples/standard_two_index_03_true-unreach-call.i 0 960   580   9900 8900 37     0   - - - - 0 .63 .39 44 0   0   0 5.1   3.2   260   .61 0  
array-examples/standard_two_index_04_true-unreach-call.i 0 970   900   4600 8700 0     0   - - - - 0 .85 .52 43 0   0   0 5.4   2.9   270   .65 0  
array-examples/standard_two_index_05_true-unreach-call.i 0 960   890   2800 9500 0     0   - - - - 0 .62 .38 43 0   0   0 5.1   3.3   260   .61 0  
array-examples/standard_two_index_06_true-unreach-call.i 0 960   770   9700 10000 32     0   - - - - 0 .63 .39 42 0   0   0 5.7   3.0   270   .65 0  
array-examples/standard_two_index_07_true-unreach-call.i 0 970   890   3900 7200 0     0   - - - - 0 .65 .39 44 0   0   0 6.2   3.6   260   .65 0  
array-examples/standard_two_index_08_true-unreach-call.i 0 970   890   4000 10000 0     0   - - - - 0 .62 .38 42 0   0   0 5.2   3.2   270   .61 0  
array-examples/standard_two_index_09_true-unreach-call.i 0 970   890   3600 9000 0     0   - - - - 0 .66 .40 42 0   0   0 5.2   3.3   260   .61 0  
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 0 960   460   6100 7400 .016 0   - - - - 0 .76 .47 43 0   0   0 5.5   3.0   260   .65 0  
array-examples/standard_vector_difference_true-unreach-call_ground.i 0 960   890   4100 11000 0     0   - - - - 0 .80 .48 42 0   0   0 6.3   3.4   260   .65 0  
array-examples/standard_sentinel_true-unreach-call.i.v+cfa-reducer.c 0 960   460   4300 10000 .016 0   - - - - 0 .66 .40 43 0   0   0 5.2   3.3   260   .61 0  
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i 0 970   890   4000 9700 0     0   0 .76 .46 43 0   0   0 5.8   3.0   270   .61 0   0 .98 .62 49 0   0   0 .0018 .0024 .53 0     0   - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 0 960   890   3700 7700 0     0   0 .65 .40 44 0   0   0 5.2   2.9   260   .65 0   0 1.0  .70 49 0   0   0 .0015 .0019 .53 0     0   - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i 0 970   890   4700 12000 0     0   0 .65 .40 43 0   0   0 5.3   2.9   270   .61 0   0 .98 .65 49 0   0   0 .0052 .0062 .52 0     0   - -
array-industry-pattern/array_range_init_false-unreach-call.i 0 960   890   3800 10000 0     0   0 .76 .46 42 0   0   0 5.3   2.9   270   .65 0   0 1.0  .64 49 0   0   0 .0053 .0068 .53 0     0   - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i 0 970   890   4000 9500 0     0   0 .69 .42 44 0   0   0 5.8   3.6   260   .65 0   0 .99 .66 48 0   0   0 .0049 .0054 .40 0     0   - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 970   890   5700 9100 0     0   0 .62 .38 42 0   0   0 5.2   3.3   260   .65 0   0 .99 .65 49 0   0   0 .0055 .0068 .52 0     0   - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i 0 970   890   4800 9800 0     0   - - - - 0 .72 .44 42 0   0   0 5.4   2.9   260   .65 0  
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i 0 970   890   4200 8400 0     0   - - - - 0 .69 .42 42 0   0   0 5.2   2.8   260   .65 0  
array-industry-pattern/array_of_struct_break_true-unreach-call.i 0 970   460   6800 7300 .016 0   - - - - 0 .81 .50 43 0   0   0 5.0   2.8   270   .65 0  
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 970   890   4800 8400 0     0   - - - - 0 .81 .50 44 0   0   0 5.7   3.1   270   .65 0  
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 0 960   890   4800 7200 0     0   - - - - 0 .78 .48 42 0   0   0 5.3   3.3   260   .65 0  
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 960   890   4000 8800 0     0   - - - - 0 .78 .48 43 0   0   0 5.3   3.4   260   .61 0  
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 960   890   4000 8900 0     0   - - - - 0 .80 .51 42 0   0   0 5.2   2.9   260   .65 0  
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 0 960   890   3900 10000 0     0   - - - - 0 .66 .40 44 0   0   0 4.8   2.7   260   .65 0  
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 0 960   890   3700 7900 0     0   - - - - 0 .67 .41 43 0   0   0 6.2   3.3   270   .65 0  
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 0 970   890   4900 7300 0     0   - - - - 0 .75 .46 43 0   0   0 6.1   3.3   260   .65 0  
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i 0 960   480   5500 7700 .016 0   - - - - 0 .64 .39 42 0   0   0 5.4   3.3   270   .61 0  
reducercommutativity/rangesum05_false-unreach-call_true-termination.i 0 380   360   2300 2800 .098 0   0 .66 .40 41 0   0   0 .022 .023 5.7 0    0   0 1.0  .64 49 0   0   0 .0036 .0056 .53 0     0   - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i 0 460   440   2500 2600 .16  0   0 .76 .46 40 0   0   0 .021 .022 5.6 0    0   0 .96 .63 48 0   0   0 .0048 .0059 .53 0     0   - -
reducercommutativity/rangesum20_false-unreach-call.i 0 900   880   3500 6400 .30  0   0 92    86    1500 0   0   0 97     70     910   .64 0   0 1.1  .68 51 0   0   0 .082  .081  11    0     0   - -
reducercommutativity/rangesum40_false-unreach-call.i 0 900   880   5100 6900 .57  0   0 92    85    1400 0   0   0 98     65     1100   .64 0   0 1.1  .70 50 0   0   0 .073  .073  11    0     0   - -
reducercommutativity/rangesum60_false-unreach-call.i 0 910   870   5800 6700 .85  0   0 92    84    1400 0   0   0 97     67     1100   1.7  0   0 1.1  .70 51 0   0   0 .070  .070  12    0     0   - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i 0 32   8.4 1400 220 .041 0   0 .61 .39 41 0   0   0 .049 .052 5.5 0    0   0 .96 .61 47 0   0   0 .0053 .0064 .53 0     0   - -
reducercommutativity/avg05_true-unreach-call_true-termination.i 0 900   890   2200 7500 .066 0   - - - - 0 600    590    2300 0   0   0 960     930     5300   1.8  0  
reducercommutativity/avg10_true-unreach-call_true-termination.i 0 900   890   3700 10000 .11  0   - - - - 0 900    890    2300 0   0   0 960     920     1900   1.2  0  
reducercommutativity/avg20_true-unreach-call.i 0 900   880   3800 6300 .20  0   - - - - 0 900    890    2800 0   0   0 960     830     1600   1.2  0  
reducercommutativity/avg40_true-unreach-call.i 0 900   880   6100 6700 .38  0   - - - - 0 900    890    4000 0   0   0 960     850     920   1.6  0  
reducercommutativity/avg60_true-unreach-call.i 0 900   880   5100 7300 .55  0   - - - - 0 900    890    4200 0   0   0 960     930     730   .72 0  
reducercommutativity/avg_true-unreach-call_true-termination.i 0 26   8.2 1200 210 .025 0   - - - - 0 .59 .38 40 0   0   0 .023 .024 5.6 0    0  
reducercommutativity/max05_true-unreach-call_true-termination.i 2 220   210   1500 1700 .082 0   - - - - 0 110    110    1000 0   0   0 960     910     1400   .82 0  
reducercommutativity/max10_true-unreach-call_true-termination.i 0 900   890   2100 6700 .14  0   - - - - 0 900    890    2200 0   0   0 960     840     3300   .64 0  
reducercommutativity/max20_true-unreach-call.i 0 900   880   2300 7900 .26  0   - - - - 0 900    890    1900 0   0   0 960     820     1000   .63 0  
reducercommutativity/max40_true-unreach-call.i 0 900   880   2700 8100 .50  0   - - - - 0 900    890    1600 0   0   0 960     850     1200   .72 0  
reducercommutativity/max60_true-unreach-call.i 0 900   870   3000 7600 .73  0   - - - - 0 900    890    1600 0   0   0 960     930     710   .63 0  
reducercommutativity/max_true-unreach-call_true-termination.i 0 960   480   5400 7300 .025 0   - - - - 0 .82 .49 43 0   0   0 5.4   3.0   260   .65 0  
reducercommutativity/sep05_true-unreach-call_true-termination.i 2 290   250   2500 2800 .090 0   -