Tool VeriAbs CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 18:04:04 CET 2017-12-03 04:46:33 CET 2017-12-03 06:08:30 CET 2017-12-03 06:21:09 CET 2017-12-03 06:27:12 CET 2017-12-03 03:55:53 CET 2017-12-03 04:55:47 CET
Run set veriabs.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-ECA; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-ProductLines; sv-comp18.ReachSafety-Recursive; sv-comp18.ReachSafety-Sequentialized] cpa-seq-validate-violation-witnesses-veriabs.[sv-comp18-violation-witness.ReachSafety-Arrays; sv-comp18-violation-witness.ReachSafety-BitVectors; sv-comp18-violation-witness.ReachSafety-ControlFlow; sv-comp18-violation-witness.ReachSafety-ECA; sv-comp18-violation-witness.ReachSafety-Floats; sv-comp18-violation-witness.ReachSafety-Heap; sv-comp18-violation-witness.ReachSafety-Loops; sv-comp18-violation-witness.ReachSafety-ProductLines; sv-comp18-violation-witness.ReachSafety-Recursive; sv-comp18-violation-witness.ReachSafety-Sequentialized] uautomizer-validate-violation-witnesses-veriabs.[sv-comp18-violation-witness.ReachSafety-Arrays; sv-comp18-violation-witness.ReachSafety-BitVectors; sv-comp18-violation-witness.ReachSafety-ControlFlow; sv-comp18-violation-witness.ReachSafety-ECA; sv-comp18-violation-witness.ReachSafety-Floats; sv-comp18-violation-witness.ReachSafety-Heap; sv-comp18-violation-witness.ReachSafety-Loops; sv-comp18-violation-witness.ReachSafety-ProductLines; sv-comp18-violation-witness.ReachSafety-Recursive; sv-comp18-violation-witness.ReachSafety-Sequentialized] cpa-witness2test-validate-violation-witnesses-veriabs.[sv-comp18-violation-witness.ReachSafety-Arrays; sv-comp18-violation-witness.ReachSafety-BitVectors; sv-comp18-violation-witness.ReachSafety-ControlFlow; sv-comp18-violation-witness.ReachSafety-ECA; sv-comp18-violation-witness.ReachSafety-Floats; sv-comp18-violation-witness.ReachSafety-Heap; sv-comp18-violation-witness.ReachSafety-Loops; sv-comp18-violation-witness.ReachSafety-ProductLines; sv-comp18-violation-witness.ReachSafety-Recursive; sv-comp18-violation-witness.ReachSafety-Sequentialized] fshell-witness2test-validate-violation-witnesses-veriabs.[sv-comp18-violation-witness.ReachSafety-Arrays; sv-comp18-violation-witness.ReachSafety-BitVectors; sv-comp18-violation-witness.ReachSafety-ControlFlow; sv-comp18-violation-witness.ReachSafety-ECA; sv-comp18-violation-witness.ReachSafety-Floats; sv-comp18-violation-witness.ReachSafety-Heap; sv-comp18-violation-witness.ReachSafety-Loops; sv-comp18-violation-witness.ReachSafety-ProductLines; sv-comp18-violation-witness.ReachSafety-Recursive; sv-comp18-violation-witness.ReachSafety-Sequentialized] cpa-seq-validate-correctness-witnesses-veriabs.[sv-comp18-correctness-witness.ReachSafety-Arrays; sv-comp18-correctness-witness.ReachSafety-BitVectors; sv-comp18-correctness-witness.ReachSafety-ControlFlow; sv-comp18-correctness-witness.ReachSafety-ECA; sv-comp18-correctness-witness.ReachSafety-Floats; sv-comp18-correctness-witness.ReachSafety-Heap; sv-comp18-correctness-witness.ReachSafety-Loops; sv-comp18-correctness-witness.ReachSafety-ProductLines; sv-comp18-correctness-witness.ReachSafety-Recursive; sv-comp18-correctness-witness.ReachSafety-Sequentialized] uautomizer-validate-correctness-witnesses-veriabs.[sv-comp18-correctness-witness.ReachSafety-Arrays; sv-comp18-correctness-witness.ReachSafety-BitVectors; sv-comp18-correctness-witness.ReachSafety-ControlFlow; sv-comp18-correctness-witness.ReachSafety-ECA; sv-comp18-correctness-witness.ReachSafety-Floats; sv-comp18-correctness-witness.ReachSafety-Heap; sv-comp18-correctness-witness.ReachSafety-Loops; sv-comp18-correctness-witness.ReachSafety-ProductLines; sv-comp18-correctness-witness.ReachSafety-Recursive; sv-comp18-correctness-witness.ReachSafety-Sequentialized]
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
/localhome/dbeyer/comp/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   9100 10000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0038  .32 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unknown 0 wit inspect 780   10000 11000 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0011  .27 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i unknown 0 wit inspect 780   10000 11000 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0012  .30 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unknown 0 wit inspect 690   9400 7500 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0042  .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i unknown 0 wit inspect 690   9600 7800 error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0017  .28 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i timeout 0 wit inspect 900   8100 9900 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .63 49 error (invalid witness file) 0 wit inspect .0012  .30 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 380   2500 5400 timeout 0 wit inspect 92    4000 out of memory 0 wit inspect 61     7000   unknown 0 wit inspect 64    3700 timeout 0 wit inspect 96       130    - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 500   3500 7400 timeout 0 wit inspect 93    4400 out of memory 0 wit inspect 84     7000   unknown 0 wit inspect 59    4400 timeout 0 wit inspect 96       150    - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 620   4500 9300 timeout 0 wit inspect 97    4500 out of memory 0 wit inspect 81     7000   unknown 0 wit inspect 70    4700 timeout 0 wit inspect 96       160    - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 700   5400 10000 timeout 0 wit inspect 91    2000 true -32 wit inspect 4.8   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .57    18    - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 700   6300 10000 timeout 0 wit inspect 91    2000 true -32 wit inspect 4.8   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .70    18    - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 700   7200 8700 timeout 0 wit inspect 91    2100 true -32 wit inspect 5.0   230   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .59    18    - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 700   8200 10000 timeout 0 wit inspect 91    2100 true -32 wit inspect 5.2   230   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .58    18    - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 700   9100 8000 timeout 0 wit inspect 91    2100 true -32 wit inspect 5.3   230   unknown 0 wit inspect 2.2  210 false(unreach-call) 1 wit inspect .58    18    - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 700   10000 9900 timeout 0 wit inspect 91    2100 true -32 wit inspect 3.5   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .62    18    - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 390   2500 5600 timeout 0 wit inspect 92    3600 timeout 0 wit inspect 98     6400   unknown 0 wit inspect 47    3600 timeout 0 wit inspect 96       130    - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 140   1000 1800 timeout 0 wit inspect 92    2200 timeout 0 wit inspect 97     6700   unknown 0 wit inspect 22    1800 timeout 0 wit inspect 96       100    - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 270   1500 3500 timeout 0 wit inspect 92    2900 timeout 0 wit inspect 97     6700   unknown 0 wit inspect 42    2800 timeout 0 wit inspect 96       110    - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 390   2000 5500 timeout 0 wit inspect 92    3600 timeout 0 wit inspect 97     6800   unknown 0 wit inspect 64    3800 timeout 0 wit inspect 96       130    - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 500   2500 6500 timeout 0 wit inspect 92    4500 timeout 0 wit inspect 98     6900   unknown 0 wit inspect 64    4400 timeout 0 wit inspect 96       130    - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 620   3000 9600 timeout 0 wit inspect 97    4600 timeout 0 wit inspect 97     6900   unknown 0 wit inspect 71    4500 timeout 0 wit inspect 96       150    - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 710   3500 9700 timeout 0 wit inspect 92    850 true -32 wit inspect 4.9   220   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .58    18    - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 710   3900 11000 timeout 0 wit inspect 92    850 true -32 wit inspect 5.0   220   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58    18    - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 710   4400 8400 timeout 0 wit inspect 91    910 true -32 wit inspect 6.6   250   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .58    18    - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 710   4800 8800 timeout 0 wit inspect 92    850 true -32 wit inspect 5.0   220   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .61    18    - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 4.4 510 35 timeout 0 wit inspect 92    1900 timeout 0 wit inspect 97     1100   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .58    18    - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i timeout 0 wit inspect 900   8100 11000 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0012  .32 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i timeout 0 wit inspect 900   9200 10000 error (invalid witness file) 0 wit inspect .43 44 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0021  .32 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unknown 0 wit inspect 650   8700 6600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .021 5.0
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i timeout 0 wit inspect 900   9200 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .018 4.9
array-examples/relax_true-unreach-call.i timeout 0 wit inspect 900   9100 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i true 2 wit inspect 8.9 220 90 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2400 timeout 0 wit inspect 960     4900  
array-examples/sanfoundry_10_true-unreach-call_ground.i true 2 wit inspect 16   220 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6400 timeout 0 wit inspect 960     1100  
array-examples/sanfoundry_24_true-unreach-call_true-termination.i true 2 wit inspect 15   210 94 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  490 true 2 wit inspect 8.4   270  
array-examples/sanfoundry_27_true-unreach-call_ground.i true 2 wit inspect 3.9 220 28 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2400 timeout 0 wit inspect 960     2800  
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect 3.3 220 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 true 2 wit inspect 4.8   220  
array-examples/sorting_bubblesort_true-unreach-call_ground.i unknown 0 wit inspect 780   10000 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .021 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i unknown 0 wit inspect 690   9200 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i true 2 wit inspect 3.6 220 24 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 timeout 0 wit inspect 960     2500  
array-examples/standard_compare_true-unreach-call_ground.i true 2 wit inspect 3.5 220 20 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 timeout 0 wit inspect 960     4800  
array-examples/standard_copy1_true-unreach-call_ground.i true 2 wit inspect 3.6 220 23 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 timeout 0 wit inspect 960     4800  
array-examples/standard_copy2_true-unreach-call_ground.i true 2 wit inspect 3.6 230 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 timeout 0 wit inspect 960     4800  
array-examples/standard_copy3_true-unreach-call_ground.i true 2 wit inspect 3.8 220 24 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5800 timeout 0 wit inspect 960     4800  
array-examples/standard_copy4_true-unreach-call_ground.i true 2 wit inspect 3.5 220 28 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 timeout 0 wit inspect 960     4900  
array-examples/standard_copy5_true-unreach-call_ground.i true 2 wit inspect 3.6 220 29 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 timeout 0 wit inspect 960     4900  
array-examples/standard_copy6_true-unreach-call_ground.i true 2 wit inspect 3.5 220 26 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 timeout 0 wit inspect 960     4900  
array-examples/standard_copy7_true-unreach-call_ground.i true 2 wit inspect 3.9 220 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 840    7000 timeout 0 wit inspect 960     4900  
array-examples/standard_copy8_true-unreach-call_ground.i true 2 wit inspect 3.7 230 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 870    7000 timeout 0 wit inspect 960     5100  
array-examples/standard_copy9_true-unreach-call_ground.i true 2 wit inspect 3.7 230 25 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6800 timeout 0 wit inspect 960     5000  
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true 2 wit inspect 16   220 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 timeout 0 wit inspect 960     4900  
array-examples/standard_copyInitSum3_true-unreach-call_ground.i true 2 wit inspect 3.4 220 24 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 timeout 0 wit inspect 960     5000  
array-examples/standard_copyInitSum_true-unreach-call_ground.i true 2 wit inspect 31   220 310 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     4800  
array-examples/standard_copyInit_true-unreach-call_ground.i true 2 wit inspect 16   220 99 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     4800  
array-examples/standard_find_true-unreach-call_ground.i true 2 wit inspect 16   220 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 timeout 0 wit inspect 960     4800  
array-examples/standard_init1_true-unreach-call_ground.i true 2 wit inspect 15   220 92 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 timeout 0 wit inspect 960     2100  
array-examples/standard_init2_true-unreach-call_ground.i true 2 wit inspect 15   220 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 timeout 0 wit inspect 960     3300  
array-examples/standard_init3_true-unreach-call_ground.i true 2 wit inspect 16   220 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 timeout 0 wit inspect 960     4900  
array-examples/standard_init4_true-unreach-call_ground.i true 2 wit inspect 16   220 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 timeout 0 wit inspect 960     5200  
array-examples/standard_init5_true-unreach-call_ground.i true 2 wit inspect 16   220 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 timeout 0 wit inspect 960     5200  
array-examples/standard_init6_true-unreach-call_ground.i true 2 wit inspect 15   220 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 timeout 0 wit inspect 960     5500  
array-examples/standard_init7_true-unreach-call_ground.i true 2 wit inspect 16   210 130 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 timeout 0 wit inspect 960     5500  
array-examples/standard_init8_true-unreach-call_ground.i true 2 wit inspect 17   220 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 timeout 0 wit inspect 960     4900  
array-examples/standard_init9_true-unreach-call_ground.i true 2 wit inspect 16   210 130 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 timeout 0 wit inspect 960     5600  
array-examples/standard_maxInArray_true-unreach-call_ground.i true 2 wit inspect 4.2 220 27 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 timeout 0 wit inspect 960     2600  
array-examples/standard_minInArray_true-unreach-call_ground.i true 2 wit inspect 4.2 220 26 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 timeout 0 wit inspect 960     2500  
array-examples/standard_palindrome_true-unreach-call_ground.i true 2 wit inspect 19   220 160 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 timeout 0 wit inspect 960     1600  
array-examples/standard_partial_init_true-unreach-call_ground.i true 2 wit inspect 15   210 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 timeout 0 wit inspect 960     4000  
array-examples/standard_partition_original_true-unreach-call_ground.i true 2 wit inspect 16   220 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 out of memory 0 wit inspect 85     7000  
array-examples/standard_partition_true-unreach-call_ground.i true 2 wit inspect 16   220 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5600 timeout 0 wit inspect 960     5300  
array-examples/standard_password_true-unreach-call_ground.i true 2 wit inspect 3.3 220 22 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6200 timeout 0 wit inspect 960     4800  
array-examples/standard_reverse_true-unreach-call_ground.i true 2 wit inspect 16   220 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 timeout 0 wit inspect 960     2000  
array-examples/standard_running_true-unreach-call.i true 2 wit inspect 17   220 89 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5600 timeout 0 wit inspect 960     740  
array-examples/standard_sentinel_true-unreach-call_true-termination.i true 2 wit inspect 100   750 870 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1000 true 2 wit inspect 9.0   320  
array-examples/standard_seq_init_true-unreach-call_ground.i true 2 wit inspect 3.4 220 21 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2400 timeout 0 wit inspect 960     2200  
array-examples/standard_strcmp_true-unreach-call_ground.i true 2 wit inspect 3.5 220 23 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     4600  
array-examples/standard_strcpy_original_true-unreach-call.i true 2 wit inspect 16   220 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 timeout 0 wit inspect 960     4800  
array-examples/standard_strcpy_true-unreach-call_ground.i true 2 wit inspect 15   210 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 timeout 0 wit inspect 960     3900  
array-examples/standard_two_index_01_true-unreach-call.i true 2 wit inspect 15   220 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     3200  
array-examples/standard_two_index_02_true-unreach-call.i true 2 wit inspect 15   220 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 timeout 0 wit inspect 960     3200  
array-examples/standard_two_index_03_true-unreach-call.i true 2 wit inspect 17   220 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 timeout 0 wit inspect 960     3300  
array-examples/standard_two_index_04_true-unreach-call.i true 2 wit inspect 16   220 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     3200  
array-examples/standard_two_index_05_true-unreach-call.i true 2 wit inspect 16   220 97 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 timeout 0 wit inspect 960     3000  
array-examples/standard_two_index_06_true-unreach-call.i true 2 wit inspect 16   220 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 timeout 0 wit inspect 960     3500  
array-examples/standard_two_index_07_true-unreach-call.i true 2 wit inspect 17   220 96 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 timeout 0 wit inspect 960     3200  
array-examples/standard_two_index_08_true-unreach-call.i true 2 wit inspect 17   220 92 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 timeout 0 wit inspect 960     3200  
array-examples/standard_two_index_09_true-unreach-call.i true 2 wit inspect 17   220 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 timeout 0 wit inspect 960     2900  
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i true 2 wit inspect 15   210 100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    7000 timeout 0 wit inspect 960     4500  
array-examples/standard_vector_difference_true-unreach-call_ground.i true 2 wit inspect 3.6 220 23 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 timeout 0 wit inspect 960     1900  
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i timeout 0 wit inspect 900   8700 9300 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .70 49 error (invalid witness file) 0 wit inspect .0020  .26 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i out of memory 0 wit inspect 220   15000 2400 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0015  .28 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16   220 100 timeout 0 wit inspect 92    2100 true -32 wit inspect 4.8   230   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .58    18    - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i false(unreach-call) 1 wit inspect 120   210 1500 timeout 0 wit inspect 92    1200 timeout 0 wit inspect 97     4700   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .60    18    - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 16   220 120 timeout 0 wit inspect 92    2100 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.0  210 true -32 wit inspect .58    18    - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 900   9100 9000 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0021  .28 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i true 2 wit inspect 15   220 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     3800  
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i timeout 0 wit inspect 900   9000 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i true 2 wit inspect 17   220 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     4900  
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i true 2 wit inspect 19   220 140 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 timeout 0 wit inspect 960     5900  
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i true 2 wit inspect 93   1200 780 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 true 2 wit inspect 12     470  
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i true 2 wit inspect 21   220 140 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 timeout 0 wit inspect 960     5900  
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i true 2 wit inspect 22   220 180 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5800 timeout 0 wit inspect 960     5900  
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i true 2 wit inspect 20   220 150 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 770    7000 timeout 0 wit inspect 960     5900  
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i true 2 wit inspect 17   220 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 timeout 0 wit inspect 960     5900  
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i true 2 wit inspect 22   220 170 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     5900  
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i true 2 wit inspect 15   220 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5600 timeout 0 wit inspect 960     4600  
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 61   510 670 true -32 wit inspect 4.1  260 false(unreach-call) 1 wit inspect 8.3   350   unknown 0 wit inspect 3.5  220 false(unreach-call) 1 wit inspect .62    20    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 70   510 780 true -32 wit inspect 5.0  290 out of memory 0 wit inspect 58     7000   unknown 0 wit inspect 2.8  220 true -32 wit inspect .66    20    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 0 wit inspect 89   1000 930 true -32 wit inspect 6.0  280 out of memory 0 wit inspect 54     7000   unknown 0 wit inspect 4.2  230 true -32 wit inspect .70    22    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 140   2700 1300 true -32 wit inspect 4.4  290 out of memory 0 wit inspect 65     7000   unknown 0 wit inspect 3.3  220 false(unreach-call) 1 wit inspect .79    25    - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect 270   3800 3400 true -32 wit inspect 5.1  330 out of memory 0 wit inspect 71     7000   unknown 0 wit inspect 6.0  330 false(unreach-call) 1 wit inspect .90    28    - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 180   590 2000 unknown 0 wit inspect 5.1  360 false(unreach-call) 1 wit inspect 16     480   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .64    19    - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i true 2 wit inspect 3.6 220 23 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1500 timeout 0 wit inspect 960     5300  
reducercommutativity/avg10_true-unreach-call_true-termination.i true 2 wit inspect 3.5 220 26 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 out of memory 0 wit inspect 860     7000  
reducercommutativity/avg20_true-unreach-call.i true 2 wit inspect 3.4 230 25 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 timeout 0 wit inspect 960     1900  
reducercommutativity/avg40_true-unreach-call.i true 2 wit inspect 3.6 220 26 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     4300  
reducercommutativity/avg60_true-unreach-call.i true 2 wit inspect 3.6 220 23 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 timeout 0 wit inspect 960     3100  
reducercommutativity/avg_true-unreach-call_true-termination.i true 2 wit inspect 2.0 150 17 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3100 timeout 0 wit inspect 960     590  
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 4.1 220 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 110    910 timeout 0 wit inspect 960     1400  
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 4.3 220 32 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 timeout 0 wit inspect 960     2700  
reducercommutativity/max20_true-unreach-call.i true 2 wit inspect 4.0 220 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 timeout 0 wit inspect 960     4600  
reducercommutativity/max40_true-unreach-call.i true 2 wit inspect 4.1 230 32 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1700 timeout 0 wit inspect 960     4700  
reducercommutativity/max60_true-unreach-call.i true 2 wit inspect 4.1 220 28 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3200 timeout 0 wit inspect 960     4600  
reducercommutativity/max_true-unreach-call_true-termination.i true 2 wit inspect 7.0 160 76 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3300 timeout 0 wit inspect 960     1000  
reducercommutativity/sep05_true-unreach-call_true-termination.i true 2 wit inspect 120   720 1200 - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 6.8  270 timeout 0 wit inspect 960     1800  
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect 130   950 1300 - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 5.0  270 timeout 0 wit inspect 960     6800  
reducercommutativity/sep20_true-unreach-call.i true 2 wit inspect 150   1100 1600 - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 5.8  290 timeout 0 wit inspect 910     7000  
reducercommutativity/sep40_true-unreach-call.i true 2 wit inspect 220   830 2500 - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 5.3  280 timeout 0 wit inspect 960     4400  
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 900   510 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/sep_true-unreach-call_true-termination.i timeout 0 wit inspect 900   2700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .022 4.9
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 3.6 220 24 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    950 true 2 wit inspect 420     2900  
reducercommutativity/sum10_true-unreach-call_true-termination.i true 2 wit inspect 3.4 220 24 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2100 timeout 0 wit inspect 960     5100  
reducercommutativity/sum20_true-unreach-call.i true 2 wit inspect 3.4 220 23 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 timeout 0 wit inspect 960     4600  
reducercommutativity/sum40_true-unreach-call.i true 2 wit inspect 3.5 220 24 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 timeout 0 wit inspect 960     4100  
reducercommutativity/sum60_true-unreach-call.i true 2 wit inspect 3.6 220 23 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3300 timeout 0 wit inspect 960     2700  
reducercommutativity/sum_true-unreach-call_true-termination.i true 2 wit inspect 1.7 150 15 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3300 timeout 0 wit inspect 960     4700  
array-tiling/mlceu_false-unreach-call.i false(unreach-call) 0 wit inspect 15   220 110 timeout 0 wit inspect 91    1800 true -32 wit inspect 4.7   230   unknown 0 wit inspect 2.6  210 true -32 wit inspect .57    18    - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i false(unreach-call) 0 wit inspect 22   220 190 error (invalid witness file) 0 wit inspect 1.8  170 false(unreach-call) 1 wit inspect 16     520   error (invalid witness file) 0 wit inspect 2.6  170 error (1) 0 wit inspect .57    18    - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i true 2 wit inspect 16   220 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 error (7) 0 wit inspect 22     320  
array-tiling/mbpr3_true-unreach-call.i true 2 wit inspect 20   220 140 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5400 timeout 0 wit inspect 960     1100  
array-tiling/mbpr4_true-unreach-call.i true 2 wit inspect 28   220 250 - wit inspect -