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