Tool ULTIMATE Kojak 0.1.23-3204b741 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 02:33:02 CET 2017-12-03 03:22:18 CET 2017-12-03 03:55:21 CET 2017-12-03 04:22:06 CET 2017-12-03 04:36:43 CET 2017-12-03 00:36:56 CET 2017-12-03 03:32:10 CET
Run set ukojak.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Arrays
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/ukojak.2017-12-02_0233.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   5100 11000 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .74 49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i timeout 0 wit inspect 900   4900 10000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .038 5.0 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0021 .28 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i timeout 0 wit inspect 900   4900 14000 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i timeout 0 wit inspect 900   5100 14000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .027 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0041 .31 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i timeout 0 wit inspect 900   5000 14000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0018 .27 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i timeout 0 wit inspect 900   5300 12000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .94 47 error (invalid witness file) 0 wit inspect .0015 .34 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i timeout 0 wit inspect 900   4900 14000 error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i timeout 0 wit inspect 900   4900 12000 error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .95 49 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i timeout 0 wit inspect 900   4700 11000 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i timeout 0 wit inspect 900   4700 12000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0014 .32 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i timeout 0 wit inspect 900   5500 11000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0040 .30 - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i timeout 0 wit inspect 900   4900 11000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect 1.1  51 error (invalid witness file) 0 wit inspect .0016 .32 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i timeout 0 wit inspect 900   4700 13000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i timeout 0 wit inspect 900   4900 11000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i timeout 0 wit inspect 900   4800 14000 error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .73 49 error (invalid witness file) 0 wit inspect .0019 .28 - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i timeout 0 wit inspect 900   4800 12000 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .79 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i timeout 0 wit inspect 900   4800 12000 error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect 1.2  49 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i timeout 0 wit inspect 900   4800 12000 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect 1.1  48 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .91 47 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .035 4.9 error (invalid witness file) 0 wit inspect .90 48 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i timeout 0 wit inspect 900   4800 12000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i timeout 0 wit inspect 900   4800 12000 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .98 47 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i timeout 0 wit inspect 900   4900 9300 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .027 4.8 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i timeout 0 wit inspect 900   4800 12000 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i timeout 0 wit inspect 900   5200 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .018 5.0
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i timeout 0 wit inspect 900   4900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 4.9
array-examples/relax_true-unreach-call.i timeout 0 wit inspect 900   590 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .017 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i timeout 0 wit inspect 900   4900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .020 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i timeout 0 wit inspect 900   5300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .020 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i true 2 wit inspect 5.8 330 48 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  510 true 2 wit inspect 7.9   280  
array-examples/sanfoundry_27_true-unreach-call_ground.i timeout 0 wit inspect 900   4700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 5.0
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect 4.3 250 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 4.9   230  
array-examples/sorting_bubblesort_true-unreach-call_ground.i timeout 0 wit inspect 900   5200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .020 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 0 wit inspect 900   5100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 5.0
array-examples/standard_compareModified_true-unreach-call_ground.i timeout 0 wit inspect 900   4900 12000 - 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-examples/standard_compare_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9
array-examples/standard_copy1_true-unreach-call_ground.i timeout 0 wit inspect 900   4700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy2_true-unreach-call_ground.i timeout 0 wit inspect 900   4900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .018 5.0
array-examples/standard_copy3_true-unreach-call_ground.i timeout 0 wit inspect 900   4700 12000 - 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-examples/standard_copy4_true-unreach-call_ground.i timeout 0 wit inspect 900   4700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.8
array-examples/standard_copy5_true-unreach-call_ground.i timeout 0 wit inspect 900   4900 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy6_true-unreach-call_ground.i timeout 0 wit inspect 900   4700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .022 5.0
array-examples/standard_copy7_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy8_true-unreach-call_ground.i timeout 0 wit inspect 900   4700 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 47 error (2) 0 wit inspect .018 5.0
array-examples/standard_copy9_true-unreach-call_ground.i timeout 0 wit inspect 900   4700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_copyInitSum2_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.8
array-examples/standard_copyInitSum3_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .017 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 47 error (2) 0 wit inspect .018 4.8
array-examples/standard_copyInit_true-unreach-call_ground.i timeout 0 wit inspect 900   5000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .017 4.8
array-examples/standard_find_true-unreach-call_ground.i timeout 0 wit inspect 900   5000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_init1_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .023 5.0
array-examples/standard_init2_true-unreach-call_ground.i timeout 0 wit inspect 900   4700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .022 4.8
array-examples/standard_init3_true-unreach-call_ground.i timeout 0 wit inspect 900   5200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.9
array-examples/standard_init4_true-unreach-call_ground.i timeout 0 wit inspect 900   5200 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_init5_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .019 4.8
array-examples/standard_init6_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .024 4.8
array-examples/standard_init7_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_init8_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 5.0
array-examples/standard_init9_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 5.0
array-examples/standard_maxInArray_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .023 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 - 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/standard_partial_init_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 46 error (2) 0 wit inspect .019 4.9
array-examples/standard_partition_original_true-unreach-call_ground.i timeout 0 wit inspect 900   5200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .80 45 error (2) 0 wit inspect .018 4.9
array-examples/standard_partition_true-unreach-call_ground.i timeout 0 wit inspect 900   4700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 48 error (2) 0 wit inspect .019 5.0
array-examples/standard_password_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_reverse_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 9400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 45 error (2) 0 wit inspect .020 4.9
array-examples/standard_running_true-unreach-call.i timeout 0 wit inspect 900   4800 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .020 4.9
array-examples/standard_sentinel_true-unreach-call_true-termination.i true 2 wit inspect 5.5 310 42 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    990 true 2 wit inspect 5.3   260  
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_strcmp_true-unreach-call_ground.i timeout 0 wit inspect 900   6900 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_strcpy_original_true-unreach-call.i timeout 0 wit inspect 900   4800 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .031 4.8
array-examples/standard_strcpy_true-unreach-call_ground.i timeout 0 wit inspect 900   4700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_01_true-unreach-call.i timeout 0 wit inspect 900   4800 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .022 5.0
array-examples/standard_two_index_02_true-unreach-call.i timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_two_index_03_true-unreach-call.i timeout 0 wit inspect 900   5000 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .020 4.9
array-examples/standard_two_index_04_true-unreach-call.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_05_true-unreach-call.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_06_true-unreach-call.i timeout 0 wit inspect 900   4800 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_two_index_07_true-unreach-call.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .021 4.8
array-examples/standard_two_index_08_true-unreach-call.i timeout 0 wit inspect 900   5000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 5.0
array-examples/standard_two_index_09_true-unreach-call.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .019 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i timeout 0 wit inspect 900   3000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 4.8
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i timeout 0 wit inspect 900   4900 10000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .99 47 error (invalid witness file) 0 wit inspect .0018 .28 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i timeout 0 wit inspect 900   5200 7300 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i timeout 0 wit inspect 900   4900 12000 error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i timeout 0 wit inspect 900   5200 7100 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i timeout 0 wit inspect 900   5900 9900 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 900   4900 11000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0023 .26 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5200 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i timeout 0 wit inspect 900   5200 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .018 5.0
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 0 wit inspect 900   6000 8800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i timeout 0 wit inspect 900   4900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 5.0
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 900   6000 8500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout 0 wit inspect 900   6400 7600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 5.0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900   6400 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 46 error (2) 0 wit inspect .021 5.0
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 0 wit inspect 900   6200 6500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900   6000 8700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i timeout 0 wit inspect 900   2700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 5.0
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.9 480 84 true -32 wit inspect 4.4  260 false(unreach-call) 1 wit inspect 8.8   330   unknown 0 wit inspect 3.9  210 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 18   700 170 true -32 wit inspect 4.9  270 false(unreach-call) 1 wit inspect 47     3500   unknown 0 wit inspect 3.4  190 false(unreach-call) 1 wit inspect .79   19    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 39   1000 390 true -32 wit inspect 5.9  270 out of memory 0 wit inspect 41     7000   unknown 0 wit inspect 4.6  220 false(unreach-call) 1 wit inspect .63   20    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i timeout 0 wit inspect 900   1900 10000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i timeout 0 wit inspect 900   3300 8700 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0041 .29 - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 17   680 190 timeout 0 wit inspect 92    1900 false(unreach-call) 1 wit inspect 7.5   310   unknown 0 wit inspect 2.2  210 true -32 wit inspect .78   19    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i timeout 0 wit inspect 900   710 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 45 error (2) 0 wit inspect .020 5.0
reducercommutativity/avg10_true-unreach-call_true-termination.i timeout 0 wit inspect 900   960 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .022 4.8
reducercommutativity/avg20_true-unreach-call.i timeout 0 wit inspect 900   1500 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .017 4.9
reducercommutativity/avg40_true-unreach-call.i error (7) 0 wit inspect 310   4300 3700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .020 4.9
reducercommutativity/avg60_true-unreach-call.i error (7) 0 wit inspect 800   5000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .017 4.8
reducercommutativity/avg_true-unreach-call_true-termination.i timeout 0 wit inspect 900   510 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i timeout 0 wit inspect 900   11000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .019 4.8
reducercommutativity/max10_true-unreach-call_true-termination.i timeout 0 wit inspect 900   13000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 4.9
reducercommutativity/max20_true-unreach-call.i timeout 0 wit inspect 900   6200 15000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.8
reducercommutativity/max40_true-unreach-call.i timeout 0 wit inspect 900   7400 9400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.8
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 900   6800 7600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/max_true-unreach-call_true-termination.i timeout 0 wit inspect 900   2900 13000 - 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
reducercommutativity/sep05_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4600 7300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 4.9
reducercommutativity/sep10_true-unreach-call.i timeout 0 wit inspect 900   6100 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.8
reducercommutativity/sep20_true-unreach-call.i timeout 0 wit inspect 910   13000 8400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .018 4.9
reducercommutativity/sep40_true-unreach-call.i timeout 0 wit inspect 910   13000 8400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 44 error (2) 0 wit inspect .018 4.8
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 900   13000 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .019 5.0
reducercommutativity/sep_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1800 13000 - 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
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 40   2600 370 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    980 true 2 wit inspect 340     3100  
reducercommutativity/sum10_true-unreach-call_true-termination.i true 2 wit inspect 230   4500 2700 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     4800  
reducercommutativity/sum20_true-unreach-call.i timeout 0 wit inspect 900   5300 6400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .019 5.0
reducercommutativity/sum40_true-unreach-call.i timeout 0 wit inspect 900   5200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.9
reducercommutativity/sum60_true-unreach-call.i timeout 0 wit inspect 900   5600 8400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .020 4.9
reducercommutativity/sum_true-unreach-call_true-termination.i timeout 0 wit inspect 900   2000 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 47 error (2) 0 wit inspect .020 4.9
array-tiling/mlceu_false-unreach-call.i timeout 0 wit inspect 900   3100 11000 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i false(unreach-call) 1 wit inspect 5.2 290 43 timeout 0 wit inspect 92    1900 false(unreach-call) 1 wit inspect 15     300   unknown 0 wit inspect 3.2  210 true -32 wit inspect .75   18    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i timeout 0 wit inspect 900   880 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .020 4.8
array-tiling/mbpr3_true-unreach-call.i timeout 0 wit inspect 900   1100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 5.0
array-tiling/mbpr4_true-unreach-call.i timeout 0 wit inspect 900   920 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .021 4.9
array-tiling/mbpr5_true-unreach-call.i timeout 0 wit inspect 900   1100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .018 4.9
array-tiling/nr2_true-unreach-call.i timeout 0 wit inspect 900   2300 12000 - 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-tiling/nr3_true-unreach-call.i timeout 0 wit inspect 900   2500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .022 5.0
array-tiling/nr4_true-unreach-call.i timeout 0 wit inspect 900   1900 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.9
array-tiling/nr5_true-unreach-call.i timeout 0 wit inspect 900   2000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .022 4.9
array-tiling/pnr2_true-unreach-call.i timeout 0 wit inspect 900   1800 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .018 5.0
array-tiling/pnr3_true-unreach-call.i timeout 0 wit inspect 900   1700 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .020 4.9
array-tiling/pnr4_true-unreach-call.i timeout 0 wit inspect 900   2100 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.9
array-tiling/pnr5_true-unreach-call.i timeout 0 wit inspect 900   4700 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .018 5.0
array-tiling/poly1_true-unreach-call.i timeout 0 wit inspect 900   1300 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .018 5.0
array-tiling/poly2_true-unreach-call.i timeout 0 wit inspect 900   2700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 45 error (2) 0 wit inspect .019 4.8
array-tiling/pr2_true-unreach-call.i timeout 0 wit inspect 900   1200 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .018 5.0
array-tiling/pr3_true-unreach-call.i timeout 0 wit inspect 900   1200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .023 4.8
array-tiling/pr4_true-unreach-call.i timeout 0 wit inspect 900   970 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .018 4.8
array-tiling/pr5_true-unreach-call.i timeout 0 wit inspect 900   950 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .022 4.9
array-tiling/revcpyswp2_true-unreach-call.i timeout 0 wit inspect 900   5200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.8
array-tiling/rew_true-unreach-call.i timeout 0 wit inspect 900   1900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .033 4.8
array-tiling/rewnif_true-unreach-call.i timeout 0 wit inspect 900   2100 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .019 4.9
array-tiling/rewnifrev2_true-unreach-call.i timeout 0 wit inspect 900   2900 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .020 4.9
array-tiling/rewnifrev_true-unreach-call.i timeout 0 wit inspect 900   4300 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .024 5.0
array-tiling/rewrev_true-unreach-call.i timeout 0 wit inspect 900   2600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.9
array-tiling/skipped_true-unreach-call.i timeout 0 wit inspect 900   840 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .018 4.9
array-tiling/tcpy_true-unreach-call.i timeout 0 wit inspect 900   1800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.9
array-programs/copysome1_false-unreach-call.i timeout 0 wit inspect 900   4900 12000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0037 .30 - wit inspect - wit inspect
array-programs/copysome2_false-unreach-call.i timeout 0 wit inspect 900   5000 14000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
array-programs/copysome1_true-unreach-call.i timeout 0 wit inspect 900   4900 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .79 44 error (2) 0 wit inspect .019 4.9
array-programs/copysome2_true-unreach-call.i timeout 0 wit inspect 900   4900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .018 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 15 140000 720000 1800000 44 -96 220 6300 44 4 120 12000 44 0 56 2900 44 -61 3.7 110 123 4 2800 10000 123 8 1300 9300
    correct results 10 15 380 11000 4100 0 4 4 78 4500 0 3 3 2.1 58 2 4 12 770 4 8 360 3900
        correct true 5 10 290 8000 3200 0 0 0 0 2 4 12 770 4 8 360 3900
        correct false 5 5 89 3200 870 0 4 4 78 4500 0 3 3 2.1 58 0 0
    incorrect results 0 3 -96 15 800 0 0 2 -64 1.5 37 0 0
        incorrect true 0 3 -96 15 800 0 0 2 -64 1.5 37 0 0
        incorrect false 0 0 0 0 0 0 0
score (167 tasks, max score: 290) 15 -96 4 0 -61 4 8
Run set ukojak.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Arrays