Tool CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:36:48 CET 2017-12-01 08:27:40 CET 2017-12-01 08:32:13 CET 2017-12-01 08:39:14 CET 2017-12-01 04:24:39 CET 2017-12-01 07:43:13 CET
Run set cpa-bam-slicing.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Arrays
Options -ldv-bam-svcomp -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-slicing.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 0 wit inspect 2.5 260 25 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i error 0 wit inspect 2.5 260 22 error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i error 0 wit inspect 2.5 270 23 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .017 5.0 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i error 0 wit inspect 2.6 260 22 error (invalid witness file) 0 wit inspect .53 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 .0013 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i error 0 wit inspect 2.5 260 21 error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i error 0 wit inspect 2.5 270 21 error (invalid witness file) 0 wit inspect .53 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 .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i error 0 wit inspect 2.5 270 19 error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 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 error 0 wit inspect 2.5 270 22 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i error 0 wit inspect 2.6 270 26 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i error 0 wit inspect 2.5 270 21 error (invalid witness file) 0 wit inspect .59 44 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 .27 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i error 0 wit inspect 2.7 270 24 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i error 0 wit inspect 2.6 270 24 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i error 0 wit inspect 2.6 260 23 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i error 0 wit inspect 2.6 260 25 error (invalid witness file) 0 wit inspect .60 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 .0016 .26 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i error 0 wit inspect 2.5 260 26 error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0017 .30 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i error 0 wit inspect 2.7 270 26 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i error 0 wit inspect 2.5 260 21 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i error 0 wit inspect 2.6 270 25 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i error 0 wit inspect 2.5 270 23 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0011 .33 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i error 0 wit inspect 2.5 270 23 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 5.0 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_init5_false-unreach-call_ground.i error 0 wit inspect 2.4 270 22 error (invalid witness file) 0 wit inspect .57 46 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i error 0 wit inspect 2.6 260 25 error (invalid witness file) 0 wit inspect .55 43 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 .26 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i error 0 wit inspect 2.7 270 21 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i error 0 wit inspect 2.5 270 22 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i error 0 wit inspect 2.5 270 22 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i error 0 wit inspect 2.6 270 24 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i error 0 wit inspect 2.5 270 21 error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .81 50 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i error 0 wit inspect 2.5 270 21 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i error 0 wit inspect 2.6 260 26 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 45 error (2) 0 wit inspect .021 4.8
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i error 0 wit inspect 2.6 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 4.8
array-examples/relax_true-unreach-call.i unknown 0 wit inspect 5.7 310 48 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .024 4.9
array-examples/sanfoundry_02_true-unreach-call_ground.i error 0 wit inspect 2.6 260 25 - 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/sanfoundry_10_true-unreach-call_ground.i timeout 0 wit inspect 900   4100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.9
array-examples/sanfoundry_24_true-unreach-call_true-termination.i error 0 wit inspect 2.5 260 21 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.9
array-examples/sanfoundry_27_true-unreach-call_ground.i error 0 wit inspect 2.5 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.8
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 7.2   290  
array-examples/sorting_bubblesort_true-unreach-call_ground.i error 0 wit inspect 2.6 260 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .022 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i error 0 wit inspect 2.5 270 24 - 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_compareModified_true-unreach-call_ground.i error 0 wit inspect 2.5 270 21 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 4.8
array-examples/standard_compare_true-unreach-call_ground.i error 0 wit inspect 2.5 260 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .023 4.9
array-examples/standard_copy1_true-unreach-call_ground.i error 0 wit inspect 2.5 260 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .022 4.8
array-examples/standard_copy2_true-unreach-call_ground.i error 0 wit inspect 2.5 260 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .017 4.9
array-examples/standard_copy3_true-unreach-call_ground.i error 0 wit inspect 2.5 260 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .020 5.0
array-examples/standard_copy4_true-unreach-call_ground.i error 0 wit inspect 2.6 260 23 - 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_copy5_true-unreach-call_ground.i error 0 wit inspect 2.6 270 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.8
array-examples/standard_copy6_true-unreach-call_ground.i error 0 wit inspect 2.6 270 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .020 4.8
array-examples/standard_copy7_true-unreach-call_ground.i error 0 wit inspect 2.5 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 5.0
array-examples/standard_copy8_true-unreach-call_ground.i error 0 wit inspect 2.6 270 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .021 4.9
array-examples/standard_copy9_true-unreach-call_ground.i error 0 wit inspect 2.5 270 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .018 4.9
array-examples/standard_copyInitSum2_true-unreach-call_ground.i error 0 wit inspect 2.5 270 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_copyInitSum3_true-unreach-call_ground.i error 0 wit inspect 2.5 270 21 - 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_copyInitSum_true-unreach-call_ground.i error 0 wit inspect 2.6 270 21 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 45 error (2) 0 wit inspect .023 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i error 0 wit inspect 2.6 270 25 - 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_find_true-unreach-call_ground.i error 0 wit inspect 2.6 270 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .021 4.8
array-examples/standard_init1_true-unreach-call_ground.i error 0 wit inspect 2.5 260 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .018 4.8
array-examples/standard_init2_true-unreach-call_ground.i error 0 wit inspect 2.5 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .021 4.9
array-examples/standard_init3_true-unreach-call_ground.i error 0 wit inspect 2.6 260 27 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .020 4.8
array-examples/standard_init4_true-unreach-call_ground.i error 0 wit inspect 2.6 270 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .018 4.9
array-examples/standard_init5_true-unreach-call_ground.i error 0 wit inspect 2.5 260 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_init6_true-unreach-call_ground.i error 0 wit inspect 2.5 260 25 - 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_init7_true-unreach-call_ground.i error 0 wit inspect 2.6 270 26 - 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
array-examples/standard_init8_true-unreach-call_ground.i error 0 wit inspect 2.7 270 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .019 5.0
array-examples/standard_init9_true-unreach-call_ground.i error 0 wit inspect 2.6 270 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 5.0
array-examples/standard_maxInArray_true-unreach-call_ground.i error 0 wit inspect 2.5 270 21 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_minInArray_true-unreach-call_ground.i error 0 wit inspect 2.4 260 21 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i error 0 wit inspect 2.4 260 21 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i error 0 wit inspect 2.6 270 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .89 43 error (2) 0 wit inspect .024 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i error 0 wit inspect 2.6 270 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .026 5.0
array-examples/standard_partition_true-unreach-call_ground.i error 0 wit inspect 2.5 270 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_password_true-unreach-call_ground.i error 0 wit inspect 2.5 260 21 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 5.0
array-examples/standard_reverse_true-unreach-call_ground.i error 0 wit inspect 2.5 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 5.0
array-examples/standard_running_true-unreach-call.i error 0 wit inspect 2.5 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .023 4.9
array-examples/standard_sentinel_true-unreach-call_true-termination.i error 0 wit inspect 2.5 270 26 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .024 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i error 0 wit inspect 2.5 270 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_strcmp_true-unreach-call_ground.i error 0 wit inspect 2.6 270 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .023 4.8
array-examples/standard_strcpy_original_true-unreach-call.i error 0 wit inspect 2.7 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .025 5.0
array-examples/standard_strcpy_true-unreach-call_ground.i error 0 wit inspect 2.5 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.8
array-examples/standard_two_index_01_true-unreach-call.i error 0 wit inspect 2.5 260 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 5.0
array-examples/standard_two_index_02_true-unreach-call.i error 0 wit inspect 2.5 270 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_03_true-unreach-call.i error 0 wit inspect 2.5 270 23 - 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-examples/standard_two_index_04_true-unreach-call.i error 0 wit inspect 2.4 270 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .021 4.9
array-examples/standard_two_index_05_true-unreach-call.i error 0 wit inspect 2.6 270 24 - 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/standard_two_index_06_true-unreach-call.i error 0 wit inspect 2.5 260 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .025 4.8
array-examples/standard_two_index_07_true-unreach-call.i error 0 wit inspect 2.5 260 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.8
array-examples/standard_two_index_08_true-unreach-call.i error 0 wit inspect 2.5 270 21 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.9
array-examples/standard_two_index_09_true-unreach-call.i error 0 wit inspect 2.6 270 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .018 4.9
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i error 0 wit inspect 2.5 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .024 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i error 0 wit inspect 2.5 260 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 4.8
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i error 0 wit inspect 2.7 270 24 error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .86 48 error (invalid witness file) 0 wit inspect .0012 .33 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i timeout 0 wit inspect 900   4200 11000 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .80 48 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i error 0 wit inspect 2.5 270 22 error (invalid witness file) 0 wit inspect .55 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 .0011 .29 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i error 0 wit inspect 2.5 260 22 error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i error 0 wit inspect 2.5 270 23 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 5.0 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/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 900   6400 11000 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i error 0 wit inspect 2.7 260 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .026 4.8
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i error 0 wit inspect 2.7 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .020 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i timeout 0 wit inspect 900   4200 9900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 5.0
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 0 wit inspect 900   4200 9300 - 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-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i timeout 0 wit inspect 910   11000 4400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .024 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 900   4200 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .021 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout 0 wit inspect 900   5100 11000 - 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-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900   3800 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .026 4.8
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 0 wit inspect 900   3900 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 5.0
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900   7800 6400 - 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-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.9 290 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 true 2 wit inspect 4.8   230  
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.5 410 60 true -32 wit inspect 4.5  260 true -32 wit inspect 5.1   240   unknown 0 wit inspect 3.2  220 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.7 530 58 true -32 wit inspect 4.4  290 true -32 wit inspect 5.0   230   unknown 0 wit inspect 3.6  230 false(unreach-call) 1 wit inspect .59   20    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 13   740 120 true -32 wit inspect 5.2  270 true -32 wit inspect 5.3   260   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .65   21    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 92   3700 900 true -32 wit inspect 5.6  270 true -32 wit inspect 5.6   250   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .65   23    - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect 210   4600 2200 true -32 wit inspect 6.2  270 true -32 wit inspect 5.6   260   unknown 0 wit inspect 4.1  210 false(unreach-call) 1 wit inspect .67   26    - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 15   650 110 timeout 0 wit inspect 92    1900 true -32 wit inspect 5.0   230   unknown 0 wit inspect 3.3  190 true -32 wit inspect .61   19    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 5.5 380 52 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 timeout 0 wit inspect 960     5400  
reducercommutativity/avg10_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 7.4 450 57 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 out of memory 0 wit inspect 60     7000  
reducercommutativity/avg20_true-unreach-call.i false(unreach-call) -16 wit inspect 10   680 89 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  270 out of memory 0 wit inspect 58     7000  
reducercommutativity/avg40_true-unreach-call.i false(unreach-call) -16 wit inspect 180   3200 1500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  270 out of memory 0 wit inspect 67     7000  
reducercommutativity/avg60_true-unreach-call.i false(unreach-call) -16 wit inspect 630   4600 7000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  270 out of memory 0 wit inspect 74     7000  
reducercommutativity/avg_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 5.8 410 50 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2300 true 2 wit inspect 6.3   230  
reducercommutativity/max05_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 5.6 300 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  260 out of memory 0 wit inspect 61     7000  
reducercommutativity/max10_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 7.2 430 64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  270 out of memory 0 wit inspect 68     7000  
reducercommutativity/max20_true-unreach-call.i false(unreach-call) -16 wit inspect 11   540 93 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  270 out of memory 0 wit inspect 57     7000  
reducercommutativity/max40_true-unreach-call.i false(unreach-call) -16 wit inspect 370   3000 4800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  270 out of memory 0 wit inspect 68     7000  
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 900   4000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .023 4.8
reducercommutativity/max_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 9.2 470 75 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 true 2 wit inspect 5.0   230  
reducercommutativity/sep05_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 6.5 360 56 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 out of memory 0 wit inspect 370     7000  
reducercommutativity/sep10_true-unreach-call.i false(unreach-call) -16 wit inspect 14   660 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  270 out of memory 0 wit inspect 74     7000  
reducercommutativity/sep20_true-unreach-call.i false(unreach-call) -16 wit inspect 63   3200 670 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  270 out of memory 0 wit inspect 55     7000  
reducercommutativity/sep40_true-unreach-call.i false(unreach-call) -16 wit inspect 850   9200 7100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  270 out of memory 0 wit inspect 66     7000  
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 910   9700 7300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 4.8
reducercommutativity/sep_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 880   6700 12000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 true 2 wit inspect 6.2   230  
reducercommutativity/sum05_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 5.2 320 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 timeout 0 wit inspect 960     4900  
reducercommutativity/sum10_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 7.3 430 59 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 out of memory 0 wit inspect 56     7000  
reducercommutativity/sum20_true-unreach-call.i false(unreach-call) -16 wit inspect 11   620 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  270 out of memory 0 wit inspect 56     7000  
reducercommutativity/sum40_true-unreach-call.i false(unreach-call) -16 wit inspect 160   3500 1800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  270 out of memory 0 wit inspect 66     7000  
reducercommutativity/sum60_true-unreach-call.i false(unreach-call) -16 wit inspect 630   4500 7200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  270 out of memory 0 wit inspect 68     7000  
reducercommutativity/sum_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 4.9 310 41 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2300 true 2 wit inspect 5.0   230  
array-tiling/mlceu_false-unreach-call.i false(unreach-call) 0 wit inspect 3.4 280 31 timeout 0 wit inspect 92    2000 true -32 wit inspect 7.6   260   unknown 0 wit inspect 2.8  180 true -32 wit inspect .60   19    - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i false(unreach-call) 1 wit inspect 3.6 290 30 timeout 0 wit inspect 92    2000 false(unreach-call) 1 wit inspect 7.9   280   unknown 0 wit inspect 2.9  210 true -32 wit inspect .59   19    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i false(unreach-call) -16 wit inspect 4.0 300 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 true 2 wit inspect 6.3   260  
array-tiling/mbpr3_true-unreach-call.i false(unreach-call) -16 wit inspect 4.5 310 38 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 true 2 wit inspect 7.5   270  
array-tiling/mbpr4_true-unreach-call.i false(unreach-call) -16 wit inspect 5.0 310 48 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 true 2 wit inspect 7.5   290  
array-tiling/mbpr5_true-unreach-call.i false(unreach-call) -16 wit inspect 5.6 320 48 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 true 2 wit inspect 8.7   310  
array-tiling/nr2_true-unreach-call.i false(unreach-call) -16 wit inspect 3.8 290 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 timeout 0 wit inspect 960     1500  
array-tiling/nr3_true-unreach-call.i false(unreach-call) -16 wit inspect 3.8 300 34 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 true 2 wit inspect 79     830  
array-tiling/nr4_true-unreach-call.i false(unreach-call) -16 wit inspect 3.8 290 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 true 2 wit inspect 130     1900  
array-tiling/nr5_true-unreach-call.i false(unreach-call) -16 wit inspect 3.8 300 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 out of memory 0 wit inspect 130     7000  
array-tiling/pnr2_true-unreach-call.i false(unreach-call) -16 wit inspect 3.6 300 33 - wit inspect - wit inspect - wit inspect -