Tool VeriAbs 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* [apollon020; apollon077; apollon078; apollon084; apollon149; apollon164] apollon* [apollon037; apollon065; apollon077; apollon078; apollon155; apollon159] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 18:04:04 CET 2017-12-03 04:46:33 CET 2017-12-03 06:08:30 CET 2017-12-03 06:21:09 CET 2017-12-03 06:27:12 CET 2017-12-03 03:55:53 CET 2017-12-03 04:55:47 CET
Run set veriabs.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Arrays
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
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 0 900   9100 10000 0 .55 41 0 .021 4.8 0 .84 47 0 .0038 .32 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 780   10000 11000 0 .57 41 0 .019 4.8 0 .82 47 0 .0011 .27 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 780   10000 11000 0 .40 41 0 .017 4.8 0 .66 50 0 .0012 .30 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 690   9400 7500 0 .55 41 0 .018 4.8 0 .84 47 0 .0042 .26 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 690   9600 7800 0 .60 41 0 .019 4.8 0 .87 49 0 .0017 .28 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i 0 900   8100 9900 0 .55 41 0 .023 4.9 0 .63 49 0 .0012 .30 - -
array-examples/standard_copy1_false-unreach-call_ground.i 0 380   2500 5400 0 92    4000 0 61     7000   0 64    3700 0 96      130    - -
array-examples/standard_copy2_false-unreach-call_ground.i 0 500   3500 7400 0 93    4400 0 84     7000   0 59    4400 0 96      150    - -
array-examples/standard_copy3_false-unreach-call_ground.i 0 620   4500 9300 0 97    4500 0 81     7000   0 70    4700 0 96      160    - -
array-examples/standard_copy4_false-unreach-call_ground.i 1 700   5400 10000 0 91    2000 -32 4.8   230   0 2.9  210 1 .57   18    - -
array-examples/standard_copy5_false-unreach-call_ground.i 1 700   6300 10000 0 91    2000 -32 4.8   230   0 2.9  210 1 .70   18    - -
array-examples/standard_copy6_false-unreach-call_ground.i 1 700   7200 8700 0 91    2100 -32 5.0   230   0 2.1  210 1 .59   18    - -
array-examples/standard_copy7_false-unreach-call_ground.i 1 700   8200 10000 0 91    2100 -32 5.2   230   0 3.0  210 1 .58   18    - -
array-examples/standard_copy8_false-unreach-call_ground.i 1 700   9100 8000 0 91    2100 -32 5.3   230   0 2.2  210 1 .58   18    - -
array-examples/standard_copy9_false-unreach-call_ground.i 1 700   10000 9900 0 91    2100 -32 3.5   230   0 2.9  210 1 .62   18    - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 0 390   2500 5600 0 92    3600 0 98     6400   0 47    3600 0 96      130    - -
array-examples/standard_init1_false-unreach-call_ground.i 0 140   1000 1800 0 92    2200 0 97     6700   0 22    1800 0 96      100    - -
array-examples/standard_init2_false-unreach-call_ground.i 0 270   1500 3500 0 92    2900 0 97     6700   0 42    2800 0 96      110    - -
array-examples/standard_init3_false-unreach-call_ground.i 0 390   2000 5500 0 92    3600 0 97     6800   0 64    3800 0 96      130    - -
array-examples/standard_init4_false-unreach-call_ground.i 0 500   2500 6500 0 92    4500 0 98     6900   0 64    4400 0 96      130    - -
array-examples/standard_init5_false-unreach-call_ground.i 0 620   3000 9600 0 97    4600 0 97     6900   0 71    4500 0 96      150    - -
array-examples/standard_init6_false-unreach-call_ground.i 1 710   3500 9700 0 92    850 -32 4.9   220   0 2.8  210 1 .58   18    - -
array-examples/standard_init7_false-unreach-call_ground.i 1 710   3900 11000 0 92    850 -32 5.0   220   0 2.0  210 1 .58   18    - -
array-examples/standard_init8_false-unreach-call_ground.i 1 710   4400 8400 0 91    910 -32 6.6   250   0 3.1  210 1 .58   18    - -
array-examples/standard_init9_false-unreach-call_ground.i 1 710   4800 8800 0 92    850 -32 5.0   220   0 2.9  210 1 .61   18    - -
array-examples/standard_minInArray_false-unreach-call_ground.i 1 4.4 510 35 0 92    1900 0 97     1100   0 2.9  210 1 .58   18    - -
array-examples/standard_partition_false-unreach-call_ground.i 0 900   8100 11000 0 .57 42 0 .020 4.9 0 .67 49 0 .0012 .32 - -
array-examples/standard_running_false-unreach-call.i 0 900   9200 10000 0 .43 44 0 .017 4.8 0 .88 50 0 .0021 .32 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 0 650   8700 6600 - - - - 0 .64 43 0 .021 5.0
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 900   9200 9200 - - - - 0 .60 44 0 .018 4.9
array-examples/relax_true-unreach-call.i 0 900   9100 9300 - - - - 0 .55 41 0 .020 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i 2 8.9 220 90 - - - - 0 900    2400 0 960     4900  
array-examples/sanfoundry_10_true-unreach-call_ground.i 2 16   220 110 - - - - 0 910    6400 0 960     1100  
array-examples/sanfoundry_24_true-unreach-call_true-termination.i 2 15   210 94 - - - - 2 6.8  490 2 8.4   270  
array-examples/sanfoundry_27_true-unreach-call_ground.i 2 3.9 220 28 - - - - 0 900    2400 0 960     2800  
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 3.3 220 26 - - - - 2 3.4  260 2 4.8   220  
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 780   10000 9800 - - - - 0 .52 44 0 .021 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 690   9200 9000 - - - - 0 .54 43 0 .018 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i 2 3.6 220 24 - - - - 0 900    4400 0 960     2500  
array-examples/standard_compare_true-unreach-call_ground.i 2 3.5 220 20 - - - - 0 900    6400 0 960     4800  
array-examples/standard_copy1_true-unreach-call_ground.i 2 3.6 220 23 - - - - 0 900    5200 0 960     4800  
array-examples/standard_copy2_true-unreach-call_ground.i 2 3.6 230 23 - - - - 0 690    7000 0 960     4800  
array-examples/standard_copy3_true-unreach-call_ground.i 2 3.8 220 24 - - - - 0 910    5800 0 960     4800  
array-examples/standard_copy4_true-unreach-call_ground.i 2 3.5 220 28 - - - - 0 900    6300 0 960     4900  
array-examples/standard_copy5_true-unreach-call_ground.i 2 3.6 220 29 - - - - 0 900    6400 0 960     4900  
array-examples/standard_copy6_true-unreach-call_ground.i 2 3.5 220 26 - - - - 0 900    6100 0 960     4900  
array-examples/standard_copy7_true-unreach-call_ground.i 2 3.9 220 26 - - - - 0 840    7000 0 960     4900  
array-examples/standard_copy8_true-unreach-call_ground.i 2 3.7 230 24 - - - - 0 870    7000 0 960     5100  
array-examples/standard_copy9_true-unreach-call_ground.i 2 3.7 230 25 - - - - 0 900    6800 0 960     5000  
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 2 16   220 120 - - - - 0 900    2900 0 960     4900  
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 2 3.4 220 24 - - - - 0 900    4100 0 960     5000  
array-examples/standard_copyInitSum_true-unreach-call_ground.i 2 31   220 310 - - - - 0 900    3400 0 960     4800  
array-examples/standard_copyInit_true-unreach-call_ground.i 2 16   220 99 - - - - 0 900    5000 0 960     4800  
array-examples/standard_find_true-unreach-call_ground.i 2 16   220 100 - - - - 0 900    4600 0 960     4800  
array-examples/standard_init1_true-unreach-call_ground.i 2 15   220 92 - - - - 0 900    4800 0 960     2100  
array-examples/standard_init2_true-unreach-call_ground.i 2 15   220 120 - - - - 0 900    4500 0 960     3300  
array-examples/standard_init3_true-unreach-call_ground.i 2 16   220 100 - - - - 0 900    5200 0 960     4900  
array-examples/standard_init4_true-unreach-call_ground.i 2 16   220 100 - - - - 0 900    4500 0 960     5200  
array-examples/standard_init5_true-unreach-call_ground.i 2 16   220 100 - - - - 0 900    4600 0 960     5200  
array-examples/standard_init6_true-unreach-call_ground.i 2 15   220 120 - - - - 0 900    4900 0 960     5500  
array-examples/standard_init7_true-unreach-call_ground.i 2 16   210 130 - - - - 0 900    4500 0 960     5500  
array-examples/standard_init8_true-unreach-call_ground.i 2 17   220 110 - - - - 0 900    4800 0 960     4900  
array-examples/standard_init9_true-unreach-call_ground.i 2 16   210 130 - - - - 0 900    5500 0 960     5600  
array-examples/standard_maxInArray_true-unreach-call_ground.i 2 4.2 220 27 - - - - 0 900    2500 0 960     2600  
array-examples/standard_minInArray_true-unreach-call_ground.i 2 4.2 220 26 - - - - 0 900    4600 0 960     2500  
array-examples/standard_palindrome_true-unreach-call_ground.i 2 19   220 160 - - - - 0 900    5200 0 960     1600  
array-examples/standard_partial_init_true-unreach-call_ground.i 2 15   210 100 - - - - 0 900    2700 0 960     4000  
array-examples/standard_partition_original_true-unreach-call_ground.i 2 16   220 120 - - - - 0 900    3800 0 85     7000  
array-examples/standard_partition_true-unreach-call_ground.i 2 16   220 120 - - - - 0 900    5600 0 960     5300  
array-examples/standard_password_true-unreach-call_ground.i 2 3.3 220 22 - - - - 0 910    6200 0 960     4800  
array-examples/standard_reverse_true-unreach-call_ground.i 2 16   220 100 - - - - 0 900    4900 0 960     2000  
array-examples/standard_running_true-unreach-call.i 2 17   220 89 - - - - 0 900    5600 0 960     740  
array-examples/standard_sentinel_true-unreach-call_true-termination.i 2 100   750 870 - - - - 0 900    1000 2 9.0   320  
array-examples/standard_seq_init_true-unreach-call_ground.i 2 3.4 220 21 - - - - 0 900    2400 0 960     2200  
array-examples/standard_strcmp_true-unreach-call_ground.i 2 3.5 220 23 - - - - 0 900    5000 0 960     4600  
array-examples/standard_strcpy_original_true-unreach-call.i 2 16   220 100 - - - - 0 900    3800 0 960     4800  
array-examples/standard_strcpy_true-unreach-call_ground.i 2 15   210 110 - - - - 0 900    4500 0 960     3900  
array-examples/standard_two_index_01_true-unreach-call.i 2 15   220 110 - - - - 0 900    3900 0 960     3200  
array-examples/standard_two_index_02_true-unreach-call.i 2 15   220 110 - - - - 0 900    4200 0 960     3200  
array-examples/standard_two_index_03_true-unreach-call.i 2 17   220 100 - - - - 0 900    4700 0 960     3300  
array-examples/standard_two_index_04_true-unreach-call.i 2 16   220 100 - - - - 0 900    3900 0 960     3200  
array-examples/standard_two_index_05_true-unreach-call.i 2 16   220 97 - - - - 0 900    3700 0 960     3000  
array-examples/standard_two_index_06_true-unreach-call.i 2 16   220 120 - - - - 0 900    3800 0 960     3500  
array-examples/standard_two_index_07_true-unreach-call.i 2 17   220 96 - - - - 0 900    4800 0 960     3200  
array-examples/standard_two_index_08_true-unreach-call.i 2 17   220 92 - - - - 0 900    4200 0 960     3200  
array-examples/standard_two_index_09_true-unreach-call.i 2 17   220 110 - - - - 0 900    4100 0 960     2900  
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 2 15   210 100 - - - - 0 590    7000 0 960     4500  
array-examples/standard_vector_difference_true-unreach-call_ground.i 2 3.6 220 23 - - - - 0 900    3800 0 960     1900  
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i 0 900   8700 9300 0 .52 41 0 .022 4.9 0 .70 49 0 .0020 .26 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 0 220   15000 2400 0 .40 43 0 .019 4.9 0 .69 49 0 .0015 .28 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i 1 16   220 100 0 92    2100 -32 4.8   230   0 2.8  190 1 .58   18    - -
array-industry-pattern/array_range_init_false-unreach-call.i 1 120   210 1500 0 92    1200 0 97     4700   0 2.0  210 1 .60   18    - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i 0 16   220 120 0 92    2100 -32 4.9   230   0 2.0  210 -32 .58   18    - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 900   9100 9000 0 .58 44 0 .019 4.9 0 .86 49 0 .0021 .28 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i 2 15   220 100 - - - - 0 900    3400 0 960     3800  
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i 0 900   9000 13000 - - - - 0 .59 43 0 .018 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i 2 17   220 120 - - - - 0 900    3900 0 960     4900  
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 2 19   220 140 - - - - 0 900    4000 0 960     5900  
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 2 93   1200 780 - - - - 0 900    6400 2 12     470  
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 2 21   220 140 - - - - 0 900    4000 0 960     5900  
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 2 22   220 180 - - - - 0 900    5800 0 960     5900  
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 2 20   220 150 - - - - 0 770    7000 0 960     5900  
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 2 17   220 110 - - - - 0 900    3800 0 960     5900  
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 2 22   220 170 - - - - 0 900    3900 0 960     5900  
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i 2 15   220 110 - - - - 0 900    5600 0 960     4600  
reducercommutativity/rangesum05_false-unreach-call_true-termination.i 1 61   510 670 -32 4.1  260 1 8.3   350   0 3.5  220 1 .62   20    - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i 0 70   510 780 -32 5.0  290 0 58     7000   0 2.8  220 -32 .66   20    - -
reducercommutativity/rangesum20_false-unreach-call.i 0 89   1000 930 -32 6.0  280 0 54     7000   0 4.2  230 -32 .70   22    - -
reducercommutativity/rangesum40_false-unreach-call.i 1 140   2700 1300 -32 4.4  290 0 65     7000   0 3.3  220 1 .79   25    - -
reducercommutativity/rangesum60_false-unreach-call.i 1 270   3800 3400 -32 5.1  330 0 71     7000   0 6.0  330 1 .90   28    - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i 1 180   590 2000 0 5.1  360 1 16     480   0 3.5  210 1 .64   19    - -
reducercommutativity/avg05_true-unreach-call_true-termination.i 2 3.6 220 23 - - - - 0 900    1500 0 960     5300  
reducercommutativity/avg10_true-unreach-call_true-termination.i 2 3.5 220 26 - - - - 0 900    3600 0 860     7000  
reducercommutativity/avg20_true-unreach-call.i 2 3.4 230 25 - - - - 0 900    4900 0 960     1900  
reducercommutativity/avg40_true-unreach-call.i 2 3.6 220 26 - - - - 0 900    3400 0 960     4300  
reducercommutativity/avg60_true-unreach-call.i 2 3.6 220 23 - - - - 0 900    3600 0 960     3100  
reducercommutativity/avg_true-unreach-call_true-termination.i 2 2.0 150 17 - - - - 0 900    3100 0 960     590  
reducercommutativity/max05_true-unreach-call_true-termination.i 2 4.1 220 32 - - - - 2 110    910 0 960     1400  
reducercommutativity/max10_true-unreach-call_true-termination.i 2 4.3 220 32 - - - - 0 900    2800 0 960     2700  
reducercommutativity/max20_true-unreach-call.i 2 4.0 220 33 - - - - 0 900    4900 0 960     4600  
reducercommutativity/max40_true-unreach-call.i 2 4.1 230 32 - - - - 0 900    1700 0 960     4700  
reducercommutativity/max60_true-unreach-call.i 2 4.1 220 28 - - - - 0 900    3200 0 960     4600  
reducercommutativity/max_true-unreach-call_true-termination.i 2 7.0 160 76 - - - - 0 900    3300 0 960     1000  
reducercommutativity/sep05_true-unreach-call_true-termination.i 2 120   720 1200 - - - - 0 6.8  270 0 960     1800  
reducercommutativity/sep10_true-unreach-call.i 2 130   950 1300 - - - - 0 5.0  270 0 960     6800  
reducercommutativity/sep20_true-unreach-call.i 2 150   1100 1600 - - - - 0 5.8  290 0 910     7000  
reducercommutativity/sep40_true-unreach-call.i 2 220   830 2500 - - - - 0 5.3  280 0 960     4400  
reducercommutativity/sep60_true-unreach-call.i 0 900   510 11000 - - - - 0 .64 45 0 .020 4.9
reducercommutativity/sep_true-unreach-call_true-termination.i 0 900   2700 11000 - - - - 0 .55 41 0 .022 4.9
reducercommutativity/sum05_true-unreach-call_true-termination.i 2 3.6 220 24 - - - - 0 900    950 2 420     2900  
reducercommutativity/sum10_true-unreach-call_true-termination.i 2 3.4 220 24 - - - - 0 900    2100 0 960     5100  
reducercommutativity/sum20_true-unreach-call.i 2 3.4 220 23 - - - - 0 900    4200 0 960     4600  
reducercommutativity/sum40_true-unreach-call.i 2 3.5 220 24 - - - - 0 900    2500 0 960     4100  
reducercommutativity/sum60_true-unreach-call.i 2 3.6 220 23 - - - - 0 900    3300 0 960     2700  
reducercommutativity/sum_true-unreach-call_true-termination.i 2 1.7 150 15 - - - - 0 900    3300 0 960     4700  
array-tiling/mlceu_false-unreach-call.i 0 15   220 110 0 91    1800 -32 4.7   230   0 2.6  210 -32 .57   18    - -
array-tiling/skippedu_false-unreach-call.i 0 22   220 190 0 1.8  170 1 16     520   0 2.6  170 0 .57   18    - -
array-tiling/mbpr2_true-unreach-call.i 2 16   220 120 - - - - 0 900    4300 0 22     320  
array-tiling/mbpr3_true-unreach-call.i 2 20   220 140 - - - - 0 900    5400 0 960     1100  
array-tiling/mbpr4_true-unreach-call.i 2 28   220 250 - - - - 0 900    6200 0 190     760  
array-tiling/mbpr5_true-unreach-call.i 2 38   230 350 - - - - 0 900    5600 0 30     340  
array-tiling/nr2_true-unreach-call.i 0 900   6000 11000 - - - - 0 .72 43 0 .021 4.9
array-tiling/nr3_true-unreach-call.i 0 900   3000 12000 - - - - 0 .55 43 0 .019 4.9
array-tiling/nr4_true-unreach-call.i 0 900   220 14000 - - - - 0 .56 43 0 .020 4.9
array-tiling/nr5_true-unreach-call.i 0 900   2000 11000 - - - - 0 .63 41 0 .025 4.9
array-tiling/pnr2_true-unreach-call.i 2 16   220 110 - - - - 0 900    2200 0 960     2200  
array-tiling/pnr3_true-unreach-call.i 2 18   220 130 - - - - 0 900    2700 0 960     1700  
array-tiling/pnr4_true-unreach-call.i 2 26   220 230 - - - - 0 900    2000 0 960     3500  
array-tiling/pnr5_true-unreach-call.i 2 94   220 1200 - - - - 0 900    2200 0 960     3900  
array-tiling/poly1_true-unreach-call.i 2 1.7 160 15 - - - - 0 900    4900 0 960     930  
array-tiling/poly2_true-unreach-call.i 2 1.9 160 17 - - - - 0 900    4000 0 960     1600  
array-tiling/pr2_true-unreach-call.i 2 16   220 110 - - - - 0 900    2500 0 960     880  
array-tiling/pr3_true-unreach-call.i 2 19   220 140 - - - - 0 900    1900 0 960     1000  
array-tiling/pr4_true-unreach-call.i 2 27   210 230 - - - - 0 900    2100 0 960     850  
array-tiling/pr5_true-unreach-call.i 2 29   220 290 - - - - 0 900    2100 0 960     1200  
array-tiling/revcpyswp2_true-unreach-call.i 0 900   3700 7400 - - - - 0 .71 41 0 .018 5.0
array-tiling/rew_true-unreach-call.i 2 17   220 130 - - - - 0 900    2800 0 960     1600  
array-tiling/rewnif_true-unreach-call.i 2 24   220 210 - - - - 0 900    2500 0 960     1200  
array-tiling/rewnifrev2_true-unreach-call.i 2 40   220 430 - - - - 0 900    1600 0 960     3000  
array-tiling/rewnifrev_true-unreach-call.i 0 780   220 9500 - - - - 0 .59 41 0 .021 4.8
array-tiling/rewrev_true-unreach-call.i 2 25   220 250 - - - - 0 900    2400 0 960     2500  
array-tiling/skipped_true-unreach-call.i 2 20   220 150 - - - - 0 900    1100 0 960     1400  
array-tiling/tcpy_true-unreach-call.i 2 20   220 160 - - - - 0 900    1200 0 960     2300  
array-programs/copysome1_false-unreach-call.i 0 18   3100 130 0 91    2000 -32 4.6   230   0 2.7  180 -32 .61   18    - -
array-programs/copysome2_false-unreach-call.i 0 19   4900 150 0 92    2100 -32 3.7   230   0 2.8  210 -32 .60   18    - -
array-programs/copysome1_true-unreach-call.i 2 16   220 100 - - - - 0 860    7000 0 960     2600  
array-programs/copysome2_true-unreach-call.i 2 17   220 110 - - - - 0 900    7000 0 960     3100  
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
total 167 235 35000 310000 420000 44 -160 2400 66000 44 -477 1400 100000 44 0 580 39000 44 -175 880   1700 123 6 91000 430000 123 10 97000 380000
    correct results 126 235 10000 99000 120000 0 3 3 40 1300 0 17 17 11   330 3 6 120 1700 5 10 450 4200
        correct true 109 218 2200 28000 19000 0 0 0 0 3 6 120 1700 5 10 450 4200
        correct false 17 17 7800 71000 100000 0 3 3 40 1300 0 17 17 11   330 0 0
    correct-unconfimed results 16 0 4100 33000 57000 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 16 0 4100 33000 57000 0 0 0 0 0 0
    incorrect results 0 5 -160 25 1400 15 -480 73 3400 0 6 -192 3.7 120 0 0
        incorrect true 0 5 -160 25 1400 15 -480 73 3400 0 6 -192 3.7 120 0 0
        incorrect false 0 0 0 0 0 0 0
score (167 tasks, max score: 290) 235 -160 -477 0 -175 6 10
Run set veriabs.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Arrays