Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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* [apollon010; apollon035; apollon045; apollon077; apollon078; apollon138] [apollon007; apollon077; apollon078; apollon143] 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-01 08:49:27 CET 2017-12-01 22:53:44 CET 2017-12-01 23:38:04 CET 2017-12-01 23:47:42 CET 2017-12-01 23:55:24 CET 2017-12-01 22:20:30 CET 2017-12-01 23:01:53 CET
Run set esbmc-incr.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Arrays
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-incr.2017-12-01_0849.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     3800 8400    error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i timeout 0 wit inspect 900     2800 10000    error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i timeout 0 wit inspect 900     2800 10000    error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i timeout 0 wit inspect 900     7400 9800    error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i timeout 0 wit inspect 900     7400 12000    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i timeout 0 wit inspect 900     3000 7000    error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .85 51 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i timeout 0 wit inspect 900     9300 10000    error (invalid witness file) 0 wit inspect .55 41 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 .26 - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i timeout 0 wit inspect 900     9400 9300    error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .037 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i timeout 0 wit inspect 900     9500 10000    error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .84 50 error (invalid witness file) 0 wit inspect .0010 .27 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i timeout 0 wit inspect 900     9300 8800    error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i timeout 0 wit inspect 900     9500 10000    error (invalid witness file) 0 wit inspect .58 43 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_copy6_false-unreach-call_ground.i timeout 0 wit inspect 900     9400 9900    error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0030 .29 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i timeout 0 wit inspect 900     9600 8700    error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .67 50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i timeout 0 wit inspect 900     9900 9700    error (invalid witness file) 0 wit inspect .58 46 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i timeout 0 wit inspect 900     9200 9500    error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .65 50 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i timeout 0 wit inspect 900     6200 12000    error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .68 50 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i timeout 0 wit inspect 900     5900 9600    error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i timeout 0 wit inspect 900     5900 10000    error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0012 .28 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i timeout 0 wit inspect 900     5900 10000    error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i timeout 0 wit inspect 900     6000 9000    error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .71 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i timeout 0 wit inspect 900     5900 9700    error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i timeout 0 wit inspect 900     6100 11000    error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i timeout 0 wit inspect 900     6000 11000    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .64 50 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i timeout 0 wit inspect 900     6100 9100    error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .036 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0012 .33 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i timeout 0 wit inspect 900     6000 11000    error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i timeout 0 wit inspect 900     7100 11000    error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i timeout 0 wit inspect 900     4200 10000    error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .67 50 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i out of memory 0 wit inspect 430     15000 5600    error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i timeout 0 wit inspect 900     9200 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i timeout 0 wit inspect 900     3500 7700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 5.0
array-examples/relax_true-unreach-call.i timeout 0 wit inspect 900     350 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .021 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i timeout 0 wit inspect 900     360 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .019 4.9
array-examples/sanfoundry_24_true-unreach-call_true-termination.i timeout 0 wit inspect 900     1000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .024 4.8
array-examples/sanfoundry_27_true-unreach-call_ground.i timeout 0 wit inspect 900     7000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.8
array-examples/sanfoundry_43_true-unreach-call_ground.i timeout 0 wit inspect 900     9700 12000    - 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/sorting_bubblesort_true-unreach-call_ground.i timeout 0 wit inspect 900     2800 9900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 5.0
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 0 wit inspect 900     7300 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .023 5.0
array-examples/standard_compareModified_true-unreach-call_ground.i timeout 0 wit inspect 900     5800 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .027 4.8
array-examples/standard_compare_true-unreach-call_ground.i timeout 0 wit inspect 900     7500 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .019 4.8
array-examples/standard_copy1_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_copy2_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .024 4.8
array-examples/standard_copy3_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 9900    - 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/standard_copy4_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 9900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .020 5.0
array-examples/standard_copy5_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 12000    - 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-examples/standard_copy6_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .019 5.0
array-examples/standard_copy7_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 44 error (2) 0 wit inspect .024 4.9
array-examples/standard_copy8_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 9800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .024 4.8
array-examples/standard_copy9_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 9900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .019 4.8
array-examples/standard_copyInitSum2_true-unreach-call_ground.i timeout 0 wit inspect 900     6000 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 44 error (2) 0 wit inspect .022 4.8
array-examples/standard_copyInitSum3_true-unreach-call_ground.i timeout 0 wit inspect 900     6100 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 41 error (2) 0 wit inspect .021 4.9
array-examples/standard_copyInitSum_true-unreach-call_ground.i timeout 0 wit inspect 900     6000 9600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_copyInit_true-unreach-call_ground.i timeout 0 wit inspect 900     6000 9500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 4.9
array-examples/standard_find_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 9800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .025 5.0
array-examples/standard_init1_true-unreach-call_ground.i timeout 0 wit inspect 900     5800 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .023 5.0
array-examples/standard_init2_true-unreach-call_ground.i timeout 0 wit inspect 900     5900 9600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .76 44 error (2) 0 wit inspect .022 4.8
array-examples/standard_init3_true-unreach-call_ground.i timeout 0 wit inspect 900     6000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .020 5.0
array-examples/standard_init4_true-unreach-call_ground.i timeout 0 wit inspect 900     6000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_init5_true-unreach-call_ground.i timeout 0 wit inspect 900     6000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 5.0
array-examples/standard_init6_true-unreach-call_ground.i timeout 0 wit inspect 900     6000 8600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .018 4.8
array-examples/standard_init7_true-unreach-call_ground.i timeout 0 wit inspect 900     6000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .022 4.8
array-examples/standard_init8_true-unreach-call_ground.i timeout 0 wit inspect 900     6000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .024 4.8
array-examples/standard_init9_true-unreach-call_ground.i timeout 0 wit inspect 900     6000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .022 5.0
array-examples/standard_maxInArray_true-unreach-call_ground.i timeout 0 wit inspect 900     7100 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_minInArray_true-unreach-call_ground.i timeout 0 wit inspect 900     7200 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .019 4.8
array-examples/standard_palindrome_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_partial_init_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 .42 44 error (2) 0 wit inspect .024 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i out of memory 0 wit inspect 480     15000 6600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .022 4.8
array-examples/standard_partition_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 .71 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_password_true-unreach-call_ground.i timeout 0 wit inspect 900     7500 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_reverse_true-unreach-call_ground.i timeout 0 wit inspect 900     8700 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .019 4.8
array-examples/standard_running_true-unreach-call.i out of memory 0 wit inspect 430     15000 5200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i timeout 0 wit inspect 900     300 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .023 4.8
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 0 wit inspect 900     6100 9900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .019 5.0
array-examples/standard_strcmp_true-unreach-call_ground.i timeout 0 wit inspect 900     7200 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.8
array-examples/standard_strcpy_original_true-unreach-call.i timeout 0 wit inspect 900     10000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_strcpy_true-unreach-call_ground.i timeout 0 wit inspect 900     10000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .023 5.0
array-examples/standard_two_index_01_true-unreach-call.i timeout 0 wit inspect 900     10000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_02_true-unreach-call.i timeout 0 wit inspect 900     10000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .023 4.8
array-examples/standard_two_index_03_true-unreach-call.i timeout 0 wit inspect 900     10000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_04_true-unreach-call.i timeout 0 wit inspect 900     10000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_two_index_05_true-unreach-call.i timeout 0 wit inspect 900     9900 9800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .47 44 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_06_true-unreach-call.i timeout 0 wit inspect 900     10000 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 5.0
array-examples/standard_two_index_07_true-unreach-call.i timeout 0 wit inspect 900     10000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 5.0
array-examples/standard_two_index_08_true-unreach-call.i timeout 0 wit inspect 900     10000 8500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 45 error (2) 0 wit inspect .018 5.0
array-examples/standard_two_index_09_true-unreach-call.i timeout 0 wit inspect 900     10000 10000    - 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_vararg_true-unreach-call_ground_true-termination.i timeout 0 wit inspect 900     830 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .021 4.8
array-examples/standard_vector_difference_true-unreach-call_ground.i timeout 0 wit inspect 900     4500 9900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .025 4.8
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i timeout 0 wit inspect 900     6400 9900    error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .65 50 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i timeout 0 wit inspect 900     5200 10000    error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i timeout 0 wit inspect 900     5000 11000    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i timeout 0 wit inspect 900     4600 11000    error (invalid witness file) 0 wit inspect .73 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0011 .35 - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i timeout 0 wit inspect 900     5000 12000    error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 900     3500 7700    error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i timeout 0 wit inspect 900     4200 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_mul_init_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 .69 43 error (2) 0 wit inspect .024 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i out of memory 0 wit inspect 660     15000 5000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 4.9
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 0 wit inspect 900     6400 9800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.9
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i timeout 0 wit inspect 900     8400 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .018 5.0
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 900     4800 8900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .020 4.9
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout 0 wit inspect 900     2500 11000    - 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-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900     1600 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 0 wit inspect 900     7300 11000    - 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-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900     4300 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .024 4.9
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i timeout 0 wit inspect 900     190 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .018 5.0
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.1   28 10    false(unreach-call) 1 wit inspect 5.4  360 true -32 wit inspect 6.3   270   unknown 0 wit inspect 2.2  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.0   29 14    false(unreach-call) 1 wit inspect 7.9  380 true -32 wit inspect 6.0   280   unknown 0 wit inspect 2.3  220 true -32 wit inspect .59   18    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 4.1   32 35    false(unreach-call) 1 wit inspect 11    440 true -32 wit inspect 6.7   320   unknown 0 wit inspect 3.5  220 true -32 wit inspect .60   18    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 15     45 170    false(unreach-call) 1 wit inspect 28    750 true -32 wit inspect 4.7   380   unknown 0 wit inspect 4.1  230 true -32 wit inspect .63   19    - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 0 wit inspect 180     170 2600    timeout 0 wit inspect 92    1300 true -32 wit inspect 5.4   480   unknown 0 wit inspect 4.4  220 true -32 wit inspect .66   19    - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.2   31 11    false(unreach-call) 1 wit inspect 5.1  360 true -32 wit inspect 6.5   270   unknown 0 wit inspect 3.1  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i true 2 wit inspect 42     72 630    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1400 timeout 0 wit inspect 960     4900  
reducercommutativity/avg10_true-unreach-call_true-termination.i true 2 wit inspect 490     190 5600    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 timeout 0 wit inspect 930     7000  
reducercommutativity/avg20_true-unreach-call.i timeout 0 wit inspect 900     290 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 45 error (2) 0 wit inspect .020 4.9
reducercommutativity/avg40_true-unreach-call.i timeout 0 wit inspect 900     370 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/avg60_true-unreach-call.i timeout 0 wit inspect 900     440 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .021 5.0
reducercommutativity/avg_true-unreach-call_true-termination.i timeout 0 wit inspect 900     150 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect .65  28 8.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 130    920 timeout 0 wit inspect 960     3500  
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 17     44 210    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3300 timeout 0 wit inspect 960     3500  
reducercommutativity/max20_true-unreach-call.i timeout 0 wit inspect 900     140 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .019 4.9
reducercommutativity/max40_true-unreach-call.i timeout 0 wit inspect 900     190 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 900     260 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .036 4.9
reducercommutativity/max_true-unreach-call_true-termination.i timeout 0 wit inspect 900     110 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 44 error (2) 0 wit inspect .019 4.8
reducercommutativity/sep05_true-unreach-call_true-termination.i true 2 wit inspect .11  26 .89 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1500 timeout 0 wit inspect 960     1700  
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect .10  26 1.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1900 out of memory 0 wit inspect 880     7000  
reducercommutativity/sep20_true-unreach-call.i true 2 wit inspect .17  26 1.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 timeout 0 wit inspect 960     6900  
reducercommutativity/sep40_true-unreach-call.i true 2 wit inspect .21  26 2.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1900 timeout 0 wit inspect 960     4600  
reducercommutativity/sep60_true-unreach-call.i true 2 wit inspect .33  26 3.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3100 timeout 0 wit inspect 960     3000  
reducercommutativity/sep_true-unreach-call_true-termination.i timeout 0 wit inspect 900     120 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .023 4.8
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect .12  26 .88 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    980 true 2 wit inspect 420     3500  
reducercommutativity/sum10_true-unreach-call_true-termination.i true 2 wit inspect .099 26 1.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     5000  
reducercommutativity/sum20_true-unreach-call.i true 2 wit inspect .14  26 1.5  - 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 true 2 wit inspect .17  26 2.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 timeout 0 wit inspect 960     4000  
reducercommutativity/sum60_true-unreach-call.i true 2 wit inspect .25  26 2.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3100 timeout 0 wit inspect 960     3100  
reducercommutativity/sum_true-unreach-call_true-termination.i timeout 0 wit inspect 900     150 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
array-tiling/mlceu_false-unreach-call.i timeout 0 wit inspect 900     180 11000    error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0030 .26 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i false(unreach-call) 1 wit inspect .13  28 1.9  false(unreach-call) 1 wit inspect 3.1  260 true -32 wit inspect 4.5   260   unknown 0 wit inspect 1.9  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i timeout 0 wit inspect 900     240 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .022 4.9
array-tiling/mbpr3_true-unreach-call.i timeout 0 wit inspect 900     240 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .024 4.9
array-tiling/mbpr4_true-unreach-call.i timeout 0 wit inspect 900     200 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .025 4.8
array-tiling/mbpr5_true-unreach-call.i timeout 0 wit inspect 900     210 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .018 5.0
array-tiling/nr2_true-unreach-call.i timeout 0 wit inspect 900     220 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8
array-tiling/nr3_true-unreach-call.i timeout 0 wit inspect 900     160 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .019 4.8
array-tiling/nr4_true-unreach-call.i timeout 0 wit inspect 900     220 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 45 error (2) 0 wit inspect .023 5.0
array-tiling/nr5_true-unreach-call.i timeout 0 wit inspect 900     140 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .024 5.0
array-tiling/pnr2_true-unreach-call.i timeout 0 wit inspect 900     260 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .018 5.0
array-tiling/pnr3_true-unreach-call.i timeout 0 wit inspect 900     270 11000    - 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-tiling/pnr4_true-unreach-call.i timeout 0 wit inspect 900     280 8700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .76 43 error (2) 0 wit inspect .018 5.0
array-tiling/pnr5_true-unreach-call.i timeout 0 wit inspect 900     290 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 4.9
array-tiling/poly1_true-unreach-call.i unknown 0 wit inspect .10  26 .80 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .021 4.8
array-tiling/poly2_true-unreach-call.i unknown 0 wit inspect .058 15 .29 - 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-tiling/pr2_true-unreach-call.i timeout 0 wit inspect 900     230 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .024 4.8
array-tiling/pr3_true-unreach-call.i timeout 0 wit inspect 900     240 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .018 4.9
array-tiling/pr4_true-unreach-call.i timeout 0 wit inspect 900     390 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .024 5.0
array-tiling/pr5_true-unreach-call.i timeout 0 wit inspect 900     280 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .019 5.0
array-tiling/revcpyswp2_true-unreach-call.i timeout 0 wit inspect 900     250 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 42 error (2) 0 wit inspect .019 4.9
array-tiling/rew_true-unreach-call.i timeout 0 wit inspect 900     210 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .022 5.0
array-tiling/rewnif_true-unreach-call.i timeout 0 wit inspect 900     210 11000    - 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-tiling/rewnifrev2_true-unreach-call.i timeout 0 wit inspect 900     380 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.9
array-tiling/rewnifrev_true-unreach-call.i timeout 0 wit inspect 900     390 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.9
array-tiling/rewrev_true-unreach-call.i timeout 0 wit inspect 900     410 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .022 5.0
array-tiling/skipped_true-unreach-call.i timeout 0 wit inspect 900     230 8300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .020 4.8
array-tiling/tcpy_true-unreach-call.i timeout 0 wit inspect 900     180 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 5.0
array-programs/copysome1_false-unreach-call.i timeout 0 wit inspect 900     9300 10000    error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-programs/copysome2_false-unreach-call.i timeout 0 wit inspect 900     9600 10000    error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0010 .34 - wit inspect - wit inspect
array-programs/copysome1_true-unreach-call.i timeout 0 wit inspect 900     9700 10000    - 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-programs/copysome2_true-unreach-call.i timeout 0 wit inspect 900     9600 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 167 34 130000 790000 1500000 44 6 170 5400 44 -224 41 2400 44 0 51 3300 44 -224 4.3 140 123 2 12000 41000 123 2 13000 63000
    correct results 20 34 570 800 6700 6 6 61 2500 0 0 0 1 2 130 920 1 2 420 3500
        correct true 14 28 550 600 6400 0 0 0 0 1 2 130 920 1 2 420 3500
        correct false 6 6 24 190 240 6 6 61 2500 0 0 0 0 0
    correct-unconfimed results 1 0 180 170 2600 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 1 0 180 170 2600 0 0 0 0 0 0
    incorrect results 0 0 7 -224 40 2300 0 7 -224 4.3 130 0 0
        incorrect true 0 0 7 -224 40 2300 0 7 -224 4.3 130 0 0
        incorrect false 0 0 0 0 0 0 0
score (167 tasks, max score: 290) 34 6 -224 0 -224 2 2
Run set esbmc-incr.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Arrays