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   - - - - 0 110    98    1300 0   0   0 960     910     3400   1.5  0  
reducercommutativity/sep10_true-unreach-call.i 0 80   37   2500 820 .16  0   - - - - 0 .61 .37 40 0   0   0 .022 .022 5.5 0    0  
reducercommutativity/sep20_true-unreach-call.i 0 910   510   4800 8900 .15  0   - - - - 0 900    890    1200 0   0   0 960     830     6500   .64 0  
reducercommutativity/sep40_true-unreach-call.i 0 910   890   3500 9100 0     0   - - - - 0 900    890    1300 0   0   0 960     910     1300   1.6  0  
reducercommutativity/sep60_true-unreach-call.i 0 920   870   4400 11000 0     0   - - - - 0 900    890    1300 0   0   0 960     920     1000   1.2  0  
reducercommutativity/sep_true-unreach-call_true-termination.i 0 940   460   5000 9600 .029 0   - - - - 0 900    870    4400 0   0   0 14     7.8   300   .75 0  
reducercommutativity/sum05_true-unreach-call_true-termination.i 0 900   890   1600 12000 .066 0   - - - - 0 160    160    1200 0   0   2 590     560     1300   .62 0  
reducercommutativity/sum10_true-unreach-call_true-termination.i 0 900   890   3600 6600 .11  0   - - - - 0 900    890    2700 0   0   0 960     900     1400   1.5  0  
reducercommutativity/sum20_true-unreach-call.i 0 900   880   4700 6800 .20  0   - - - - 0 900    890    2300 0   0   0 960     840     1400   .72 0  
reducercommutativity/sum40_true-unreach-call.i 0 910   880   5600 8200 .38  0   - - - - 0 900    890    4100 0   0   0 960     860     900   .97 0  
reducercommutativity/sum60_true-unreach-call.i 0 910   880   6300 7700 .55  0   - - - - 0 900    890    3200 0   0   0 960     920     890   .63 0  
reducercommutativity/sum_true-unreach-call_true-termination.i 0 970   480   4500 9500 .025 0   - - - - 0 .83 .51 42 0   0   0 6.1   3.3   270   .65 0  
array-tiling/mlceu_false-unreach-call.i 0 960   480   5600 9300 .016 0   0 .68 .41 43 0   0   0 5.1   3.2   270   .65 0   0 1.1  .67 50 0   0   0 .0051 .0063 .53 0     0   - -
array-tiling/skippedu_false-unreach-call.i 1 6.4 2.2 320 60 .041 0   1 5.3  2.9  260 0   0   1 12     6.9   380   .62 0   0 3.7  2.1  240 0   0   -32 .57   .57   21    .053 0   - -
array-tiling/mbpr2_true-unreach-call.i 0 970   470   6000 7500 .025 0   - - - - 0 .68 .41 43 0   0   0 6.0   3.3   260   .65 0  
array-tiling/mbpr3_true-unreach-call.i 0 960   450   6700 7200 .025 0   - - - - 0 15    8.3  450 0   0   0 15     8.4   300   .75 0  
array-tiling/mbpr4_true-unreach-call.i 0 920   400   7500 9100 .033 0   - - - - 0 910    900    2100 0   0   0 13     7.5   290   .75 0  
array-tiling/mbpr5_true-unreach-call.i 0 930   410   7200 9500 .033 0   - - - - 0 910    900    2100 0   0   0 16     8.9   300   .75 0  
array-tiling/nr2_true-unreach-call.i 0 970   470   6700 10000 .025 0   - - - - 0 .90 .53 43 0   0   0 5.8   3.1   270   .65 0  
array-tiling/nr3_true-unreach-call.i 0 960   460   6200 7800 .025 0   - - - - 0 .63 .40 44 0   0   0 5.1   2.8   260   .65 0  
array-tiling/nr4_true-unreach-call.i 0 970   460   6600 8500 .025 0   - - - - 0 .70 .43 44 0   0   0 5.4   2.9   270   .65 0  
array-tiling/nr5_true-unreach-call.i 0 960   460   6100 11000 .025 0   - - - - 0 .69 .44 43 0   0   0 7.1   4.0   270   .65 0  
array-tiling/pnr2_true-unreach-call.i 0 960   480   3700 9700 .016 0   - - - - 0 .76 .46 43 0   0   0 6.1   3.3   260   .65 0  
array-tiling/pnr3_true-unreach-call.i 0 960   450   6900 7100 .016 0   - - - - 0 .65 .40 41 0   0   0 .021 .022 5.6 0    0  
array-tiling/pnr4_true-unreach-call.i 0 960   480   3500 10000 .016 0   - - - - 0 .77 .46 43 0   0   0 5.2   2.9   250   .65 0  
array-tiling/pnr5_true-unreach-call.i 0 960   450   6600 9300 .016 0   - - - - 0 .59 .37 42 0   0   0 .025 .026 5.6 0    0  
array-tiling/poly1_true-unreach-call.i 0 960   470   5300 6100 .016 0   - - - - 0 .82 .50 43 0   0   0 6.0   3.6   270   .65 0  
array-tiling/poly2_true-unreach-call.i 0 970   460   5100 6600 .016 0   - - - - 0 .79 .48 43 0   0   0 5.0   2.7   270   .61 0  
array-tiling/pr2_true-unreach-call.i 0 960   460   3800 6800 .025 0   - - - - 0 .63 .38 42 0   0   0 5.4   3.3   260   .65 0  
array-tiling/pr3_true-unreach-call.i 0 960   470   3800 6400 .025 0   - - - - 0 .81 .49 44 0   0   0 5.4   2.9   270   .65 0  
array-tiling/pr4_true-unreach-call.i 0 960   470   3800 7000 .025 0   - - - - 0 .78 .47 43 0   0   0 5.3   3.2   260   .65 0  
array-tiling/pr5_true-unreach-call.i 0 960   480   3300 8900 .025 0   - - - - 0 .80 .49 43 0   0   0 4.9   3.1   260   .65 0  
array-tiling/revcpyswp2_true-unreach-call.i 0 960   480   3400 6400 .025 0   - - - - 0 .65 .40 44 0   0   0 5.5   3.0   270   .65 0  
array-tiling/rew_true-unreach-call.i 0 960   480   4100 7200 .016 0   - - - - 0 .65 .40 42 0   0   0 5.8   3.4   260   .65 0  
array-tiling/rewnif_true-unreach-call.i 0 960   480   4200 7700 .016 0   - - - - 0 .72 .44 42 0   0   0 5.1   3.2   260   .65 0  
array-tiling/rewnifrev2_true-unreach-call.i 0 960   480   4100 9500 .016 0   - - - - 0 .66 .41 41 0   0   0 .024 .024 5.6 0    0  
array-tiling/rewnifrev_true-unreach-call.i 0 960   480   3900 7200 .016 0   - - - - 0 .68 .42 42 0   0   0 5.1   2.8   260   .61 0  
array-tiling/rewrev_true-unreach-call.i 0 960   480   4100 7100 .016 0   - - - - 0 .76 .47 41 0   0   0 .020 .021 5.6 0    0  
array-tiling/skipped_true-unreach-call.i 0 960   470   3700 10000 .016 0   - - - - 0 .69 .42 42 0   0   0 5.3   2.9   270   .65 0  
array-tiling/tcpy_true-unreach-call.i 0 960   470   3700 9700 .016 0   - - - - 0 .85 .52 43 0   0   0 5.2   2.8   260   .61 0  
array-programs/copysome1_false-unreach-call.i 0 970   890   4600 11000 0     0   0 .83 .50 43 0   0   0 5.5   3.5   260   .61 0   0 .99 .65 48 0   0   0 .0055 .0073 .54 0     0   - -
array-programs/copysome2_false-unreach-call.i 0 960   890   4100 10000 0     0   0 .79 .48 42 0   0   0 5.1   3.2   260   .61 0   0 .95 .61 48 0   0   0 .0017 .0027 .54 0     0   - -
array-programs/copysome1_true-unreach-call.i 0 960   890   5000 9300 0     0   - - - - 0 .64 .40 42 0   0   0 5.3   2.9   270   .65 0  
array-programs/copysome2_true-unreach-call.i 0 970   890   5100 9200 0     0   - - - - 0 .65 .39 42 0   0   0 5.2   3.2   270   .65 0  
array-crafted/bAnd1_true-unreach-call.i 0 900   870   6500 8100 .90  0   - - - - 0 900    890    4500 0   0   0 960     930     720   .63 0  
array-crafted/bAnd2_true-unreach-call.i 0 910   760   5900 11000 13     0   - - - - 0 910    880    5000 0   0   0 13     7.8   290   .75 0  
array-crafted/bAnd3_true-unreach-call.i 0 960   890   5400 9900 0     0   - - - - 0 .68 .42 42 0   0   0 5.5   3.0   270   .65 0  
array-crafted/bAnd4_true-unreach-call.i 0 960   890   4000 8900 0     0   - - - - 0 .66 .42 42 0   0   0 5.3   3.3   260   .65 0  
array-crafted/bAnd5_true-unreach-call.i 0 960   480   4600 7200 .025 0   - - - - 0 .79 .48 43 0   0   0 5.5   3.0   270   .61 0  
array-crafted/bor1_true-unreach-call.i 0 910   870   7600 8100 .90  0   - - - - 0 900    890    4400 0   0   0 960     920     830   .63 0  
array-crafted/bor2_true-unreach-call.i 0 910   770   5900 9700 12     0   - - - - 0 910    890    5600 0   0   0 12     7.0   290   .75 0  
array-crafted/bor3_true-unreach-call.i 0 970   900   4800 10000 0     0   - - - - 0 .78 .48 42 0   0   0 6.1   3.3   260   .65 0  
array-crafted/bor4_true-unreach-call.i 0 960   890   4300 10000 0     0   - - - - 0 .66 .41 43 0   0   0 5.5   3.3   260   .65 0  
array-crafted/bor5_true-unreach-call.i 0 960   480   4700 7600 .025 0   - - - - 0 .88 .54 45 0   0   0 5.3   3.2   260   .65 0  
array-crafted/mapavg1_true-unreach-call.i 0 900   870   5300 7500 .91  0   - - - - 0 900    890    4000 0   0   0 960     930     690   1.9  0  
array-crafted/mapavg2_true-unreach-call.i 0 920   730   7800 8500 13     0   - - - - 0 910    880    5900 0   0   0 15     8.1   290   .75 0  
array-crafted/mapavg3_true-unreach-call.i 0 960   890   4600 11000 0     0   - - - - 0 .66 .41 43 0   0   0 6.0   3.2   270   .65 0  
array-crafted/mapavg4_true-unreach-call.i 0 960   900   3700 11000 0     0   - - - - 0 .62 .38 42 0   0   0 5.7   3.4   260   .65 0  
array-crafted/mapavg5_true-unreach-call.i 0 11   3.1 660 92 .025 0   - - - - 0 .60 .38 40 0   0   0 .021 .022 5.7 0    0  
array-crafted/mapsum1_true-unreach-call.i 0 910   870   6500 9100 .91  0   - - - - 0 900    890    4100 0   0   0 960     920     910   1.6  0  
array-crafted/mapsum2_true-unreach-call.i 0 910   690   6000 9900 13     0   - - - - 0 910    880    5800 0   0   0 14     7.3   300   .75 0  
array-crafted/mapsum3_true-unreach-call.i 0 960   890   5500 10000 0     0   - - - - 0 .61 .38 43 0   0   0 5.4   3.0   260   .65 0  
array-crafted/mapsum4_true-unreach-call.i 0 970   890   5000 11000 0     0   - - - - 0 .64 .39 43 0   0   0 5.7   3.0   270   .65 0  
array-crafted/mapsum5_true-unreach-call.i 0 960   480   3900 9800 .025 0   - - - - 0 .82 .50 43 0   0   0 5.7   3.1   260   .65 0  
array-crafted/xor1_true-unreach-call.i 0 910   870   7400 9900 .90  0   - - - - 0 910    890    5300 0   0   0 960     930     810   1.6  0  
array-crafted/xor2_true-unreach-call.i 0 910   720   7800 11000 12     0   - - - - 0 910    880    5800 0   0   0 12     6.9   290   .75 0  
array-crafted/xor3_true-unreach-call.i 0 960   900   4100 13000 0     0   - - - - 0 .60 .37 43 0   0   0 5.8   3.1   270   .65 0  
array-crafted/xor4_true-unreach-call.i 0 960   890   2900 8900 0     0   - - - - 0 .73 .44 44 0   0   0 5.8   3.1   270   .65 0  
array-crafted/xor5_true-unreach-call.i 0 970   480   5000 7900 .025 0   - - - - 0 .63 .40 43 0   0   0 5.4   3.3   270   .65 0  
array-crafted/zero_sum1_true-unreach-call.c 0 960   480   3700 9400 .016 0   - - - - 0 .80 .48 42 0   0   0 .024 .024 5.6 0    0  
array-crafted/zero_sum2_true-unreach-call.c 0 960   450   4200 9400 .025 0   - - - - 0 .81 .48 44 0   0   0 5.6   3.4   270   .65 0  
array-crafted/zero_sum3_true-unreach-call.c 0 960   450   5700 8400 .025 0   - - - - 0 .83 .51 43 0   0   0 5.1   2.9   250   .65 0  
array-crafted/zero_sum4_true-unreach-call.c 0 970   420   7700 8900 .033 0   - - - - 0 .72 .44 43 0   0   0 6.0   3.5   270   .32 0  
array-crafted/zero_sum5_true-unreach-call.c 0 970   400   8200 8800 .033 0   - - - - 0 .62 .38 42 0   0   0 5.2   2.9   260   .61 0  
array-crafted/zero_sum_const1_true-unreach-call.c 0 960   480   5600 7900 .025 0   - - - - 0 .81 .49 43 0   0   0 5.3   2.8   270   .65 0  
array-crafted/zero_sum_const2_true-unreach-call.c 0 960   460   6200 9400 .025 0   - - - - 0 .76 .46 42 0   0   0 5.6   3.1   250   .65 0  
array-crafted/zero_sum_const3_true-unreach-call.c 0 970   410   7700 9900 .029 0   - - - - 0 .63 .39 41 0   0   0 .022 .023 5.6 0    0  
array-crafted/zero_sum_const4_true-unreach-call.c 0 960   400   7600 8400 .033 0   - - - - 0 .83 .50 43 0   0   0 5.2   3.3   260   .61 0  
array-crafted/zero_sum_const5_true-unreach-call.c 0 950   390   7200 8900 .033 0   - - - - 0 900    850    4100 0   0   0 14     8.9   300   .75 0  
array-crafted/zero_sum_const_m2_true-unreach-call.c 0 970   430   7000 7500 .025 0   - - - - 0 .64 .40 42 0   0   0 5.4   2.9   270   .65 0  
array-crafted/zero_sum_const_m3_true-unreach-call.c 0 960   420   7300 9100 .029 0   - - - - 0 .69 .41 43 0   0   0 5.8   3.1   260   .65 0  
array-crafted/zero_sum_const_m4_true-unreach-call.c 0 960   390   8400 10000 .033 0   - - - - 0 .77 .47 42 0   0   0 5.3   2.8   260   .65 0  
array-crafted/zero_sum_const_m5_true-unreach-call.c 0 960   390   8200 8700 .033 0   - - - - 0 .78 .49 42 0   0   0 5.4   2.9   270   .65 0  
array-crafted/zero_sum_m2_true-unreach-call.c 0 970   460   4300 8100 .025 0   - - - - 0 .60 .37 43 0   0   0 5.3   2.9   270   .65 0  
array-crafted/zero_sum_m3_true-unreach-call.c 0 960   460   6500 7900 .025 0   - - - - 0 .66 .40 43 0   0   0 5.5   3.1   270   .65 0  
array-crafted/zero_sum_m4_true-unreach-call.c 0 970   430   6900 8500 .033 0   - - - - 0 .82 .49 43 0   0   0 5.2   2.8   270   .65 0  
array-crafted/zero_sum_m5_true-unreach-call.c 0 970   410   7500 8500 .033 0   - - - - 0 .63 .40 43 0   0   0 5.6   3.0   270   .65 0  
array-multidimensional/add-2-n-u_true-unreach-call.i 0 910   870   3400 10000 0     0   - - - - 0 410    390    7000 0   0   0 960     950     2100   .64 0  
array-multidimensional/add-3-n-u_true-unreach-call.i 0 910   870   3700 9900 0     0   - - - - 0 570    510    7000 0   0   0 960     950     510   .63 0  
array-multidimensional/copy-2-u_true-unreach-call.i 0 910   860   4300 11000 0     0   - - - - 0 810    780    7000 0   0   0 960     950     1200   1.6  0  
array-multidimensional/copy-3-n-u_true-unreach-call.i 0 910   870   3900 8200 0     0   - - - - 0 540    480    7000 0   0   0 960     950     730   .63 0  
array-multidimensional/copy-partial-2-n-u_true-unreach-call.i 0 910   890   4100 9300 0     0   - - - - 0 550    520    7000 0   0   0 960     950     1200   .65 0  
array-multidimensional/copy-partial-3-u_true-unreach-call.i 0 910   890   4000 8800 0     0   - - - - 2 15    8.1  490 0   0   2 12     6.9   400   .62 0  
array-multidimensional/diff-2-n-u_true-unreach-call.i 0 910   790   6400 10000 0     0   - - - - 0 550    510    7000 0   0   0 960     950     720   .98 0  
array-multidimensional/diff-3-n-u_true-unreach-call.i 0 910   860   4400 9100 0     0   - - - - 0 480    420    7000 0   0   0 960     950     510   1.3  0  
array-multidimensional/init-2-n-u_true-unreach-call.i 0 910   890   4000 8200 0     0   - - - - 0 900    880    6900 0   0   0 960     950     930   2.1  0  
array-multidimensional/init-3-u_true-unreach-call.i 0 910   890   4100 12000 0     0   - - - - 0 720    690    7000 0   0   0 960     950     620   1.7  0  
array-multidimensional/init-4-n-u_true-unreach-call.i 0 920   890   4200 7200 0     0   - - - - 0 550    520    7000 0   0   0 960     950     680   .63 0  
array-multidimensional/init-non-constant-2-n-u_true-unreach-call.i 0 960   480   6300 7100 .025 0   - - - - 0 .63 .39 44 0   0   0 5.8   3.1   270   .65 0  
array-multidimensional/init-non-constant-3-u_true-unreach-call.i 0 910   890   3500 8900 0     0   - - - - 0 510    480    7000 0   0   0 960     950     1100   .79 0  
array-multidimensional/max-2-u_true-unreach-call.i 0 910   890   4000 10000 0     0   - - - - 0 900    880    4300 0   0   0 960     950     1100   .63 0  
array-multidimensional/max-3-n-u_true-unreach-call.i 0 910   870   4000 11000 0     0   - - - - 0 900    850    4800 0   0   0 960     940     2000   .68 0  
array-multidimensional/min-2-u_true-unreach-call.i 0 910   890   4200 11000 0     0   - - - - 0 900    870    5500 0   0   0 960     950     1000   .70 0  
array-multidimensional/min-3-n-u_true-unreach-call.i 0 910   870   3900 9500 0     0   - - - - 0 520    470    7000 0   0   0 960     940     1800   .70 0  
array-multidimensional/rev-2-n-u_true-unreach-call.i 0 910   870   4000 11000 0     0   - - - - 0 700    670    7000 0   0   0 250     200     7000   .63 0  
array-multidimensional/rev-3-u_true-unreach-call.i 0 910   860   3800 10000 0     0   - - - - 0 550    480    7000 0   0   0 960     950     610   .95 0  
array-multidimensional/transpose-u_true-unreach-call.i 0 910   860   4000 11000 0     0   - - - - 0 660    630    7000 0   0   0 16     8.8   300   .71 0  
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)
total 231 11 210000   170000   1000000 2000000 200     0   44 1 310   270   6300 0   0   44 1 500 320   13000 27    0   44 0 47 30 2400 0   0   44 -32 .95 .99 75 .053 0   187 6 41000 39000 250000 0   0   187 -8 40000 38000 100000 130    0  
    correct results 6 11 720   640   7400 6800 .23  0   1 1 5.3 2.9 260 0   0   1 1 12 6.9 380 .62 0   0 0 3 6 30 16 1300 0   0   4 8 620 570 2300 2.5  0  
        correct true 5 10 710   640   7000 6700 .19  0   0 0 0 0 3 6 30 16 1300 0   0   4 8 620 570 2300 2.5  0  
        correct false 1 1 6.4 2.2 320 60 .041 0   1 1 5.3 2.9 260 0   0   1 1 12 6.9 380 .62 0   0 0 0 0
    incorrect results 0 0 0 0 1 -32 .57 .57 21 .053 0   0 1 -16 65 43 830 .62 0  
        incorrect true 0 0 0 0 1 -32 .57 .57 21 .053 0   0 0
        incorrect false 0 0 0 0 0 0 1 -16 65 43 830 .62 0  
score (231 tasks, max score: 418) 11 1 1 0 -32 6 -8
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