Tool CBMC 5.8 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:26:01 CET 2017-12-01 07:56:00 CET 2017-12-01 08:08:00 CET 2017-12-01 08:15:34 CET 2017-12-01 04:22:29 CET 2017-12-01 07:31:28 CET
Run set cbmc.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Arrays
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cbmc.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 (6) 0 wit inspect 160    14000 1700   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .84 48 error (invalid witness file) 0 wit inspect .0013 .32 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i out of memory 0 wit inspect 23    15000 370   error (invalid witness file) 0 wit inspect .57 43 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 .0018 .26 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i out of memory 0 wit inspect 23    15000 300   error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .90 47 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i error (134) 0 wit inspect 62    13000 780   error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i error (134) 0 wit inspect 77    13000 1000   error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .97 50 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i error (6) 0 wit inspect 420    10000 2500   error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect 1.1  51 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i out of memory 0 wit inspect 100    15000 1300   error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i out of memory 0 wit inspect 120    15000 1900   error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i out of memory 0 wit inspect 130    15000 1800   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .91 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i error (134) 0 wit inspect 95    15000 1300   error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0013 .31 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i out of memory 0 wit inspect 100    15000 1200   error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i out of memory 0 wit inspect 110    15000 1500   error (invalid witness file) 0 wit inspect .53 45 error (2) 0 wit inspect .025 5.0 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i out of memory 0 wit inspect 120    15000 1900   error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i error (134) 0 wit inspect 65    14000 970   error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .91 47 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i error (134) 0 wit inspect 70    15000 910   error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .95 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i out of memory 0 wit inspect 72    15000 980   error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .86 51 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i out of memory 0 wit inspect 100    15000 1500   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i out of memory 0 wit inspect 61    15000 790   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i out of memory 0 wit inspect 64    15000 840   error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .86 51 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i out of memory 0 wit inspect 67    15000 1100   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .021 5.0 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/standard_init5_false-unreach-call_ground.i out of memory 0 wit inspect 71    15000 1000   error (invalid witness file) 0 wit inspect .53 46 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .94 49 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i out of memory 0 wit inspect 74    15000 980   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .92 51 error (invalid witness file) 0 wit inspect .0042 .26 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i out of memory 0 wit inspect 52    15000 790   error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .88 51 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i out of memory 0 wit inspect 54    15000 660   error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .026 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i out of memory 0 wit inspect 56    15000 680   error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .90 47 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i error (42) 0 wit inspect 870    1400 3800   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.1  47 error (invalid witness file) 0 wit inspect .0012 .31 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i error (134) 0 wit inspect 65    14000 710   error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i out of memory 0 wit inspect 88    15000 1300   error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i error (42) 0 wit inspect 870    1500 4900   - 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
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i error (134) 0 wit inspect 26    13000 420   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .021 4.9
array-examples/relax_true-unreach-call.i error (6) 0 wit inspect 690    14000 3800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .023 4.9
array-examples/sanfoundry_02_true-unreach-call_ground.i error (42) 0 wit inspect 870    2600 4400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i error (134) 0 wit inspect 28    13000 400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .018 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    4200 9100   - 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
array-examples/sanfoundry_27_true-unreach-call_ground.i error (42) 0 wit inspect 870    1400 4100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 46 error (2) 0 wit inspect .018 4.9
array-examples/sanfoundry_43_true-unreach-call_ground.i out of memory 0 wit inspect 93    15000 1200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .026 4.8
array-examples/sorting_bubblesort_true-unreach-call_ground.i out of memory 0 wit inspect 20    15000 250   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .020 4.9
array-examples/sorting_selectionsort_true-unreach-call_ground.i error (134) 0 wit inspect 74    13000 820   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i error (6) 0 wit inspect 120    15000 1800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_compare_true-unreach-call_ground.i error (42) 0 wit inspect 870    1500 3800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .052 4.9
array-examples/standard_copy1_true-unreach-call_ground.i out of memory 0 wit inspect 68    15000 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .048 4.8
array-examples/standard_copy2_true-unreach-call_ground.i out of memory 0 wit inspect 81    15000 1000   - 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_copy3_true-unreach-call_ground.i out of memory 0 wit inspect 92    15000 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .047 4.8
array-examples/standard_copy4_true-unreach-call_ground.i out of memory 0 wit inspect 100    15000 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 46 error (2) 0 wit inspect .025 4.8
array-examples/standard_copy5_true-unreach-call_ground.i error (134) 0 wit inspect 82    15000 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_copy6_true-unreach-call_ground.i out of memory 0 wit inspect 91    15000 1200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 5.0
array-examples/standard_copy7_true-unreach-call_ground.i out of memory 0 wit inspect 99    15000 1200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8
array-examples/standard_copy8_true-unreach-call_ground.i error (134) 0 wit inspect 82    15000 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .042 4.9
array-examples/standard_copy9_true-unreach-call_ground.i error (134) 0 wit inspect 62    14000 730   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .023 5.0
array-examples/standard_copyInitSum2_true-unreach-call_ground.i out of memory 0 wit inspect 72    15000 900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .025 4.8
array-examples/standard_copyInitSum3_true-unreach-call_ground.i out of memory 0 wit inspect 75    15000 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .025 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i out of memory 0 wit inspect 72    15000 1000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .019 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i out of memory 0 wit inspect 69    15000 900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .021 4.9
array-examples/standard_find_true-unreach-call_ground.i out of memory 0 wit inspect 100    15000 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 45 error (2) 0 wit inspect .023 5.0
array-examples/standard_init1_true-unreach-call_ground.i out of memory 0 wit inspect 100    15000 1400   - 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-examples/standard_init2_true-unreach-call_ground.i out of memory 0 wit inspect 61    15000 860   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .050 5.0
array-examples/standard_init3_true-unreach-call_ground.i out of memory 0 wit inspect 64    15000 880   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_init4_true-unreach-call_ground.i out of memory 0 wit inspect 67    15000 910   - 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-examples/standard_init5_true-unreach-call_ground.i out of memory 0 wit inspect 71    15000 1000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_init6_true-unreach-call_ground.i out of memory 0 wit inspect 74    15000 990   - 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-examples/standard_init7_true-unreach-call_ground.i out of memory 0 wit inspect 52    15000 700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .023 4.8
array-examples/standard_init8_true-unreach-call_ground.i out of memory 0 wit inspect 54    15000 730   - 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-examples/standard_init9_true-unreach-call_ground.i out of memory 0 wit inspect 56    15000 730   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .021 4.9
array-examples/standard_maxInArray_true-unreach-call_ground.i error (42) 0 wit inspect 870    1400 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 5.0
array-examples/standard_minInArray_true-unreach-call_ground.i error (42) 0 wit inspect 870    1400 3900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .021 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i out of memory 0 wit inspect 100    15000 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .018 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i error (134) 0 wit inspect 90    13000 870   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .020 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i error (134) 0 wit inspect 74    14000 880   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.9
array-examples/standard_partition_true-unreach-call_ground.i error (134) 0 wit inspect 66    14000 810   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 5.0
array-examples/standard_password_true-unreach-call_ground.i error (42) 0 wit inspect 870    1500 3500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_reverse_true-unreach-call_ground.i out of memory 0 wit inspect 110    15000 1500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .026 4.8
array-examples/standard_running_true-unreach-call.i out of memory 0 wit inspect 88    15000 1100   - 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-examples/standard_sentinel_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    3900 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i out of memory 0 wit inspect 100    15000 1400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.9
array-examples/standard_strcmp_true-unreach-call_ground.i error (42) 0 wit inspect 870    3500 5500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 46 error (2) 0 wit inspect .018 4.8
array-examples/standard_strcpy_original_true-unreach-call.i out of memory 0 wit inspect 73    15000 940   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .020 4.8
array-examples/standard_strcpy_true-unreach-call_ground.i out of memory 0 wit inspect 73    15000 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_01_true-unreach-call.i out of memory 0 wit inspect 96    15000 1100   - 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-examples/standard_two_index_02_true-unreach-call.i out of memory 0 wit inspect 68    15000 890   - 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-examples/standard_two_index_03_true-unreach-call.i out of memory 0 wit inspect 96    15000 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_two_index_04_true-unreach-call.i out of memory 0 wit inspect 68    15000 890   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .017 4.9
array-examples/standard_two_index_05_true-unreach-call.i out of memory 0 wit inspect 68    15000 950   - 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-examples/standard_two_index_06_true-unreach-call.i out of memory 0 wit inspect 96    15000 1400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .023 4.8
array-examples/standard_two_index_07_true-unreach-call.i out of memory 0 wit inspect 68    15000 860   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9
array-examples/standard_two_index_08_true-unreach-call.i out of memory 0 wit inspect 68    15000 880   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.8
array-examples/standard_two_index_09_true-unreach-call.i out of memory 0 wit inspect 68    15000 900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .020 4.9
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i error (42) 0 wit inspect 870    4500 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .022 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i error (6) 0 wit inspect 120    15000 1600   - 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-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i out of memory 0 wit inspect 60    15000 770   error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i out of memory 0 wit inspect 410    15000 3800   error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i out of memory 0 wit inspect 71    15000 930   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .032 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i out of memory 0 wit inspect 440    15000 6400   error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i out of memory 0 wit inspect 71    15000 960   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i error (134) 0 wit inspect 23    12000 300   error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i out of memory 0 wit inspect 100    15000 1300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i out of memory 0 wit inspect 120    15000 1500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i out of memory 0 wit inspect 250    15000 2500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .021 4.8
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i out of memory 0 wit inspect 280    15000 3900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 5.0
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i out of memory 0 wit inspect 150    15000 1800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .026 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i out of memory 0 wit inspect 290    15000 3300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i out of memory 0 wit inspect 560    15000 8100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .024 4.9
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i out of memory 0 wit inspect 130    15000 1700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .018 4.8
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i out of memory 0 wit inspect 430    15000 5200   - 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-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i out of memory 0 wit inspect 200    15000 2500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    5600 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .020 4.9
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .67 34 6.4 unknown 0 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 11     340   unknown 0 wit inspect 4.5  220 error (2) 0 wit inspect .67   19    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.1  34 9.8 unknown 0 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 51     4000   unknown 0 wit inspect 4.6  220 error (2) 0 wit inspect .86   19    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 0 wit inspect 2.0  35 26   unknown 0 wit inspect 4.3  270 out of memory 0 wit inspect 55     7000   unknown 0 wit inspect 4.7  230 error (2) 0 wit inspect .74   20    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 0 wit inspect 4.9  41 61   unknown 0 wit inspect 6.2  280 out of memory 0 wit inspect 84     7000   unknown 0 wit inspect 6.1  300 error (2) 0 wit inspect 1.1    22    - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 0 wit inspect 8.9  59 110   unknown 0 wit inspect 5.6  320 out of memory 0 wit inspect 62     7000   unknown 0 wit inspect 7.4  340 error (2) 0 wit inspect 1.2    23    - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .96 58 12   true -32 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 11     360   unknown 0 wit inspect 3.8  220 true -32 wit inspect .65   19    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i true 2 wit inspect 35    51 500   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2300 timeout 0 wit inspect 960     5200  
reducercommutativity/avg10_true-unreach-call_true-termination.i true 2 wit inspect 530    180 6000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 timeout 0 wit inspect 960     6400  
reducercommutativity/avg20_true-unreach-call.i error (42) 0 wit inspect 870    280 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.9
reducercommutativity/avg40_true-unreach-call.i error (42) 0 wit inspect 870    300 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9
reducercommutativity/avg60_true-unreach-call.i error (42) 0 wit inspect 870    350 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .024 5.0
reducercommutativity/avg_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    220 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .049 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 2.4  35 27   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 6.5  270 timeout 0 wit inspect 960     1500  
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 87    66 970   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 9.0  300 timeout 0 wit inspect 960     3200  
reducercommutativity/max20_true-unreach-call.i error (42) 0 wit inspect 870    200 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9
reducercommutativity/max40_true-unreach-call.i error (42) 0 wit inspect 870    230 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.9
reducercommutativity/max60_true-unreach-call.i error (42) 0 wit inspect 870    260 9500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .023 4.9
reducercommutativity/max_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    230 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .021 5.0
reducercommutativity/sep05_true-unreach-call_true-termination.i true 2 wit inspect .93 35 8.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 430    1400 timeout 0 wit inspect 960     1800  
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect 1.5  38 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 out of memory 0 wit inspect 850     7000  
reducercommutativity/sep20_true-unreach-call.i true 2 wit inspect 4.8  48 59   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 timeout 0 wit inspect 960     6500  
reducercommutativity/sep40_true-unreach-call.i true 2 wit inspect 35    87 490   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2400 timeout 0 wit inspect 960     4600  
reducercommutativity/sep60_true-unreach-call.i true 2 wit inspect 150    160 2100   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5800 timeout 0 wit inspect 960     3500  
reducercommutativity/sep_true-unreach-call_true-termination.i error (42) 0 wit inspect 880    9700 4300   - 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
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 4.7  39 56   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    990 true 2 wit inspect 350     3200  
reducercommutativity/sum10_true-unreach-call_true-termination.i true 2 wit inspect 180    130 2200   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     5100  
reducercommutativity/sum20_true-unreach-call.i error (42) 0 wit inspect 870    270 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .018 5.0
reducercommutativity/sum40_true-unreach-call.i error (42) 0 wit inspect 870    270 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.8
reducercommutativity/sum60_true-unreach-call.i error (42) 0 wit inspect 870    270 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .020 5.0
reducercommutativity/sum_true-unreach-call_true-termination.i error (42) 0 wit inspect 870    220 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 4.8
array-tiling/mlceu_false-unreach-call.i error (42) 0 wit inspect 870    5800 8700   error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .91 48 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i false(unreach-call) 1 wit inspect .26 33 2.8 false(unreach-call) 1 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 7.9   260   unknown 0 wit inspect 3.0  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i error (134) 0 wit inspect 81    13000 690   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.9
array-tiling/mbpr3_true-unreach-call.i error (134) 0 wit inspect 230    13000 1400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .019 4.8
array-tiling/mbpr4_true-unreach-call.i error (134) 0 wit inspect 210    13000 2000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.8
array-tiling/mbpr5_true-unreach-call.i error (134) 0 wit inspect 150    14000 1400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .018 4.8
array-tiling/nr2_true-unreach-call.i error (134) 0 wit inspect 60    14000 720   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .018 4.8
array-tiling/nr3_true-unreach-call.i error (134) 0 wit inspect 56    13000 660   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9
array-tiling/nr4_true-unreach-call.i error (134) 0 wit inspect 84    13000 960   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.8
array-tiling/nr5_true-unreach-call.i error (134) 0 wit inspect 110    13000 870   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .020 4.9
array-tiling/pnr2_true-unreach-call.i error (134) 0 wit inspect 660    13000 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9
array-tiling/pnr3_true-unreach-call.i error (42) 0 wit inspect 870    3700 4500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8
array-tiling/pnr4_true-unreach-call.i error (42) 0 wit inspect 870    6200 5600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 5.0
array-tiling/pnr5_true-unreach-call.i error (42) 0 wit inspect 870    2700 5800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .017 4.9
array-tiling/poly1_true-unreach-call.i error (42) 0 wit inspect 880    11000 7500   - 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/poly2_true-unreach-call.i error (134) 0 wit inspect 160    13000 1600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .019 4.9
array-tiling/pr2_true-unreach-call.i error (134) 0 wit inspect 130    13000 1700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .020 5.0
array-tiling/pr3_true-unreach-call.i error (134) 0 wit inspect 220    13000 1800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .030 5.0
array-tiling/pr4_true-unreach-call.i error (134) 0 wit inspect 280    13000 2300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .76 41 error (2) 0 wit inspect .019 4.8
array-tiling/pr5_true-unreach-call.i error (42) 0 wit inspect 880    9500 3900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .020 4.8
array-tiling/revcpyswp2_true-unreach-call.i error (42) 0 wit inspect 870    1400 5600   - 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-tiling/rew_true-unreach-call.i error (134) 0 wit inspect 470    14000 3500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .048 4.9
array-tiling/rewnif_true-unreach-call.i error (134) 0 wit inspect 660    14000 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.8
array-tiling/rewnifrev2_true-unreach-call.i error (6) 0 wit inspect 130    14000 1100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .017 4.8
array-tiling/rewnifrev_true-unreach-call.i error (134) 0 wit inspect 130    14000 1300   - 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-tiling/rewrev_true-unreach-call.i error (134) 0 wit inspect 120    14000 1500   - 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-tiling/skipped_true-unreach-call.i error (134) 0 wit inspect 560    14000 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .018 4.8
array-tiling/tcpy_true-unreach-call.i error (42) 0 wit inspect 870    1000 4200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 45 error (2) 0 wit inspect .019 4.9
array-programs/copysome1_false-unreach-call.i error (134) 0 wit inspect 130    15000 1500   error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-programs/copysome2_false-unreach-call.i error (134) 0 wit inspect 130    14000 1800   error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .95 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-programs/copysome1_true-unreach-call.i error (134) 0 wit inspect 130    15000 2100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .77 42 error (2) 0 wit inspect .024 4.8
array-programs/copysome2_true-unreach-call.i error (134) 0 wit inspect 130    14000 1700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 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 26 46000   1800000 440000 44 -31 52   3500 44 4 280 26000 44 0 68 3500 44 -64 5.9 150 123 2 7700 30000 123 2 9900 49000
    correct results 15 26 1000   1000 13000 1 1 3.7 270 4 4 81 5000 0 0 1 2 430 1400 1 2 350 3200
        correct true 11 22 1000   860 12000 0 0 0 0 1 2 430 1400 1 2 350 3200
        correct false 4 4 2.9 160 31 1 1 3.7 270 4 4 81 5000 0 0 0 0
    correct-unconfimed results 3 0 16   130 200 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 3 0 16   130 200 0 0 0 0 0 0
    incorrect results 0 1 -32 3.9 260 0 0 2 -64 1.2 37 0 0
        incorrect true 0 1 -32 3.9 260 0 0 2 -64 1.2 37 0 0
        incorrect false 0 0 0 0 0 0 0
score (167 tasks, max score: 290) 26 -31 4 0 -64 2 2
Run set cbmc.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Arrays