Tool CPAchecker 1.6.1-svn 26725 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:36:53 CET 2017-12-01 08:24:12 CET 2017-12-01 08:27:09 CET 2017-12-01 08:31:26 CET 2017-12-01 04:24:37 CET 2017-12-01 07:42:15 CET
Run set cpa-bam-bnb.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Arrays
Options -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.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-bnb.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-bnb.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-bnb.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-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-bnb.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.6 270 21 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i error 0 wit inspect 2.5 270 25 error (invalid witness file) 0 wit inspect .55 43 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 .0011 .30 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i error 0 wit inspect 2.6 270 23 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect 1.0  52 error (invalid witness file) 0 wit inspect .0035 .30 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i error 0 wit inspect 2.8 290 26 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect 1.0  51 error (invalid witness file) 0 wit inspect .0012 .32 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i error 0 wit inspect 2.8 290 28 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .94 47 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i error 0 wit inspect 2.5 270 23 error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0011 .30 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i error 0 wit inspect 2.5 270 24 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0011 .27 - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i error 0 wit inspect 2.5 260 20 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.1  48 error (invalid witness file) 0 wit inspect .0012 .33 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i error 0 wit inspect 2.6 270 23 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0032 .26 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i error 0 wit inspect 2.6 270 24 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .95 48 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i error 0 wit inspect 2.6 270 23 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i error 0 wit inspect 2.5 270 23 error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .96 49 error (invalid witness file) 0 wit inspect .0027 .29 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i error 0 wit inspect 2.5 270 23 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect 1.1  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 270 25 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .92 50 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i error 0 wit inspect 2.6 270 21 error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .84 48 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i error 0 wit inspect 2.5 270 25 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i error 0 wit inspect 2.4 270 22 error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i error 0 wit inspect 2.7 290 23 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .94 47 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i error 0 wit inspect 2.6 260 24 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i error 0 wit inspect 2.6 270 25 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0016 .23 - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i error 0 wit inspect 2.7 290 26 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0013 .33 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i error 0 wit inspect 2.7 290 23 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .80 49 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i error 0 wit inspect 2.7 270 22 error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .71 49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i error 0 wit inspect 2.7 270 21 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i error 0 wit inspect 2.7 270 23 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.0  53 error (invalid witness file) 0 wit inspect .0011 .31 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i error 0 wit inspect 2.5 270 22 error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .96 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i error 0 wit inspect 2.4 270 23 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0012 .36 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i error 0 wit inspect 3.0 290 26 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .026 4.8 error (invalid witness file) 0 wit inspect .93 47 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i error 0 wit inspect 2.5 260 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .024 4.9
array-examples/data_structures_set_multi_proc_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 .59 44 error (2) 0 wit inspect .022 4.8
array-examples/relax_true-unreach-call.i error 0 wit inspect 8.1 440 61 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.9
array-examples/sanfoundry_02_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 .69 44 error (2) 0 wit inspect .022 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i timeout 0 wit inspect 900   4100 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 5.0
array-examples/sanfoundry_24_true-unreach-call_true-termination.i error 0 wit inspect 2.7 290 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .020 4.9
array-examples/sanfoundry_27_true-unreach-call_ground.i error 0 wit inspect 2.5 270 26 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .021 4.9
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect 2.8 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 5.1   230  
array-examples/sorting_bubblesort_true-unreach-call_ground.i error 0 wit inspect 3.0 290 25 - 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/sorting_selectionsort_true-unreach-call_ground.i error 0 wit inspect 2.5 270 20 - 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/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 .65 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_compare_true-unreach-call_ground.i error 0 wit inspect 2.9 290 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .020 4.8
array-examples/standard_copy1_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 .53 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy2_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 .54 41 error (2) 0 wit inspect .020 4.9
array-examples/standard_copy3_true-unreach-call_ground.i error 0 wit inspect 2.7 270 20 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .019 5.0
array-examples/standard_copy4_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 .68 44 error (2) 0 wit inspect .017 4.9
array-examples/standard_copy5_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 .51 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_copy6_true-unreach-call_ground.i error 0 wit inspect 2.5 270 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_copy7_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 .69 44 error (2) 0 wit inspect .024 5.0
array-examples/standard_copy8_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 .51 41 error (2) 0 wit inspect .022 4.8
array-examples/standard_copy9_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 .69 41 error (2) 0 wit inspect .022 4.8
array-examples/standard_copyInitSum2_true-unreach-call_ground.i error 0 wit inspect 2.5 270 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 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 .55 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_copyInitSum_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 .69 43 error (2) 0 wit inspect .021 5.0
array-examples/standard_copyInit_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 .54 43 error (2) 0 wit inspect .022 4.9
array-examples/standard_find_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 .56 44 error (2) 0 wit inspect .024 4.8
array-examples/standard_init1_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 .69 44 error (2) 0 wit inspect .022 4.9
array-examples/standard_init2_true-unreach-call_ground.i error 0 wit inspect 2.4 270 21 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .021 4.9
array-examples/standard_init3_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 .70 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_init4_true-unreach-call_ground.i error 0 wit inspect 2.5 270 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 4.8
array-examples/standard_init5_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 .73 44 error (2) 0 wit inspect .019 4.9
array-examples/standard_init6_true-unreach-call_ground.i error 0 wit inspect 2.8 290 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .020 4.8
array-examples/standard_init7_true-unreach-call_ground.i error 0 wit inspect 2.7 290 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_init8_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 .71 43 error (2) 0 wit inspect .024 4.8
array-examples/standard_init9_true-unreach-call_ground.i error 0 wit inspect 2.6 260 22 - 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_maxInArray_true-unreach-call_ground.i error 0 wit inspect 2.4 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .022 5.0
array-examples/standard_minInArray_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 .56 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_palindrome_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 .60 43 error (2) 0 wit inspect .023 4.8
array-examples/standard_partial_init_true-unreach-call_ground.i error 0 wit inspect 2.8 300 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .020 4.9
array-examples/standard_partition_original_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 .55 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_partition_true-unreach-call_ground.i error 0 wit inspect 2.8 290 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_password_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 .54 41 error (2) 0 wit inspect .019 4.9
array-examples/standard_reverse_true-unreach-call_ground.i error 0 wit inspect 2.4 260 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_running_true-unreach-call.i error 0 wit inspect 2.8 290 26 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 41 error (2) 0 wit inspect .022 4.9
array-examples/standard_sentinel_true-unreach-call_true-termination.i error 0 wit inspect 2.5 270 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 5.0
array-examples/standard_seq_init_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 .58 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 26 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .023 4.9
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 .73 43 error (2) 0 wit inspect .020 4.8
array-examples/standard_strcpy_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 .53 41 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_01_true-unreach-call.i error 0 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_two_index_02_true-unreach-call.i error 0 wit inspect 2.7 300 24 - 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_two_index_03_true-unreach-call.i error 0 wit inspect 2.7 290 27 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .021 5.0
array-examples/standard_two_index_04_true-unreach-call.i error 0 wit inspect 2.6 270 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_two_index_05_true-unreach-call.i error 0 wit inspect 2.5 270 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .023 5.0
array-examples/standard_two_index_06_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 .57 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_two_index_07_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 .58 42 error (2) 0 wit inspect .018 4.9
array-examples/standard_two_index_08_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 .55 42 error (2) 0 wit inspect .020 4.8
array-examples/standard_two_index_09_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 44 error (2) 0 wit inspect .024 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i error 0 wit inspect 2.7 290 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .022 4.8
array-examples/standard_vector_difference_true-unreach-call_ground.i error 0 wit inspect 2.8 290 26 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 5.0
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i error 0 wit inspect 2.6 270 22 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .99 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i timeout 0 wit inspect 900   4200 8400 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .98 49 error (invalid witness file) 0 wit inspect .0014 .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 43 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0012 .32 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i error 0 wit inspect 2.6 270 25 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i error 0 wit inspect 2.6 270 23 error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 900   5600 9300 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i error 0 wit inspect 2.5 270 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .023 5.0
array-industry-pattern/array_mul_init_true-unreach-call_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 .69 44 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i timeout 0 wit inspect 900   4200 9500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .026 5.0
array-industry-pattern/array_of_struct_ptr_cond_init_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 .53 41 error (2) 0 wit inspect .019 5.0
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i timeout 0 wit inspect 900   5700 8800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 900   3900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout 0 wit inspect 900   4200 7800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 46 error (2) 0 wit inspect .019 5.0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900   4300 8800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 46 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 5.0
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900   3900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i timeout 0 wit inspect 900   11000 6600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 45 error (2) 0 wit inspect .019 5.0
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.2 400 60 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 74     4900   unknown 0 wit inspect 3.9  210 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.6 430 65 true -32 wit inspect 4.3  270 out of memory 0 wit inspect 88     7000   unknown 0 wit inspect 3.8  220 false(unreach-call) 1 wit inspect .61   20    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 9.5 580 67 true -32 wit inspect 4.6  260 out of memory 0 wit inspect 88     7000   unknown 0 wit inspect 3.8  220 false(unreach-call) 1 wit inspect .61   21    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i timeout 0 wit inspect 900   5400 11000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .95 47 error (invalid witness file) 0 wit inspect .0032 .34 - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i timeout 0 wit inspect 900   5400 9800 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .96 49 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 17   590 120 timeout 0 wit inspect 91    2000 false(unreach-call) 1 wit inspect 16     540   unknown 0 wit inspect 3.5  210 true -32 wit inspect .58   19    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 5.8 370 52 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2100 out of memory 0 wit inspect 75     7000  
reducercommutativity/avg10_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 7.2 420 64 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 out of memory 0 wit inspect 100     7000  
reducercommutativity/avg20_true-unreach-call.i false(unreach-call) -16 wit inspect 9.1 560 81 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2100 out of memory 0 wit inspect 120     7000  
reducercommutativity/avg40_true-unreach-call.i false(unreach-call) -16 wit inspect 53   2400 530 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 out of memory 0 wit inspect 55     7000  
reducercommutativity/avg60_true-unreach-call.i false(unreach-call) -16 wit inspect 120   4000 1200 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 600    7000 out of memory 0 wit inspect 70     7000  
reducercommutativity/avg_true-unreach-call_true-termination.i timeout 0 wit inspect 900   7800 8000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .023 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 8.5 520 72 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.9  280 out of memory 0 wit inspect 67     7000  
reducercommutativity/max10_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 14   520 100 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 6.0  350 out of memory 0 wit inspect 79     7000  
reducercommutativity/max20_true-unreach-call.i false(unreach-call) -16 wit inspect 18   710 140 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 14    570 out of memory 0 wit inspect 63     7000  
reducercommutativity/max40_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 .63 43 error (2) 0 wit inspect .019 4.8
reducercommutativity/max60_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 .63 44 error (2) 0 wit inspect .026 4.8
reducercommutativity/max_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 260   3200 3100 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.7  280 out of memory 0 wit inspect 420     7000  
reducercommutativity/sep05_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 13   500 100 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.3  300 out of memory 0 wit inspect 76     7000  
reducercommutativity/sep10_true-unreach-call.i false(unreach-call) -16 wit inspect 34   1200 240 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.4  330 out of memory 0 wit inspect 81     7000  
reducercommutativity/sep20_true-unreach-call.i false(unreach-call) -16 wit inspect 140   3900 1600 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 15    520 out of memory 0 wit inspect 62     7000  
reducercommutativity/sep40_true-unreach-call.i timeout 0 wit inspect 910   9900 6900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .019 4.8
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 910   10000 7700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .018 4.9
reducercommutativity/sep_true-unreach-call_true-termination.i timeout 0 wit inspect 900   3900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/sum05_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 5.3 320 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 out of memory 0 wit inspect 94     7000  
reducercommutativity/sum10_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 6.5 360 46 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 out of memory 0 wit inspect 96     7000  
reducercommutativity/sum20_true-unreach-call.i false(unreach-call) -16 wit inspect 8.1 480 68 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 out of memory 0 wit inspect 80     7000  
reducercommutativity/sum40_true-unreach-call.i false(unreach-call) -16 wit inspect 55   2500 480 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 out of memory 0 wit inspect 74     7000  
reducercommutativity/sum60_true-unreach-call.i false(unreach-call) -16 wit inspect 120   3900 1100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 290    7000 out of memory 0 wit inspect 69     7000  
reducercommutativity/sum_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 93   3600 1000 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 7.1  330 timeout 0 wit inspect 960     5400  
array-tiling/mlceu_false-unreach-call.i error 0 wit inspect 58   2900 560 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .90 47 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 3.9 300 34 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 9.3   280   unknown 0 wit inspect 3.0  190 true -32 wit inspect .59   19    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i error 0 wit inspect 50   2400 440 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .024 5.0
array-tiling/mbpr3_true-unreach-call.i error 0 wit inspect 56   2500 490 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .018 5.0
array-tiling/mbpr4_true-unreach-call.i error 0 wit inspect 45   1800 380 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8
array-tiling/mbpr5_true-unreach-call.i error 0 wit inspect 47   1700 430 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .025 4.9
array-tiling/nr2_true-unreach-call.i error 0 wit inspect 48   1900 430 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 45 error (2) 0 wit inspect .019 4.9
array-tiling/nr3_true-unreach-call.i error 0 wit inspect 45   2000 370 - 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-tiling/nr4_true-unreach-call.i error 0 wit inspect 33   1200 300 - 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-tiling/nr5_true-unreach-call.i error 0 wit inspect 30   1200 240 - 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-tiling/pnr2_true-unreach-call.i error 0 wit inspect 5.1 300 42 - 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-tiling/pnr3_true-unreach-call.i error 0 wit inspect 4.4 310 35 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit