Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 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*
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-11-30 16:01:31 CET 2017-12-01 08:31:47 CET 2017-12-01 08:56:50 CET 2017-12-01 08:59:39 CET 2017-12-01 09:01:39 CET 2017-12-01 08:10:33 CET 2017-12-01 08:38:18 CET
Run set depthk.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Arrays
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.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/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.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/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/depthk.2017-11-30_1601.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 timeout 0 wit inspect 900   750 11000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .89 50 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unknown 0 wit inspect 46   160 530 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i unknown 0 wit inspect 46   160 650 error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .93 50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unknown 0 wit inspect 890   340 12000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i unknown 0 wit inspect 890   360 9100 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0035 .26 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i unknown 0 wit inspect 900   1400 9700 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i timeout 0 wit inspect 900   2400 13000 timeout 0 wit inspect 92    2200 timeout 0 wit inspect 97     1400   unknown 0 wit inspect .93 51 error (1) 0 wit inspect .078  9.0  - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i timeout 0 wit inspect 900   1400 12000 timeout 0 wit inspect 92    1800 timeout 0 wit inspect 96     1200   unknown 0 wit inspect 1.1  54 error (1) 0 wit inspect .080  9.0  - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i timeout 0 wit inspect 900   2400 11000 timeout 0 wit inspect 92    2000 timeout 0 wit inspect 96     1800   unknown 0 wit inspect .99 51 error (1) 0 wit inspect .068  9.1  - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i timeout 0 wit inspect 900   2400 11000 timeout 0 wit inspect 92    2000 timeout 0 wit inspect 97     1700   unknown 0 wit inspect .95 51 error (1) 0 wit inspect .068  9.1  - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i timeout 0 wit inspect 900   2500 12000 timeout 0 wit inspect 92    2400 timeout 0 wit inspect 97     2000   unknown 0 wit inspect .94 53 error (1) 0 wit inspect .072  9.0  - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i timeout 0 wit inspect 900   2200 13000 timeout 0 wit inspect 92    2600 timeout 0 wit inspect 97     2700   unknown 0 wit inspect 1.0  51 error (1) 0 wit inspect .067  9.0  - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i timeout 0 wit inspect 900   2200 13000 timeout 0 wit inspect 92    2400 timeout 0 wit inspect 97     2500   unknown 0 wit inspect .97 51 error (1) 0 wit inspect .071  9.1  - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i timeout 0 wit inspect 900   2200 11000 timeout 0 wit inspect 92    3000 timeout 0 wit inspect 97     2900   unknown 0 wit inspect .99 51 error (1) 0 wit inspect .071  9.1  - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i timeout 0 wit inspect 900   2500 11000 timeout 0 wit inspect 92    2700 timeout 0 wit inspect 97     2600   unknown 0 wit inspect .99 54 error (1) 0 wit inspect .070  9.0  - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unknown 0 wit inspect 890   220 9100 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i timeout 0 wit inspect 900   700 11000 timeout 0 wit inspect 92    1900 timeout 0 wit inspect 97     1100   unknown 0 wit inspect .95 51 error (1) 0 wit inspect .067  9.1  - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i timeout 0 wit inspect 900   710 13000 timeout 0 wit inspect 92    1700 timeout 0 wit inspect 96     1100   unknown 0 wit inspect .91 51 error (1) 0 wit inspect .071  9.1  - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i timeout 0 wit inspect 900   730 12000 timeout 0 wit inspect 92    2000 timeout 0 wit inspect 97     1200   unknown 0 wit inspect .71 51 error (1) 0 wit inspect .068  9.1  - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i timeout 0 wit inspect 900   700 12000 timeout 0 wit inspect 92    2100 timeout 0 wit inspect 97     1300   unknown 0 wit inspect .98 52 error (1) 0 wit inspect .068  9.1  - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i unknown 0 wit inspect 890   210 9200 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .86 51 error (invalid witness file) 0 wit inspect .0012 .32 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i unknown 0 wit inspect 890   240 8400 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i unknown 0 wit inspect 900   270 8300 error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .83 51 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i unknown 0 wit inspect 890   290 8700 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i unknown 0 wit inspect 900   320 10000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0012 .31 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i unknown 0 wit inspect 98   110 1400 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i timeout 0 wit inspect 900   2300 12000 timeout 0 wit inspect 92    2000 timeout 0 wit inspect 97     590   unknown 0 wit inspect .99 51 error (1) 0 wit inspect .069  9.1  - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i unknown 0 wit inspect 890   340 9300 error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unknown 0 wit inspect 890   970 7800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .048 4.8
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unknown 0 wit inspect 900   260 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .034 4.8
array-examples/relax_true-unreach-call.i unknown 0 wit inspect 890   190 7100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i unknown 0 wit inspect 320   180 4200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 4.8
array-examples/sanfoundry_10_true-unreach-call_ground.i unknown 0 wit inspect 890   180 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i timeout 0 wit inspect 900   3900 11000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  510 true 2 wit inspect 7.3   260  
array-examples/sanfoundry_27_true-unreach-call_ground.i unknown 0 wit inspect 120   120 1500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.9
array-examples/sanfoundry_43_true-unreach-call_ground.i unknown 0 wit inspect 52   100 720 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 5.0
array-examples/sorting_bubblesort_true-unreach-call_ground.i unknown 0 wit inspect 46   160 510 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i unknown 0 wit inspect 890   300 7800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 47 error (2) 0 wit inspect .020 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i unknown 0 wit inspect 890   190 9500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .019 4.9
array-examples/standard_compare_true-unreach-call_ground.i unknown 0 wit inspect 110   170 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_copy1_true-unreach-call_ground.i unknown 0 wit inspect 890   240 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.9
array-examples/standard_copy2_true-unreach-call_ground.i timeout 0 wit inspect 900   2200 12000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    7000 timeout 0 wit inspect 960     4800  
array-examples/standard_copy3_true-unreach-call_ground.i timeout 0 wit inspect 900   2200 12000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 timeout 0 wit inspect 960     4800  
array-examples/standard_copy4_true-unreach-call_ground.i timeout 0 wit inspect 900   1400 12000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 850    7000 timeout 0 wit inspect 960     4900  
array-examples/standard_copy5_true-unreach-call_ground.i timeout 0 wit inspect 900   2200 11000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 timeout 0 wit inspect 960     4900  
array-examples/standard_copy6_true-unreach-call_ground.i timeout 0 wit inspect 900   1400 11000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    7000 timeout 0 wit inspect 960     5000  
array-examples/standard_copy7_true-unreach-call_ground.i timeout 0 wit inspect 900   2200 11000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 810    7000 timeout 0 wit inspect 960     4900  
array-examples/standard_copy8_true-unreach-call_ground.i timeout 0 wit inspect 900   2200 12000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 730    7000 timeout 0 wit inspect 960     5100  
array-examples/standard_copy9_true-unreach-call_ground.i timeout 0 wit inspect 900   2400 13000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 830    7000 timeout 0 wit inspect 960     5000  
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unknown 0 wit inspect 890   160 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .018 4.9
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unknown 0 wit inspect 900   210 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.9
array-examples/standard_copyInitSum_true-unreach-call_ground.i unknown 0 wit inspect 890   190 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i unknown 0 wit inspect 890   220 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_find_true-unreach-call_ground.i timeout 0 wit inspect 900   2300 13000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 timeout 0 wit inspect 960     4800  
array-examples/standard_init1_true-unreach-call_ground.i timeout 0 wit inspect 900   730 13000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 timeout 0 wit inspect 960     2100  
array-examples/standard_init2_true-unreach-call_ground.i timeout 0 wit inspect 900   770 10000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     4000  
array-examples/standard_init3_true-unreach-call_ground.i timeout 0 wit inspect 900   730 10000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 timeout 0 wit inspect 960     4800  
array-examples/standard_init4_true-unreach-call_ground.i timeout 0 wit inspect 900   770 10000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     5200  
array-examples/standard_init5_true-unreach-call_ground.i unknown 0 wit inspect 890   220 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .019 4.9
array-examples/standard_init6_true-unreach-call_ground.i unknown 0 wit inspect 900   240 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .023 5.0
array-examples/standard_init7_true-unreach-call_ground.i unknown 0 wit inspect 890   270 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .036 4.8
array-examples/standard_init8_true-unreach-call_ground.i unknown 0 wit inspect 890   290 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .023 4.9
array-examples/standard_init9_true-unreach-call_ground.i unknown 0 wit inspect 900   320 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 46 error (2) 0 wit inspect .020 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i unknown 0 wit inspect 120   120 1600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 5.0
array-examples/standard_minInArray_true-unreach-call_ground.i unknown 0 wit inspect 100   120 1500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .048 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i unknown 0 wit inspect 890   160 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .035 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i timeout 0 wit inspect 900   2200 13000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 timeout 0 wit inspect 960     3900  
array-examples/standard_partition_original_true-unreach-call_ground.i timeout 0 wit inspect 900   2500 12000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 out of memory 0 wit inspect 84     7000  
array-examples/standard_partition_true-unreach-call_ground.i unknown 0 wit inspect 890   270 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_password_true-unreach-call_ground.i unknown 0 wit inspect 120   180 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_reverse_true-unreach-call_ground.i unknown 0 wit inspect 900   180 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_running_true-unreach-call.i unknown 0 wit inspect 890   300 9900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .029 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i unknown 0 wit inspect 100   75 1000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 0 wit inspect 900   780 13000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 timeout 0 wit inspect 960     2100  
array-examples/standard_strcmp_true-unreach-call_ground.i unknown 0 wit inspect 120   120 1800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_strcpy_original_true-unreach-call.i timeout 0 wit inspect 900   2300 11000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     4800  
array-examples/standard_strcpy_true-unreach-call_ground.i unknown 0 wit inspect 890   270 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_01_true-unreach-call.i unknown 0 wit inspect 890   250 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_02_true-unreach-call.i unknown 0 wit inspect 890   200 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_two_index_03_true-unreach-call.i unknown 0 wit inspect 890   180 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 46 error (2) 0 wit inspect .020 4.9
array-examples/standard_two_index_04_true-unreach-call.i unknown 0 wit inspect 890   230 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 4.9
array-examples/standard_two_index_05_true-unreach-call.i unknown 0 wit inspect 890   220 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .020 4.9
array-examples/standard_two_index_06_true-unreach-call.i unknown 0 wit inspect 890   180 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .034 4.8
array-examples/standard_two_index_07_true-unreach-call.i unknown 0 wit inspect 890   230 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .020 4.8
array-examples/standard_two_index_08_true-unreach-call.i unknown 0 wit inspect 890   190 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_09_true-unreach-call.i unknown 0 wit inspect 890   180 8700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unknown 0 wit inspect 98   100 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i timeout 0 wit inspect 900   2400 12000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     2100  
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unknown 0 wit inspect 890   330 9300 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unknown 0 wit inspect 890   300 9800 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unknown 0 wit inspect 890   250 9900 error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0012 .35 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i unknown 0 wit inspect 890   190 9700 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0035 .28 - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unknown 0 wit inspect 890   250 9600 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 900   5900 9600 timeout 0 wit inspect 91    2500 timeout 0 wit inspect 97     1300   unknown 0 wit inspect 1.0  52 error (1) 0 wit inspect .073  9.1  - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unknown 0 wit inspect 890   230 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .029 4.8
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unknown 0 wit inspect 890   1700 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i unknown 0 wit inspect 890   220 9400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 44 error (2) 0 wit inspect .020 4.9
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 0 wit inspect 900   3700 7100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 timeout 0 wit inspect 960     6000  
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unknown 0 wit inspect 540   650 5000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .023 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 900   4100 8200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 timeout 0 wit inspect 960     6000  
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unknown 0 wit inspect 890   230 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .047 5.0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unknown 0 wit inspect 890   250 9500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unknown 0 wit inspect 890   430 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unknown 0 wit inspect 890   390 9500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .018 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4100 8700 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6200 timeout 0 wit inspect 960     4500  
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 490   210 5400 true -32 wit inspect 3.7  260 true -32 wit inspect 5.3   260   unknown 0 wit inspect 2.2  210 error (2) 0 wit inspect .61   19    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 500   210 6800 true -32 wit inspect 4.1  270 true -32 wit inspect 5.5   270   unknown 0 wit inspect 3.5  220 error (2) 0 wit inspect .62   19    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 0 wit inspect 640   210 8400 true -32 wit inspect 3.1  270 true -32 wit inspect 5.7   320   unknown 0 wit inspect 3.8  220 error (2) 0 wit inspect .66   19    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i unknown 0 wit inspect 890   250 12000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0011 .35 - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i unknown 0 wit inspect 890   210 13000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 490   210 6000 timeout 0 wit inspect 92    1900 true -32 wit inspect 5.2   250   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i timeout 0 wit inspect 900   2200 11000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1500 timeout 0 wit inspect 960     5400  
reducercommutativity/avg10_true-unreach-call_true-termination.i timeout 0 wit inspect 900   3400 11000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 out of memory 0 wit inspect 900     7000  
reducercommutativity/avg20_true-unreach-call.i timeout 0 wit inspect 900   700 6500 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     1700  
reducercommutativity/avg40_true-unreach-call.i unknown 0 wit inspect 890   260 7300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8
reducercommutativity/avg60_true-unreach-call.i unknown 0 wit inspect 890   260 8300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
reducercommutativity/avg_true-unreach-call_true-termination.i unknown 0 wit inspect 890   180 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .023 4.8
reducercommutativity/max05_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1500 10000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 81    870 timeout 0 wit inspect 960     1300  
reducercommutativity/max10_true-unreach-call_true-termination.i timeout 0 wit inspect 900   2400 8700 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 timeout 0 wit inspect 960     3300  
reducercommutativity/max20_true-unreach-call.i unknown 0 wit inspect 890   190 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
reducercommutativity/max40_true-unreach-call.i unknown 0 wit inspect 890   270 7900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.9
reducercommutativity/max60_true-unreach-call.i unknown 0 wit inspect 890   230 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.9
reducercommutativity/max_true-unreach-call_true-termination.i unknown 0 wit inspect 890   250 9400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 timeout 0 wit inspect 960     880  
reducercommutativity/sep05_true-unreach-call_true-termination.i true 2 wit inspect 790   1600 9900 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 830    1500 timeout 0 wit inspect 960     1700  
reducercommutativity/sep10_true-unreach-call.i timeout 0 wit inspect 900   4900 9200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1700 out of memory 0 wit inspect 880     7000  
reducercommutativity/sep20_true-unreach-call.i unknown 0 wit inspect 900   190 10000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 900     7000  
reducercommutativity/sep40_true-unreach-call.i unknown 0 wit inspect 900   190 9400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 5.0
reducercommutativity/sep60_true-unreach-call.i unknown 0 wit inspect 890   190 9400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.8
reducercommutativity/sep_true-unreach-call_true-termination.i unknown 0 wit inspect 890   190 7500 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 timeout 0 wit inspect 960     3000  
reducercommutativity/sum05_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4000 10000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    900 true 2 wit inspect 320     3500  
reducercommutativity/sum10_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1900 13000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     5400  
reducercommutativity/sum20_true-unreach-call.i unknown 0 wit inspect 890   240 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9
reducercommutativity/sum40_true-unreach-call.i unknown 0 wit inspect 890   200 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 45 error (2) 0 wit inspect .020 4.8
reducercommutativity/sum60_true-unreach-call.i unknown 0 wit inspect 890   230 6900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.8
reducercommutativity/sum_true-unreach-call_true-termination.i unknown 0 wit inspect 890   200 9000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     4800  
array-tiling/mlceu_false-unreach-call.i timeout 0 wit inspect 900   3500 7800 timeout 0 wit inspect 92    1600 timeout 0 wit inspect 96     1000   unknown 0 wit inspect .96 53 error (1) 0 wit inspect .066  9.0  - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i false(unreach-call) 0 wit inspect 1.1 100 13 timeout 0 wit inspect 92    2000 true -32 wit inspect 4.9   230   unknown 0 wit inspect 3.2  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i unknown 0 wit inspect 890   160 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .018 4.9
array-tiling/mbpr3_true-unreach-call.i unknown 0 wit inspect 890   220 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .051 4.9
array-tiling/mbpr4_true-unreach-call.i unknown 0 wit inspect 890   300 9100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 45 error (2) 0 wit inspect .020 4.9
array-tiling/mbpr5_true-unreach-call.i unknown 0 wit inspect 890   350 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.9
array-tiling/nr2_true-unreach-call.i unknown 0 wit inspect 890   420 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .019 4.9
array-tiling/nr3_true-unreach-call.i unknown 0 wit inspect 890   470 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .026 4.9
array-tiling/nr4_true-unreach-call.i unknown 0 wit inspect 890   440 8700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 5.0
array-tiling/nr5_true-unreach-call.i unknown 0 wit inspect 890   450 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .018 4.8
array-tiling/pnr2_true-unreach-call.i unknown 0 wit inspect 890   140 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 5.0
array-tiling/pnr3_true-unreach-call.i unknown 0 wit inspect 890   200 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .020 4.9
array-tiling/pnr4_true-unreach-call.i unknown 0 wit inspect 890   240 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 5.0
array-tiling/pnr5_true-unreach-call.i unknown 0 wit inspect 890   280 8800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9
array-tiling/poly1_true-unreach-call.i unknown 0 wit inspect 890   190 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9
array-tiling/poly2_true-unreach-call.i unknown 0 wit inspect 890   160 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 5.0
array-tiling/pr2_true-unreach-call.i unknown 0 wit inspect 890   260 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.8
array-tiling/pr3_true-unreach-call.i unknown 0 wit inspect 890   230 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .017 4.8
array-tiling/pr4_true-unreach-call.i unknown 0 wit inspect 890   240 9500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .018 4.9
array-tiling/pr5_true-unreach-call.i unknown 0 wit inspect 890   280 9500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 4.8
array-tiling/revcpyswp2_true-unreach-call.i timeout 0 wit inspect 900   5600 8100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2400 timeout 0 wit inspect 960     2000  
array-tiling/rew_true-unreach-call.i timeout 0 wit inspect 900   3400 9100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 timeout 0 wit inspect 960     1700  
array-tiling/rewnif_true-unreach-call.i timeout 0 wit inspect 900   4900 10000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 timeout 0 wit inspect 960     1200  
array-tiling/rewnifrev2_true-unreach-call.i timeout 0 wit inspect 900   5000 8400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 timeout 0 wit inspect 960     2900  
array-tiling/rewnifrev_true-unreach-call.i timeout 0 wit inspect 900   2600 11000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     2400  
array-tiling/rewrev_true-unreach-call.i timeout 0 wit inspect 900   3800 11000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 timeout 0 wit inspect 960     2200  
array-tiling/skipped_true-unreach-call.i unknown 0 wit inspect 890   100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.9
array-tiling/tcpy_true-unreach-call.i unknown 0 wit inspect 890   170 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9
array-programs/copysome1_false-unreach-call.i unknown 0 wit inspect 890   280 10000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-programs/copysome2_false-unreach-call.i unknown 0 wit inspect 890   310 9300 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 48 error (invalid witness file) 0 wit inspect .0012 .31 - wit inspect - wit inspect
array-programs/copysome1_true-unreach-call.i unknown 0 wit inspect 890   280 7900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.8
array-programs/copysome2_true-unreach-call.i unknown 0 wit inspect 890   260 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.9
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 3 140000 160000 1500000 44 -96 1700 40000 44 -160 1600 28000 44 0 51 3000 44 -31 4.2  250 123 6 35000 170000 123 4 37000 160000
    correct results 2 3 1300 1800 16000 0 0 0 1 1 .61 19 3 6 920 2900 2 4 330 3800
        correct true 1 2 790 1600 9900 0 0 0 0 3 6 920 2900 2 4 330 3800
        correct false 1 1 490 210 6000 0 0 0 1 1 .61 19 0 0
    correct-unconfimed results 4 0 1600 740 21000 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 4 0 1600 740 21000 0 0 0 0 0 0
    incorrect results 0 3 -96 11 800 5 -160 27 1300 0 1 -32 .58 18 0 0
        incorrect true 0 3 -96 11 800 5 -160 27 1300 0 1 -32 .58 18 0 0
        incorrect false 0 0 0 0 0 0 0
score (167 tasks, max score: 290) 3 -96 -160 0 -31 6 4
Run set depthk.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Arrays