Tool VerifierIntegerAssignmentPrograms File not exits 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*
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-03 03:42:11 CET 2017-12-03 04:30:19 CET 2017-12-03 04:52:11 CET 2017-12-03 04:56:53 CET 2017-12-03 05:05:18 CET 2017-12-03 04:20:47 CET 2017-12-03 04:35:31 CET
Run set viap.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-viap.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-viap.sv-comp18-correctness-witness.ReachSafety-Arrays
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/viap.2017-12-03_0342.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/viap.2017-12-03_0342.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/viap.2017-12-03_0342.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/viap.2017-12-03_0342.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/viap.2017-12-03_0342.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/viap.2017-12-03_0342.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 46   120 620 0 .56 43 0 .019 4.9 0 .92 50 0 .0016 .26 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 230   370 2300 0 .64 44 0 .018 4.8 0 .85 49 0 .0025 .30 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 230   330 2200 0 .64 41 0 .020 4.8 0 .86 47 0 .0014 .26 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 470   420 5600 0 .61 44 0 .022 5.0 0 .84 47 0 .0013 .26 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 260   280 3700 0 .66 42 0 .022 5.0 0 .87 47 0 .0037 .29 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i 0 530   420 5300 0 .51 42 0 .018 4.8 0 1.1  49 0 .0015 .26 - -
array-examples/standard_copy1_false-unreach-call_ground.i 1 15   540 190 0 92    2000 -32 6.5   260   0 2.7  190 1 .59   18    - -
array-examples/standard_copy2_false-unreach-call_ground.i 1 18   710 240 0 92    2000 -32 5.3   220   0 2.8  190 1 .62   18    - -
array-examples/standard_copy3_false-unreach-call_ground.i 1 21   880 270 0 91    2000 -32 4.8   230   0 3.1  210 1 .68   18    - -
array-examples/standard_copy4_false-unreach-call_ground.i 1 23   1000 320 0 92    2000 -32 5.0   230   0 2.7  190 1 .59   18    - -
array-examples/standard_copy5_false-unreach-call_ground.i 1 26   1200 310 0 91    2000 -32 4.8   230   0 2.8  190 1 .74   18    - -
array-examples/standard_copy6_false-unreach-call_ground.i 1 28   1400 410 0 92    2000 -32 4.9   230   0 2.7  180 1 .70   18    - -
array-examples/standard_copy7_false-unreach-call_ground.i 1 31   1600 490 0 92    2100 -32 4.9   230   0 3.1  210 1 .71   18    - -
array-examples/standard_copy8_false-unreach-call_ground.i 1 34   1800 440 0 91    2100 -32 4.7   230   0 2.9  190 1 .67   18    - -
array-examples/standard_copy9_false-unreach-call_ground.i 1 36   2000 550 0 92    2100 -32 5.1   230   0 2.8  210 1 .59   18    - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 1 17   1100 260 0 97    5300 0 97     6700   0 98    5500 1 82      6300    - -
array-examples/standard_init1_false-unreach-call_ground.i 1 12   480 160 0 97    3900 0 96     6100   0 97    3800 1 26      2100    - -
array-examples/standard_init2_false-unreach-call_ground.i 1 14   790 210 0 96    5100 0 96     6100   0 96    4800 1 62      4200    - -
array-examples/standard_init3_false-unreach-call_ground.i 1 17   1100 210 0 98    5300 0 87     7000   0 98    5300 1 80      6300    - -
array-examples/standard_init4_false-unreach-call_ground.i 0 20   1400 290 0 98    5500 0 98     6700   0 98    5500 0 91      7000    - -
array-examples/standard_init5_false-unreach-call_ground.i 0 23   1800 290 0 98    5900 0 96     5400   0 98    5500 0 82      7000    - -
array-examples/standard_init6_false-unreach-call_ground.i 0 26   2100 350 0 98    5400 0 97     5400   0 98    5500 0 73      7000    - -
array-examples/standard_init7_false-unreach-call_ground.i 0 28   2400 400 0 98    5500 0 98     5500   0 98    5500 0 87      7000    - -
array-examples/standard_init8_false-unreach-call_ground.i 0 31   2700 380 0 98    5500 0 97     5600   0 98    5500 0 75      7000    - -
array-examples/standard_init9_false-unreach-call_ground.i 0 34   3100 420 0 98    5500 0 97     5600   0 98    5500 0 76      7000    - -
array-examples/standard_minInArray_false-unreach-call_ground.i 1 12   580 160 0 96    4100 0 96     6300   0 97    3800 1 38      2700    - -
array-examples/standard_partition_false-unreach-call_ground.i 0 29   110 430 0 .53 42 0 .018 4.8 0 .87 47 0 .0013 .26 - -
array-examples/standard_running_false-unreach-call.i 0 530   1200 5200 0 .70 42 0 .025 4.9 0 .86 49 0 .0013 .26 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 0 70   160 1000 - - - - 0 .72 43 0 .023 4.9
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 46   120 680 - - - - 0 .69 44 0 .019 4.8
array-examples/relax_true-unreach-call.i 0 11   92 170 - - - - 0 .71 44 0 .023 4.9
array-examples/sanfoundry_02_true-unreach-call_ground.i 2 360   1100 3600 - - - - 0 .62 42 0 .024 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i 0 340   730 4000 - - - - 0 .50 44 0 .023 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i 2 15   130 180 - - - - 0 .56 43 0 .024 5.0
array-examples/sanfoundry_27_true-unreach-call_ground.i 2 120   840 1100 - - - - 0 .63 43 0 .026 4.8
array-examples/sanfoundry_43_true-unreach-call_ground.i 0 13   93 160 - - - - 0 .69 44 0 .025 4.8
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 230   320 1900 - - - - 0 .70 43 0 .018 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 260   250 3600 - - - - 0 .54 42 0 .019 5.0
array-examples/standard_compareModified_true-unreach-call_ground.i 2 120   550 1300 - - - - 0 .51 43 0 .024 5.0
array-examples/standard_compare_true-unreach-call_ground.i 2 120   900 1400 - - - - 0 .66 41 0 .025 4.9
array-examples/standard_copy1_true-unreach-call_ground.i 2 33   140 430 - - - - 0 .65 44 0 .022 4.9
array-examples/standard_copy2_true-unreach-call_ground.i 2 36   140 460 - - - - 0 .58 43 0 .027 4.8
array-examples/standard_copy3_true-unreach-call_ground.i 2 38   140 610 - - - - 0 .60 43 0 .023 4.9
array-examples/standard_copy4_true-unreach-call_ground.i 2 41   140 600 - - - - 0 .72 41 0 .019 4.9
array-examples/standard_copy5_true-unreach-call_ground.i 2 44   140 570 - - - - 0 .70 43 0 .025 4.8
array-examples/standard_copy6_true-unreach-call_ground.i 2 46   140 620 - - - - 0 .63 43 0 .019 4.9
array-examples/standard_copy7_true-unreach-call_ground.i 2 50   140 730 - - - - 0 .70 43 0 .024 5.0
array-examples/standard_copy8_true-unreach-call_ground.i 2 53   170 760 - - - - 0 .60 42 0 .033 4.8
array-examples/standard_copy9_true-unreach-call_ground.i 2 55   150 710 - - - - 0 .53 45 0 .025 5.0
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 2 25   130 360 - - - - 0 .64 41 0 .023 5.0
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 2 30   170 390 - - - - 0 .68 41 0 .023 5.0
array-examples/standard_copyInitSum_true-unreach-call_ground.i 2 26   130 370 - - - - 0 .54 43 0 .023 4.8
array-examples/standard_copyInit_true-unreach-call_ground.i 2 22   130 300 - - - - 0 .69 43 0 .021 5.0
array-examples/standard_find_true-unreach-call_ground.i 2 25   180 340 - - - - 0 .77 45 0 .024 4.9
array-examples/standard_init1_true-unreach-call_ground.i 2 20   130 330 - - - - 0 .72 43 0 .025 4.9
array-examples/standard_init2_true-unreach-call_ground.i 2 22   130 360 - - - - 0 .61 41 0 .025 4.8
array-examples/standard_init3_true-unreach-call_ground.i 2 25   140 380 - - - - 0 .70 43 0 .022 4.8
array-examples/standard_init4_true-unreach-call_ground.i 2 28   140 370 - - - - 0 .67 44 0 .024 4.8
array-examples/standard_init5_true-unreach-call_ground.i 2 30   140 390 - - - - 0 .70 41 0 .020 4.9
array-examples/standard_init6_true-unreach-call_ground.i 2 33   140 490 - - - - 0 .69 42 0 .018 4.8
array-examples/standard_init7_true-unreach-call_ground.i 2 35   150 490 - - - - 0 .54 43 0 .019 4.8
array-examples/standard_init8_true-unreach-call_ground.i 2 38   140 520 - - - - 0 .62 42 0 .024 4.8
array-examples/standard_init9_true-unreach-call_ground.i 2 40   170 520 - - - - 0 .61 42 0 .028 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i 2 130   1200 1500 - - - - 0 .61 42 0 .020 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i 2 130   1400 1600 - - - - 0 .63 43 0 .022 4.9
array-examples/standard_palindrome_true-unreach-call_ground.i 2 18   130 250 - - - - 0 .67 43 0 .025 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i 0 220   740 2300 - - - - 0 .71 41 0 .024 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i 0 24   120 350 - - - - 0 .57 42 0 .024 4.8
array-examples/standard_partition_true-unreach-call_ground.i 0 31   120 410 - - - - 0 .69 41 0 .025 4.8
array-examples/standard_password_true-unreach-call_ground.i 2 120   1200 1500 - - - - 0 .55 43 0 .019 4.9
array-examples/standard_reverse_true-unreach-call_ground.i 2 20   120 280 - - - - 0 .59 41 0 .023 4.8
array-examples/standard_running_true-unreach-call.i 2 430   1200 3800 - - - - 0 .68 43 0 .025 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i 2 9.3 150 130 - - - - 0 .58 44 0 .022 4.9
array-examples/standard_seq_init_true-unreach-call_ground.i 2 23   230 270 - - - - 0 .58 44 0 .023 4.8
array-examples/standard_strcmp_true-unreach-call_ground.i 2 130   670 1500 - - - - 0 .68 41 0 .024 4.8
array-examples/standard_strcpy_original_true-unreach-call.i 2 23   140 330 - - - - 0 .55 41 0 .023 4.8
array-examples/standard_strcpy_true-unreach-call_ground.i 2 24   140 340 - - - - 0 .51 41 0 .023 4.9
array-examples/standard_two_index_01_true-unreach-call.i 2 18   140 270 - - - - 0 .62 41 0 .024 4.8
array-examples/standard_two_index_02_true-unreach-call.i 2 29   140 360 - - - - 0 .70 44 0 .021 4.9
array-examples/standard_two_index_03_true-unreach-call.i 2 18   140 220 - - - - 0 .72 43 0 .019 5.0
array-examples/standard_two_index_04_true-unreach-call.i 2 28   150 410 - - - - 0 .56 42 0 .024 4.8
array-examples/standard_two_index_05_true-unreach-call.i 2 28   140 390 - - - - 0 .50 44 0 .022 5.0
array-examples/standard_two_index_06_true-unreach-call.i 2 18   140 270 - - - - 0 .75 46 0 .018 4.9
array-examples/standard_two_index_07_true-unreach-call.i 2 27   140 320 - - - - 0 .60 43 0 .024 4.9
array-examples/standard_two_index_08_true-unreach-call.i 2 27   140 360 - - - - 0 .68 41 0 .019 4.8
array-examples/standard_two_index_09_true-unreach-call.i 2 27   140 400 - - - - 0 .57 41 0 .023 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 0 29   350 370 - - - - 0 .67 43 0 .018 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i 2 21   130 270 - - - - 0 .54 43 0 .019 4.8
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i 1 12   520 160 0 96    3900 0 92     7000   0 97    3800 1 29      2100    - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 0 15   110 210 0 .66 43 0 .029 4.8 0 .68 50 0 .0013 .28 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i 0 220   1300 2300 0 .66 43 0 .019 4.8 0 .86 47 0 .0015 .30 - -
array-industry-pattern/array_range_init_false-unreach-call.i 1 12   100 160 0 92    830 0 97     4700   0 2.7  180 1 .57   18    - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i 0 220   1400 2700 0 .62 41 0 .018 4.8 0 .86 47 0 .0014 .26 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 22   110 270 0 93    2200 -32 3.7   240   0 2.8  210 -32 .58   18    - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i 2 21   210 270 - - - - 0 .63 41 0 .024 5.0
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i 2 54   340 780 - - - - 0 .68 44 0 .024 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i 2 18   230 230 - - - - 0 .74 44 0 .023 4.8
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 3.4 92 50 - - - - 0 .74 43 0 .021 4.8
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 0 4.3 92 59 - - - - 0 .55 43 0 .024 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 3.3 92 50 - - - - 0 .51 43 0 .024 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 2.5 92 32 - - - - 0 .53 43 0 .018 4.8
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 0 24   130 310 - - - - 0 .56 44 0 .025 4.8
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 0 3.3 92 40 - - - - 0 .56 44 0 .018 4.8
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 0 3.4 92 51 - - - - 0 .56 41 0 .023 4.9
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i 2 14   130 180 - - - - 0 .59 43 0 .018 5.0
reducercommutativity/rangesum05_false-unreach-call_true-termination.i 1 25   120 320 0 2.3  160 -32 6.6   230   0 2.6  170 1 .61   18    - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i 1 25   110 310 0 3.0  170 -32 5.5   240   0 2.4  170 1 .59   18    - -
reducercommutativity/rangesum20_false-unreach-call.i 1 25   96 340 0 1.6  160 -32 4.9   230   0 1.8  170 1 .59   18    - -
reducercommutativity/rangesum40_false-unreach-call.i 1 25   98 330 0 2.6  160 -32 5.7   230   0 1.8  170 1 .62   18    - -
reducercommutativity/rangesum60_false-unreach-call.i 1 25   120 420 0 3.1  170 -32 5.2   230   0 2.5  170 1 .58   18    - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i 0 360   340 4500 0 .52 41 0 .019 4.9 0 .89 49 0 .0013 .26 - -
reducercommutativity/avg05_true-unreach-call_true-termination.i 2 41   240 450 - - - - 0 .70 43 0 .023 4.8
reducercommutativity/avg10_true-unreach-call_true-termination.i 2 25   250 340 - - - - 0 .54 41 0 .023 4.9
reducercommutativity/avg20_true-unreach-call.i 2 320   660 4300 - - - - 0 .69 44 0 .024 4.9
reducercommutativity/avg40_true-unreach-call.i 2 25   250 300 - - - - 0 .67 44 0 .023 4.9
reducercommutativity/avg60_true-unreach-call.i 2 25   260 340 - - - - 0 .59 43 0 .033 4.9
reducercommutativity/avg_true-unreach-call_true-termination.i 0 330   270 4700 - - - - 0 .73 44 0 .025 4.8
reducercommutativity/max05_true-unreach-call_true-termination.i 2 180   250 2100 - - - - 0 .52 41 0 .019 4.8
reducercommutativity/max10_true-unreach-call_true-termination.i 2 250   450 3200 - - - - 0 .61 42 0 .021 4.8
reducercommutativity/max20_true-unreach-call.i 2 370   680 4200 - - - - 0 .66 43 0 .026 5.0
reducercommutativity/max40_true-unreach-call.i 2 250   640 3100 - - - - 0 .68 44 0 .024 4.9
reducercommutativity/max60_true-unreach-call.i 2 250   450 3100 - - - - 0 .70 43 0 .019 4.9
reducercommutativity/max_true-unreach-call_true-termination.i 0 340   560 4500 - - - - 0 .63 43 0 .027 4.8
reducercommutativity/sep05_true-unreach-call_true-termination.i 0 350   440 4600 - - - - 0 .68 41 0 .027 4.8
reducercommutativity/sep10_true-unreach-call.i 0 350   470 4800 - - - - 0 .62 44 0 .022 4.8
reducercommutativity/sep20_true-unreach-call.i 0 350   510 4200 - - - - 0 .68 41 0 .023 4.8
reducercommutativity/sep40_true-unreach-call.i 0 350   510 4500 - - - - 0 .73 43 0 .027 4.8
reducercommutativity/sep60_true-unreach-call.i 0 350   470 4100 - - - - 0 .69 42 0 .023 4.8
reducercommutativity/sep_true-unreach-call_true-termination.i 0 240   500 2900 - - - - 0 .68 43 0 .021 5.0
reducercommutativity/sum05_true-unreach-call_true-termination.i 2 43   240 500 - - - - 0 .70 43 0 .025 4.9
reducercommutativity/sum10_true-unreach-call_true-termination.i 2 26   250 310 - - - - 0 .65 41 0 .023 4.8
reducercommutativity/sum20_true-unreach-call.i 2 320   600 3600 - - - - 0 .57 42 0 .025 4.9
reducercommutativity/sum40_true-unreach-call.i 2 26   250 330 - - - - 0 .55 43 0 .022 4.9
reducercommutativity/sum60_true-unreach-call.i 2 25   250 300 - - - - 0 .68 43 0 .025 4.9
reducercommutativity/sum_true-unreach-call_true-termination.i 0 330   460 4600 - - - - 0 .64 43 0 .023 5.0
array-tiling/mlceu_false-unreach-call.i 0 17   120 260 0 .71 41 0 .030 4.8 0 .86 49 0 .0015 .26 - -
array-tiling/skippedu_false-unreach-call.i 0 89   490 1100 0 .70 42 0 .017 4.8 0 .86 47 0 .0013 .28 - -
array-tiling/mbpr2_true-unreach-call.i 2 38   200 430 - - - - 0 .54 45 0 .019 4.9
array-tiling/mbpr3_true-unreach-call.i 2 57   200 750 - - - - 0 .67 46 0 .028 4.8
array-tiling/mbpr4_true-unreach-call.i 2 100   360 1500 - - - - 0 .70 43 0 .019 4.9
array-tiling/mbpr5_true-unreach-call.i 2 330   6200 4100 - - - - 0 .60 42 0 .018 4.8
array-tiling/nr2_true-unreach-call.i 2 31   230 430 - - - - 0 .53 43 0 .020 4.8
array-tiling/nr3_true-unreach-call.i 2 30   220 490 - - - - 0 .71 41 0 .024 4.8
array-tiling/nr4_true-unreach-call.i 2 30   230 410 - - - - 0 .66 45 0 .024 4.9
array-tiling/nr5_true-unreach-call.i 2 30   230 380 - - - - 0 .53 43 0 .021 5.0
array-tiling/pnr2_true-unreach-call.i 2 30   220 420 - - - - 0 .55 44 0 .026 4.9
array-tiling/pnr3_true-unreach-call.i 2 31   220 420 - - - - 0 .61 41 0 .019 4.8
array-tiling/pnr4_true-unreach-call.i 2 40   210 590 - - - - 0 .54 44 0 .023 4.9
array-tiling/pnr5_true-unreach-call.i 2 57   210 640 - - - - 0 .70 41 0 .018 5.0
array-tiling/poly1_true-unreach-call.i 2 13   140 190 - - - - 0 .70 43 0 .023 4.8
array-tiling/poly2_true-unreach-call.i 2 16   150 200 - - - - 0 .50 43 0 .020 4.8
array-tiling/pr2_true-unreach-call.i 2 30   220 400 - - - - 0 .71 42 0 .019 4.8
array-tiling/pr3_true-unreach-call.i 2 33   230 400 - - - - 0 .51 44 0 .026 4.8
array-tiling/pr4_true-unreach-call.i 2 41   210 510 - - - - 0 .67 41 0 .018 4.9
array-tiling/pr5_true-unreach-call.i 2 65   230 740 - - - - 0 .59 42 0 .021 4.8
array-tiling/revcpyswp2_true-unreach-call.i 2 130   440 1600 - - - - 0 .61 43 0 .024 4.9
array-tiling/rew_true-unreach-call.i 2 15   150 200 - - - - 0 .68 43 0 .024 5.0
array-tiling/rewnif_true-unreach-call.i 2 15   170 210 - - - - 0 .62 44 0 .025 4.8
array-tiling/rewnifrev2_true-unreach-call.i 0 170   310 2100 - - - - 0 .71 42 0 .019 4.8
array-tiling/rewnifrev_true-unreach-call.i 2 66   330 570 - - - - 0 .67 41 0 .024 4.8
array-tiling/rewrev_true-unreach-call.i 2 16   210 210 - - - - 0 .69 43 0 .024 4.9
array-tiling/skipped_true-unreach-call.i 0 130   610 1400 - - - - 0 .69 41 0 .023 4.8
array-tiling/tcpy_true-unreach-call.i 2 30   220 440 - - - - 0 .76 43 0 .022 4.8
array-programs/copysome1_false-unreach-call.i 0 22   1300 290 0 92    2000 -32 4.4   220   0 3.0  180 -32 .72   19    - -
array-programs/copysome2_false-unreach-call.i 0 26   1600 350 0 91    2100 -32 4.6   220   0 2.8  190 -32 .60   18    - -
array-programs/copysome1_true-unreach-call.i 2 71   230 960 - - - - 0 .62 43 0 .023 4.8
array-programs/copysome2_true-unreach-call.i 2 97   270 1200 - - - - 0 .69 42 0 .020 4.8
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 209 15000 82000 180000 44 0 2400 88000 44 -544 1300 82000 44 0 1200 64000 44 -75 810   66000 123 0 78 5300 123 0 2.8 600
    correct results 115 209 7000 50000 86000 0 0 0 21 21 330   24000 0 0
        correct true 94 188 6600 34000 80000 0 0 0 0 0 0
        correct false 21 21 460 16000 6300 0 0 0 21 21 330   24000 0 0
    correct-unconfimed results 9 0 230 16000 3000 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 9 0 230 16000 3000 0 0 0 0 0 0
    incorrect results 0 0 17 -544 86 3900 0 3 -96 1.9 55 0 0
        incorrect true 0 0 17 -544 86 3900 0 3 -96 1.9 55 0 0
        incorrect false 0 0 0 0 0 0 0
score (167 tasks, max score: 290) 209 0 -544 0 -75 0 0
Run set viap.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-viap.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-viap.sv-comp18-correctness-witness.ReachSafety-Arrays