Tool 2LS 0.6.0 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 11:20:26 CET 2017-12-01 07:32:03 CET 2017-12-01 08:01:50 CET 2017-12-01 08:11:41 CET 2017-12-01 08:15:34 CET 2017-12-01 04:23:32 CET 2017-12-01 07:36:49 CET
Run set 2ls.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Arrays
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.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/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.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/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/2ls.2017-11-30_1120.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 error (134) 0 wit inspect .093 22 .78 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i out of memory 0 wit inspect 31     15000 440    error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0013 .33 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i out of memory 0 wit inspect 33     15000 490    error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0015 .30 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i out of memory 0 wit inspect 33     15000 470    error (invalid witness file) 0 wit inspect .58 42 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 .0014 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i out of memory 0 wit inspect 33     15000 470    error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i out of memory 0 wit inspect 290     15000 2000    error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .92 47 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 360    error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 400    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .96 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 430    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .91 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 460    error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 390    error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0011 .35 - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 380    error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .91 49 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 420    error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  52 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 390    error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0011 .33 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 490    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0011 .30 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i out of memory 0 wit inspect 33     15000 440    error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.2  51 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i true -32 wit inspect 32     12000 400    timeout 0 wit inspect 92    1900 timeout 0 wit inspect 96     940   unknown 0 wit inspect .96 51 error (1) 0 wit inspect .068  9.0  - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 410    error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 400    error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0015 .30 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 390    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.0  49 error (invalid witness file) 0 wit inspect .0017 .30 - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 460    error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0015 .30 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 410    error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0012 .32 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 470    error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .96 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 470    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i out of memory 0 wit inspect 33     15000 480    error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i out of memory 0 wit inspect 320     15000 2200    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0012 .35 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i out of memory 0 wit inspect 31     15000 380    error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i out of memory 0 wit inspect 31     15000 370    error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i error (134) 0 wit inspect .11  22 .62 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .026 4.8
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i error (134) 0 wit inspect .078 22 .71 - 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/relax_true-unreach-call.i error (134) 0 wit inspect .18  26 1.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i out of memory 0 wit inspect 180     15000 1400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 5.0
array-examples/sanfoundry_10_true-unreach-call_ground.i out of memory 0 wit inspect 34     15000 390    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .022 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i true 2 wit inspect 17     5700 190    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  510 true 2 wit inspect 7.5   270  
array-examples/sanfoundry_27_true-unreach-call_ground.i out of memory 0 wit inspect 270     15000 2100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 5.0
array-examples/sanfoundry_43_true-unreach-call_ground.i error (134) 0 wit inspect .074 22 .82 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 5.0
array-examples/sorting_bubblesort_true-unreach-call_ground.i out of memory 0 wit inspect 31     15000 370    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .019 4.9
array-examples/sorting_selectionsort_true-unreach-call_ground.i out of memory 0 wit inspect 33     15000 520    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .032 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i out of memory 0 wit inspect 32     15000 450    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_compare_true-unreach-call_ground.i out of memory 0 wit inspect 150     15000 1300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .035 4.9
array-examples/standard_copy1_true-unreach-call_ground.i out of memory 0 wit inspect 33     15000 440    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .024 4.8
array-examples/standard_copy2_true-unreach-call_ground.i out of memory 0 wit inspect 34     15000 430    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .024 4.9
array-examples/standard_copy3_true-unreach-call_ground.i out of memory 0 wit inspect 33     15000 430    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy4_true-unreach-call_ground.i out of memory 0 wit inspect 33     15000 470    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .044 4.8
array-examples/standard_copy5_true-unreach-call_ground.i out of memory 0 wit inspect 33     15000 440    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_copy6_true-unreach-call_ground.i out of memory 0 wit inspect 33     15000 480    - 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
array-examples/standard_copy7_true-unreach-call_ground.i out of memory 0 wit inspect 33     15000 450    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy8_true-unreach-call_ground.i out of memory 0 wit inspect 33     15000 520    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .024 5.0
array-examples/standard_copy9_true-unreach-call_ground.i out of memory 0 wit inspect 33     15000 390    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_copyInitSum2_true-unreach-call_ground.i out of memory 0 wit inspect 32     15000 500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .018 5.0
array-examples/standard_copyInitSum3_true-unreach-call_ground.i out of memory 0 wit inspect 32     15000 420    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .023 4.9
array-examples/standard_copyInitSum_true-unreach-call_ground.i out of memory 0 wit inspect 32     15000 460    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .020 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i out of memory 0 wit inspect 32     15000 390    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9
array-examples/standard_find_true-unreach-call_ground.i true 2 wit inspect 40     15000 500    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 timeout 0 wit inspect 960     4700  
array-examples/standard_init1_true-unreach-call_ground.i true 2 wit inspect 32     12000 390    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 timeout 0 wit inspect 960     2000  
array-examples/standard_init2_true-unreach-call_ground.i out of memory 0 wit inspect 31     15000 380    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .024 4.8
array-examples/standard_init3_true-unreach-call_ground.i out of memory 0 wit inspect 31     15000 410    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .023 4.9
array-examples/standard_init4_true-unreach-call_ground.i out of memory 0 wit inspect 31     15000 470    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .021 5.0
array-examples/standard_init5_true-unreach-call_ground.i out of memory 0 wit inspect 31     15000 400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .050 4.9
array-examples/standard_init6_true-unreach-call_ground.i out of memory 0 wit inspect 31     15000 400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .025 4.9
array-examples/standard_init7_true-unreach-call_ground.i out of memory 0 wit inspect 31     15000 490    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .020 5.0
array-examples/standard_init8_true-unreach-call_ground.i out of memory 0 wit inspect 31     15000 440    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_init9_true-unreach-call_ground.i out of memory 0 wit inspect 31     15000 450    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i out of memory 0 wit inspect 260     15000 1900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .024 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i out of memory 0 wit inspect 310     15000 2100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .024 4.9
array-examples/standard_palindrome_true-unreach-call_ground.i out of memory 0 wit inspect 34     15000 420    - 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_partial_init_true-unreach-call_ground.i out of memory 0 wit inspect 31     15000 400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i out of memory 0 wit inspect 29     15000 370    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .018 5.0
array-examples/standard_partition_true-unreach-call_ground.i out of memory 0 wit inspect 31     15000 400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_password_true-unreach-call_ground.i out of memory 0 wit inspect 150     15000 1400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.9
array-examples/standard_reverse_true-unreach-call_ground.i out of memory 0 wit inspect 33     15000 510    - 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_running_true-unreach-call.i out of memory 0 wit inspect 31     15000 510    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .048 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i out of memory 0 wit inspect 110     15000 880    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .048 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i out of memory 0 wit inspect 34     15000 420    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_strcmp_true-unreach-call_ground.i false(unreach-call) -16 wit inspect 75     11000 870    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2300 true 2 wit inspect 5.6   290  
array-examples/standard_strcpy_original_true-unreach-call.i out of memory 0 wit inspect 33     15000 410    - 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_strcpy_true-unreach-call_ground.i out of memory 0 wit inspect 33     15000 420    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_two_index_01_true-unreach-call.i out of memory 0 wit inspect 250     15000 1600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_two_index_02_true-unreach-call.i out of memory 0 wit inspect 34     15000 440    - 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
array-examples/standard_two_index_03_true-unreach-call.i out of memory 0 wit inspect 240     15000 1800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .035 4.8
array-examples/standard_two_index_04_true-unreach-call.i out of memory 0 wit inspect 33     15000 480    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_05_true-unreach-call.i out of memory 0 wit inspect 34     15000 430    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .023 5.0
array-examples/standard_two_index_06_true-unreach-call.i out of memory 0 wit inspect 240     15000 1700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .021 4.9
array-examples/standard_two_index_07_true-unreach-call.i out of memory 0 wit inspect 34     15000 420    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .024 4.8
array-examples/standard_two_index_08_true-unreach-call.i out of memory 0 wit inspect 34     15000 420    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 5.0
array-examples/standard_two_index_09_true-unreach-call.i out of memory 0 wit inspect 34     15000 430    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .048 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i out of memory 0 wit inspect 170     15000 1200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 46 error (2) 0 wit inspect .020 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i out of memory 0 wit inspect 32     15000 400    - 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-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i out of memory 0 wit inspect 32     15000 380    error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .83 48 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i out of memory 0 wit inspect 34     15000 500    error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0011 .35 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i out of memory 0 wit inspect 26     15000 330    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i true -32 wit inspect 38     15000 460    timeout 0 wit inspect 92    2500 timeout 0 wit inspect 97     4800   unknown 0 wit inspect .95 51 error (1) 0 wit inspect .066  9.0  - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i out of memory 0 wit inspect 26     15000 340    error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .93 51 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i error (134) 0 wit inspect .079 23 .65 error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i out of memory 0 wit inspect 29     15000 370    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 5.0
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i out of memory 0 wit inspect 30     15000 370    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 46 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i true 2 wit inspect 36     13000 390    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 timeout 0 wit inspect 960     4900  
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i error (5) 0 wit inspect 110     7000 820    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i error (134) 0 wit inspect .16  24 1.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i error (5) 0 wit inspect 100     7000 830    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .024 4.9
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i out of memory 0 wit inspect 34     15000 440    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 5.0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i out of memory 0 wit inspect 26     15000 320    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 45 error (2) 0 wit inspect .020 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i error (5) 0 wit inspect 130     11000 1200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .024 4.9
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i true 2 wit inspect 29     12000 360    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 timeout 0 wit inspect 960     5900  
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i timeout 0 wit inspect 900     14000 3700    - 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
reducercommutativity/rangesum05_false-unreach-call_true-termination.i error (134) 0 wit inspect .089 22 .64 error (invalid witness file) 0 wit inspect .53 43 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 .0014 .31 - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i error (134) 0 wit inspect .11  22 .64 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .99 49 error (invalid witness file) 0 wit inspect .0030 .26 - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i error (134) 0 wit inspect .092 22 .76 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i error (134) 0 wit inspect .094 22 .82 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i error (134) 0 wit inspect .11  23 .63 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .81 48 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i error (134) 0 wit inspect .097 22 .63 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i true 2 wit inspect 110     360 1300    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 860    7000 timeout 0 wit inspect 960     4600  
reducercommutativity/avg10_true-unreach-call_true-termination.i timeout 0 wit inspect 900     710 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .019 4.8
reducercommutativity/avg20_true-unreach-call.i timeout 0 wit inspect 900     810 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .021 5.0
reducercommutativity/avg40_true-unreach-call.i timeout 0 wit inspect 900     890 7700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/avg60_true-unreach-call.i timeout 0 wit inspect 900     1000 8800    - 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
reducercommutativity/avg_true-unreach-call_true-termination.i timeout 0 wit inspect 900     1600 7200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 46 error (2) 0 wit inspect .020 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 6.0   89 85    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     4100  
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 300     480 3800    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     3400  
reducercommutativity/max20_true-unreach-call.i timeout 0 wit inspect 900     1000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9
reducercommutativity/max40_true-unreach-call.i timeout 0 wit inspect 900     1400 9000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .031 4.8
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 900     1900 5600    - 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
reducercommutativity/max_true-unreach-call_true-termination.i timeout 0 wit inspect 900     2500 3700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .019 4.9
reducercommutativity/sep05_true-unreach-call_true-termination.i true 2 wit inspect 2.1   69 24    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 timeout 0 wit inspect 960     1700  
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect 3.3   100 41    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 920     7000  
reducercommutativity/sep20_true-unreach-call.i true 2 wit inspect 12     280 120    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3000 timeout 0 wit inspect 910     7000  
reducercommutativity/sep40_true-unreach-call.i timeout 0 wit inspect 900     1400 9300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 5.0
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 900     2200 9400    - 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
reducercommutativity/sep_true-unreach-call_true-termination.i timeout 0 wit inspect 900     10000 7000    - 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
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 20     170 270    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 380     3200  
reducercommutativity/sum10_true-unreach-call_true-termination.i timeout 0 wit inspect 900     760 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.9
reducercommutativity/sum20_true-unreach-call.i timeout 0 wit inspect 900     720 8100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9
reducercommutativity/sum40_true-unreach-call.i timeout 0 wit inspect 900     860 8600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.8
reducercommutativity/sum60_true-unreach-call.i timeout 0 wit inspect 900     1000 6100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .020 5.0
reducercommutativity/sum_true-unreach-call_true-termination.i timeout 0 wit inspect 900     1900 8000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.8
array-tiling/mlceu_false-unreach-call.i out of memory 0 wit inspect 670     15000 3200    error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i false(unreach-call) 1 wit inspect .33  38 3.4  false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 15     300   unknown 0 wit inspect 2.9  190 true -32 wit inspect .77   18    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i out of memory 0 wit inspect 510     15000 2500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .021 4.8
array-tiling/mbpr3_true-unreach-call.i out of memory 0 wit inspect 410     15000 2000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .022 4.8
array-tiling/mbpr4_true-unreach-call.i out of memory 0 wit inspect 440     15000 2600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 5.0
array-tiling/mbpr5_true-unreach-call.i timeout 0 wit inspect 900     12000 4400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 42 error (2) 0 wit inspect .019 4.8
array-tiling/nr2_true-unreach-call.i out of memory 0 wit inspect 680     15000 3300    - 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-tiling/nr3_true-unreach-call.i out of memory 0 wit inspect 490     15000 4500    - 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-tiling/nr4_true-unreach-call.i out of memory 0 wit inspect 400     15000 2100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9
array-tiling/nr5_true-unreach-call.i out of memory 0 wit inspect 590     15000 4100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 5.0
array-tiling/pnr2_true-unreach-call.i out of memory 0 wit inspect 560     15000 3500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .017 4.9
array-tiling/pnr3_true-unreach-call.i out of memory 0 wit inspect 580     15000 2700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .019 4.8
array-tiling/pnr4_true-unreach-call.i out of memory 0 wit inspect 530     15000 1800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .021 4.8
array-tiling/pnr5_true-unreach-call.i out of memory 0 wit inspect 350     15000 1800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .018 4.9
array-tiling/poly1_true-unreach-call.i timeout 0 wit inspect 900     10000 4200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .83 44 error (2) 0 wit inspect .019 4.8
array-tiling/poly2_true-unreach-call.i timeout 0 wit inspect 900     11000 4700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .017 4.8
array-tiling/pr2_true-unreach-call.i out of memory 0 wit inspect 460     15000 2800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .022 5.0
array-tiling/pr3_true-unreach-call.i out of memory 0 wit inspect 380     15000 2100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 4.8
array-tiling/pr4_true-unreach-call.i out of memory 0 wit inspect 400     15000 2100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.9
array-tiling/pr5_true-unreach-call.i out of memory 0 wit inspect 280     15000 2100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .019 4.8
array-tiling/revcpyswp2_true-unreach-call.i timeout 0 wit inspect 900     11000 5500    - 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-tiling/rew_true-unreach-call.i out of memory 0 wit inspect 540     15000 2900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .019 4.8
array-tiling/rewnif_true-unreach-call.i out of memory 0 wit inspect 500     15000 3300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.9
array-tiling/rewnifrev2_true-unreach-call.i out of memory 0 wit inspect 610     15000 4700    - 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
array-tiling/rewnifrev_true-unreach-call.i out of memory 0 wit inspect 560     15000 3900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .023 4.9
array-tiling/rewrev_true-unreach-call.i out of memory 0 wit inspect 580     15000 3300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .024 4.8
array-tiling/skipped_true-unreach-call.i out of memory 0 wit inspect 780     15000 2800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9
array-tiling/tcpy_true-unreach-call.i timeout 0 wit inspect 900     14000 6500    - 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-programs/copysome1_false-unreach-call.i out of memory 0 wit inspect 25     15000 310    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 .0020 .26 - wit inspect - wit inspect
array-programs/copysome2_false-unreach-call.i out of memory 0 wit inspect 27     15000 340    error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0013 .34 - wit inspect - wit inspect
array-programs/copysome1_true-unreach-call.i out of memory 0 wit inspect 25     15000 340    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8
array-programs/copysome2_true-unreach-call.i out of memory 0 wit inspect 27     15000 380    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .036 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 -55 38000    1900000 300000   44 1 210   6400 44 1 210 6200 44 0 43 2300 44 -32 .96 48 123 2 11000   54000 123 6 9900 50000
    correct results 13 25 600    60000 7500   1 1 3.1 260 1 1 15 300 0 0 1 2 6.9 510 3 6 400 3800
        correct true 12 24 600    60000 7500   0 0 0 0 1 2 6.9 510 3 6 400 3800
        correct false 1 1 .33 38 3.4 1 1 3.1 260 1 1 15 300 0 0 0 0
    incorrect results 3 -80 150    38000 1700   0 0 0 1 -32 .77 18 0 0
        incorrect true 2 -64 71    27000 860   0 0 0 1 -32 .77 18 0 0
        incorrect false 1 -16 75    11000 870   0 0 0 0 0 0
score (167 tasks, max score: 290) -55 1 1 0 -32 2 6
Run set 2ls.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Arrays