Tool CPAchecker 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-12-05 07:52:24 CET 2017-12-05 13:10:09 CET 2017-12-05 13:34:02 CET 2017-12-05 13:37:41 CET 2017-12-05 13:41:35 CET 2017-12-05 12:37:13 CET 2017-12-05 13:13:01 CET
Run set interpchecker.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-Arrays
Options -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i timeout 0 wit inspect 900   5100 11000 error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0044 .34 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i timeout 0 wit inspect 900   5000 11000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .79 47 error (invalid witness file) 0 wit inspect .0034 .29 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i timeout 0 wit inspect 910   5000 12000 error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0039 .29 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i timeout 0 wit inspect 900   4800 10000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0044 .30 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i timeout 0 wit inspect 900   4900 12000 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .050 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0048 .35 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i timeout 0 wit inspect 910   4600 11000 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .043 4.8 error (invalid witness file) 0 wit inspect .86 51 error (invalid witness file) 0 wit inspect .0019 .26 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i timeout 0 wit inspect 900   4500 11000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .87 51 error (invalid witness file) 0 wit inspect .0045 .29 - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i timeout 0 wit inspect 900   4400 10000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0042 .31 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i timeout 0 wit inspect 900   4400 11000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0041 .31 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i timeout 0 wit inspect 900   4400 11000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .042 5.0 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0033 .32 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i timeout 0 wit inspect 900   4300 12000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i timeout 0 wit inspect 900   4200 11000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i timeout 0 wit inspect 900   4300 12000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0031 .30 - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i timeout 0 wit inspect 900   4200 11000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .83 48 error (invalid witness file) 0 wit inspect .0049 .29 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i timeout 0 wit inspect 900   4300 13000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .81 51 error (invalid witness file) 0 wit inspect .0038 .34 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i timeout 0 wit inspect 900   4200 11000 error (invalid witness file) 0 wit inspect .51 45 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .80 49 error (invalid witness file) 0 wit inspect .0041 .31 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i timeout 0 wit inspect 900   4500 13000 error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0035 .33 - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i timeout 0 wit inspect 900   4400 13000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .050 4.9 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0035 .32 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i timeout 0 wit inspect 900   4200 11000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .045 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i timeout 0 wit inspect 900   4000 12000 error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0041 .36 - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i timeout 0 wit inspect 900   4000 13000 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0040 .30 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i timeout 0 wit inspect 900   3900 12000 error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0036 .32 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i timeout 0 wit inspect 900   4000 11000 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .043 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0041 .34 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i timeout 0 wit inspect 900   3900 13000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0011 .30 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i timeout 0 wit inspect 900   4000 12000 error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .85 51 error (invalid witness file) 0 wit inspect .0039 .34 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i timeout 0 wit inspect 900   5100 13000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 51 error (invalid witness file) 0 wit inspect .0052 .26 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i timeout 0 wit inspect 900   4200 14000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i timeout 0 wit inspect 900   4100 12000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .040 4.8 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0042 .29 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i timeout 0 wit inspect 900   5000 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .022 4.8
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i timeout 0 wit inspect 900   5100 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .047 4.9
array-examples/relax_true-unreach-call.i timeout 0 wit inspect 900   5300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i timeout 0 wit inspect 900   5100 10000 - 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-examples/sanfoundry_10_true-unreach-call_ground.i timeout 0 wit inspect 900   4600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .019 5.0
array-examples/sanfoundry_24_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4300 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .018 5.0
array-examples/sanfoundry_27_true-unreach-call_ground.i timeout 0 wit inspect 900   5100 11000 - 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-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect 2.5 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  280 true 2 wit inspect 4.3   220  
array-examples/sorting_bubblesort_true-unreach-call_ground.i timeout 0 wit inspect 900   5000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .020 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .046 4.8
array-examples/standard_compareModified_true-unreach-call_ground.i timeout 0 wit inspect 900   4600 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .023 4.9
array-examples/standard_compare_true-unreach-call_ground.i timeout 0 wit inspect 900   5000 9900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 4.8
array-examples/standard_copy1_true-unreach-call_ground.i timeout 0 wit inspect 900   4500 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy2_true-unreach-call_ground.i timeout 0 wit inspect 900   4500 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .040 4.9
array-examples/standard_copy3_true-unreach-call_ground.i timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .047 5.0
array-examples/standard_copy4_true-unreach-call_ground.i timeout 0 wit inspect 900   4300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .031 4.8
array-examples/standard_copy5_true-unreach-call_ground.i timeout 0 wit inspect 900   4300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .052 4.9
array-examples/standard_copy6_true-unreach-call_ground.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .023 4.8
array-examples/standard_copy7_true-unreach-call_ground.i timeout 0 wit inspect 900   4100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .023 4.9
array-examples/standard_copy8_true-unreach-call_ground.i timeout 0 wit inspect 900   4100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .043 4.8
array-examples/standard_copy9_true-unreach-call_ground.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.9
array-examples/standard_copyInitSum2_true-unreach-call_ground.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.8
array-examples/standard_copyInitSum3_true-unreach-call_ground.i timeout 0 wit inspect 900   4000 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .017 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i timeout 0 wit inspect 900   4200 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .018 5.0
array-examples/standard_copyInit_true-unreach-call_ground.i timeout 0 wit inspect 900   4300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .048 4.8
array-examples/standard_find_true-unreach-call_ground.i timeout 0 wit inspect 900   4600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .018 4.9
array-examples/standard_init1_true-unreach-call_ground.i timeout 0 wit inspect 900   4500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 5.0
array-examples/standard_init2_true-unreach-call_ground.i timeout 0 wit inspect 900   4400 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.8
array-examples/standard_init3_true-unreach-call_ground.i timeout 0 wit inspect 900   4200 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9
array-examples/standard_init4_true-unreach-call_ground.i timeout 0 wit inspect 900   4000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .024 4.8
array-examples/standard_init5_true-unreach-call_ground.i timeout 0 wit inspect 900   4000 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .048 5.0
array-examples/standard_init6_true-unreach-call_ground.i timeout 0 wit inspect 900   3900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .049 4.8
array-examples/standard_init7_true-unreach-call_ground.i timeout 0 wit inspect 900   4000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 4.9
array-examples/standard_init8_true-unreach-call_ground.i timeout 0 wit inspect 900   3900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_init9_true-unreach-call_ground.i timeout 0 wit inspect 900   3900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .050 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i timeout 0 wit inspect 900   5100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .019 5.0
array-examples/standard_minInArray_true-unreach-call_ground.i timeout 0 wit inspect 900   5100 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .040 4.9
array-examples/standard_palindrome_true-unreach-call_ground.i timeout 0 wit inspect 900   4700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .025 5.0
array-examples/standard_partial_init_true-unreach-call_ground.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .052 4.9
array-examples/standard_partition_original_true-unreach-call_ground.i timeout 0 wit inspect 900   4600 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .025 4.8
array-examples/standard_partition_true-unreach-call_ground.i timeout 0 wit inspect 910   4200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 46 error (2) 0 wit inspect .018 4.8
array-examples/standard_password_true-unreach-call_ground.i timeout 0 wit inspect 900   5000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_reverse_true-unreach-call_ground.i timeout 0 wit inspect 900   4500 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .018 4.8
array-examples/standard_running_true-unreach-call.i timeout 0 wit inspect 900   4100 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .052 4.9
array-examples/standard_sentinel_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4800 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 0 wit inspect 900   4600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .018 4.8
array-examples/standard_strcmp_true-unreach-call_ground.i timeout 0 wit inspect 910   5000 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .77 44 error (2) 0 wit inspect .050 4.8
array-examples/standard_strcpy_original_true-unreach-call.i timeout 0 wit inspect 900   4500 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 46 error (2) 0 wit inspect .043 4.9
array-examples/standard_strcpy_true-unreach-call_ground.i timeout 0 wit inspect 900   4500 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .024 4.9
array-examples/standard_two_index_01_true-unreach-call.i timeout 0 wit inspect 900   4100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .050 4.9
array-examples/standard_two_index_02_true-unreach-call.i timeout 0 wit inspect 900   4300 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_03_true-unreach-call.i timeout 0 wit inspect 900   4300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .021 4.8
array-examples/standard_two_index_04_true-unreach-call.i timeout 0 wit inspect 900   4400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 4.8
array-examples/standard_two_index_05_true-unreach-call.i timeout 0 wit inspect 900   4500 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .047 4.9
array-examples/standard_two_index_06_true-unreach-call.i timeout 0 wit inspect 900   4600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .023 4.8
array-examples/standard_two_index_07_true-unreach-call.i timeout 0 wit inspect 900   4500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .049 5.0
array-examples/standard_two_index_08_true-unreach-call.i timeout 0 wit inspect 900   4500 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .022 4.8
array-examples/standard_two_index_09_true-unreach-call.i timeout 0 wit inspect 900   4500 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i timeout 0 wit inspect 900   4200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .019 4.8
array-examples/standard_vector_difference_true-unreach-call_ground.i timeout 0 wit inspect 900   4400 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .049 4.9
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i timeout 0 wit inspect 900   4000 11000 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .038 5.0 error (invalid witness file) 0 wit inspect .79 51 error (invalid witness file) 0 wit inspect .0039 .31 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i timeout 0 wit inspect 900   4000 12000 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0041 .30 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i timeout 0 wit inspect 900   4200 12000 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i timeout 0 wit inspect 900   4200 11000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .028 4.9 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i timeout 0 wit inspect 900   4200 12000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .90 47 error (invalid witness file) 0 wit inspect .0041 .35 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .50 44 error (2) 0 wit inspect .029 5.0 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0037 .30 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .025 4.8
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4300 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .024 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i timeout 0 wit inspect 900   4000 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .048 4.8
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 0 wit inspect 900   4100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i timeout 0 wit inspect 900   4500 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 900   4200 11000 - 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-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout 0 wit inspect 900   4300 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 4.9
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900   4100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 0 wit inspect 900   4000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .047 4.9
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900   4200 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .047 4.8
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i timeout 0 wit inspect 900   5000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .018 4.9
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 42   1500 380 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 45     4000   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 55   2400 490 true -32 wit inspect 4.0  280 out of memory 0 wit inspect 66     7000   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .64   20    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 360   3900 4500 true -32 wit inspect 4.8  280 out of memory 0 wit inspect 61     7000   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .65   20    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 220   3900 2900 true -32 wit inspect 5.5  280 out of memory 0 wit inspect 64     7000   unknown 0 wit inspect 4.6  230 false(unreach-call) 1 wit inspect .71   22    - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect 740   4400 8600 true -32 wit inspect 6.4  280 out of memory 0 wit inspect 73     7000   unknown 0 wit inspect 4.5  220 false(unreach-call) 1 wit inspect .80   24    - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 19   970 160 timeout 0 wit inspect 91    1900 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.8  210 error (1) 0 wit inspect .57   18    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 45   2000 380 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 true 2 wit inspect 6.0   270  
reducercommutativity/avg10_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 110   3700 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3300 true 2 wit inspect 5.9   290  
reducercommutativity/avg20_true-unreach-call.i timeout 0 wit inspect 900   4400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .024 5.0
reducercommutativity/avg40_true-unreach-call.i false(unreach-call) -16 wit inspect 210   3900 2500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  300 out of memory 0 wit inspect 61     7000  
reducercommutativity/avg60_true-unreach-call.i false(unreach-call) -16 wit inspect 790   4600 9100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  290 out of memory 0 wit inspect 66     7000  
reducercommutativity/avg_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 13   610 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 true 2 wit inspect 4.5   230  
reducercommutativity/max05_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4500 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 45 error (2) 0 wit inspect .040 4.9
reducercommutativity/max10_true-unreach-call_true-termination.i timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .044 5.0
reducercommutativity/max20_true-unreach-call.i timeout 0 wit inspect 900   4400 12000 - 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
reducercommutativity/max40_true-unreach-call.i false(unreach-call) -16 wit inspect 540   4100 6600 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  280 out of memory 0 wit inspect 65     7000  
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 900   4200 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0
reducercommutativity/max_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 31   1500 260 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 true 2 wit inspect 4.5   240  
reducercommutativity/sep05_true-unreach-call_true-termination.i true 2 wit inspect 160   3800 1800 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 timeout 0 wit inspect 960     1700  
reducercommutativity/sep10_true-unreach-call.i timeout 0 wit inspect 900   4500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .047 4.8
reducercommutativity/sep20_true-unreach-call.i timeout 0 wit inspect 900   4600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .050 4.9
reducercommutativity/sep40_true-unreach-call.i false(unreach-call) -16 wit inspect 640   4500 8500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0  280 out of memory 0 wit inspect 60     7000  
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 910   4200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/sep_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 390   4100 4900 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 true 2 wit inspect 6.0   290  
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 46   1600 310 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    970 true 2 wit inspect 340     3100  
reducercommutativity/sum10_true-unreach-call_true-termination.i true 2 wit inspect 110   3100 1400 - 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 true 2 wit inspect 690   4000 9000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 timeout 0 wit inspect 960     4600  
reducercommutativity/sum40_true-unreach-call.i false(unreach-call) -16 wit inspect 210   3900 2300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0  280 out of memory 0 wit inspect 68     7000  
reducercommutativity/sum60_true-unreach-call.i false(unreach-call) -16 wit inspect 800   4600 9100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6  280 out of memory 0 wit inspect 76     7000  
reducercommutativity/sum_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 9.2 470 76 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 true 2 wit inspect 5.0   230  
array-tiling/mlceu_false-unreach-call.i timeout 0 wit inspect 900   5100 14000 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .82 50 error (invalid witness file) 0 wit inspect .0039 .30 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i false(unreach-call) 0 wit inspect 160   3700 1900 true -32 wit inspect 4.7  280 out of memory 0 wit inspect 73     7000   unknown 0 wit inspect 3.8  220 true -32 wit inspect .64   20    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i false(unreach-call) -16 wit inspect 42   2200 330 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    2600 error (7) 0 wit inspect 100     730  
array-tiling/mbpr3_true-unreach-call.i false(unreach-call) -16 wit inspect 380   3900 4300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  280 out of memory 0 wit inspect 58     7000  
array-tiling/mbpr4_true-unreach-call.i false(unreach-call) -16 wit inspect 94   3700 900 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    4000 error (7) 0 wit inspect 100     1100  
array-tiling/mbpr5_true-unreach-call.i false(unreach-call) -16 wit inspect 650   4200 8000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  270 out of memory 0 wit inspect 58     7000  
array-tiling/nr2_true-unreach-call.i false(unreach-call) -16 wit inspect 520   4200 7700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  280 timeout 0 wit inspect 960     2700  
array-tiling/nr3_true-unreach-call.i false(unreach-call) -16 wit inspect 99   3700 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 true 2 wit inspect 380     1900  
array-tiling/nr4_true-unreach-call.i false(unreach-call) -16 wit inspect 430   4100 5600 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7  280 timeout 0 wit inspect 960     4700  
array-tiling/nr5_true-unreach-call.i false(unreach-call) -16 wit inspect 510   4300 6800 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 timeout 0 wit inspect 960     5100  
array-tiling/pnr2_true-unreach-call.i false(unreach-call) -16 wit inspect 77   3700 810 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit