Tool PeSCo 1.7-svn b8d6131600+ CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
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* [apollon004; apollon069; apollon137; apollon154] [apollon004; apollon006; apollon021; apollon061; apollon109; apollon155] apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 12:44:04 CET 2018-12-08 07:39:30 CET 2018-12-08 12:16:42 CET 2018-12-08 13:32:07 CET 2018-12-12 20:37:42 CET 2018-12-08 05:07:50 CET 2018-12-08 09:11:31 CET
Run set pesco.sv-comp19_prop-reachsafety.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Arrays uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Arrays
Options -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i unknown 0 --- inspect 100 74   2800 1000 0      0     error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .61 46 0   0   error (invalid witness file) 0 --- inspect .0058 .0075 .53 0     0      - --- inspect - --- inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i timeout 0 wit inspect 960 510   4500 7000 0      0     error (invalid witness file) 0 --- inspect .75 .45 43 0   0   error (invalid witness file) 0 --- inspect 5.0   3.2   260   .65 0   error (invalid witness file) 0 --- inspect .96 .62 49 0   0   error (invalid witness file) 0 --- inspect .0052 .0064 .53 0     0      - --- inspect - --- inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i timeout 0 wit inspect 960 510   4700 7200 0      0     error (invalid witness file) 0 --- inspect .66 .41 44 0   0   error (invalid witness file) 0 --- inspect 5.4   2.9   250   .61 0   error (invalid witness file) 0 --- inspect .99 .62 49 0   0   error (invalid witness file) 0 --- inspect .0023 .0029 .54 0     0      - --- inspect - --- inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i timeout 0 wit inspect 960 470   6700 8600 0      0     error (invalid witness file) 0 --- inspect .67 .42 42 0   0   error (invalid witness file) 0 --- inspect 5.7   3.2   260   .65 0   error (invalid witness file) 0 --- inspect 1.0  .68 49 0   0   error (invalid witness file) 0 --- inspect .0018 .0028 .53 0     0      - --- inspect - --- inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i timeout 0 wit inspect 960 480   8300 9700 0      0     error (invalid witness file) 0 --- inspect .64 .39 42 0   0   error (invalid witness file) 0 --- inspect 5.5   3.0   270   .65 0   error (invalid witness file) 0 --- inspect 1.1  .68 50 0   0   error (invalid witness file) 0 --- inspect .0022 .0030 .53 0     0      - --- inspect - --- inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i timeout 0 wit inspect 920 890   12000 10000 0      0     timeout 0 wit inspect 92    77    1600 0   0   timeout 0 --- inspect 97     69     1100   1.3  0   unknown 0 --- inspect 1.1  .68 50 0   0   error (1) 0 --- inspect .091  .089  11    0     0      - --- inspect - --- inspect
array-examples/standard_copy1_false-unreach-call_ground.i timeout 0 wit inspect 970 490   5600 8900 0      0     error (invalid witness file) 0 --- inspect .73 .45 42 0   0   error (invalid witness file) 0 --- inspect 5.2   3.3   260   .65 0   error (invalid witness file) 0 --- inspect .98 .64 50 0   0   error (invalid witness file) 0 --- inspect .0058 .0070 .53 0     0      - --- inspect - --- inspect
array-examples/standard_copy2_false-unreach-call_ground.i timeout 0 wit inspect 960 500   6000 8000 0      0     error (invalid witness file) 0 --- inspect .62 .38 43 0   0   error (invalid witness file) 0 --- inspect 5.1   3.3   260   .65 0   error (invalid witness file) 0 --- inspect .99 .64 51 0   0   error (invalid witness file) 0 --- inspect .0056 .0070 .53 0     0      - --- inspect - --- inspect
array-examples/standard_copy3_false-unreach-call_ground.i timeout 0 wit inspect 960 490   5800 8200 0      0     error (invalid witness file) 0 --- inspect .74 .46 43 0   0   error (invalid witness file) 0 --- inspect 5.2   2.9   270   .61 0   error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0   error (invalid witness file) 0 --- inspect .0049 .0055 .39 0     0      - --- inspect - --- inspect
array-examples/standard_copy4_false-unreach-call_ground.i timeout 0 wit inspect 900 880   8800 12000 0      0     timeout 0 wit inspect 93    73    2500 0   0   timeout 0 --- inspect 96     75     2600   1.5  0   unknown 0 --- inspect 1.2  .75 58 0   0   error (1) 0 --- inspect .078  .077  12    0     0      - --- inspect - --- inspect
array-examples/standard_copy5_false-unreach-call_ground.i timeout 0 wit inspect 960 480   5300 8800 0      0     error (invalid witness file) 0 --- inspect .67 .41 42 0   0   error (invalid witness file) 0 --- inspect 6.1   3.6   270   .65 0   error (invalid witness file) 0 --- inspect .99 .66 49 0   0   error (invalid witness file) 0 --- inspect .0017 .0021 .53 0     0      - --- inspect - --- inspect
array-examples/standard_copy6_false-unreach-call_ground.i timeout 0 wit inspect 960 490   5700 8800 0      0     error (invalid witness file) 0 --- inspect .80 .49 43 0   0   error (invalid witness file) 0 --- inspect 5.5   3.4   250   .65 0   error (invalid witness file) 0 --- inspect .98 .63 50 0   0   error (invalid witness file) 0 --- inspect .0059 .0075 .53 0     0      - --- inspect - --- inspect
array-examples/standard_copy7_false-unreach-call_ground.i timeout 0 wit inspect 960 490   6900 8800 0      0     error (invalid witness file) 0 --- inspect .67 .41 44 0   0   error (invalid witness file) 0 --- inspect 5.5   3.0   260   .65 0   error (invalid witness file) 0 --- inspect 1.1  .69 48 0   0   error (invalid witness file) 0 --- inspect .0017 .0021 .53 0     0      - --- inspect - --- inspect
array-examples/standard_copy8_false-unreach-call_ground.i timeout 0 wit inspect 960 490   4500 11000 0      0     error (invalid witness file) 0 --- inspect .64 .40 44 0   0   error (invalid witness file) 0 --- inspect 5.8   3.0   280   .65 0   error (invalid witness file) 0 --- inspect 1.0  .66 50 0   0   error (invalid witness file) 0 --- inspect .0046 .0058 .53 0     0      - --- inspect - --- inspect
array-examples/standard_copy9_false-unreach-call_ground.i timeout 0 wit inspect 960 490   5200 8800 0      0     error (invalid witness file) 0 --- inspect .75 .48 43 0   0   error (invalid witness file) 0 --- inspect 5.4   3.3   260   .65 0   error (invalid witness file) 0 --- inspect 1.0  .65 49 0   0   error (invalid witness file) 0 --- inspect .0022 .0025 .39 0     0      - --- inspect - --- inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i timeout 0 wit inspect 960 490   3900 7500 0      0     error (invalid witness file) 0 --- inspect .61 .38 43 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   270   .65 0   error (invalid witness file) 0 --- inspect 1.0  .66 48 0   0   error (invalid witness file) 0 --- inspect .0049 .0061 .54 0     0      - --- inspect - --- inspect
array-examples/standard_init1_false-unreach-call_ground.i timeout 0 wit inspect 960 500   6800 8400 0      0     error (invalid witness file) 0 --- inspect .65 .40 44 0   0   error (invalid witness file) 0 --- inspect 6.8   3.7   280   .65 0   error (invalid witness file) 0 --- inspect 1.2  .77 49 0   0   error (invalid witness file) 0 --- inspect .0050 .0062 .52 0     0      - --- inspect - --- inspect
array-examples/standard_init2_false-unreach-call_ground.i timeout 0 wit inspect 960 500   6600 8200 0      0     error (invalid witness file) 0 --- inspect .65 .39 42 0   0   error (invalid witness file) 0 --- inspect 5.9   3.2   260   .61 0   error (invalid witness file) 0 --- inspect 1.0  .64 49 0   0   error (invalid witness file) 0 --- inspect .0017 .0021 .52 0     0      - --- inspect - --- inspect
array-examples/standard_init3_false-unreach-call_ground.i timeout 0 wit inspect 960 490   5900 8800 0      0     error (invalid witness file) 0 --- inspect .69 .44 42 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   260   .65 0   error (invalid witness file) 0 --- inspect 1.1  .70 50 0   0   error (invalid witness file) 0 --- inspect .0054 .0069 .52 0     0      - --- inspect - --- inspect
array-examples/standard_init4_false-unreach-call_ground.i timeout 0 wit inspect 960 490   5200 9400 0      0     error (invalid witness file) 0 --- inspect .64 .39 44 0   0   error (invalid witness file) 0 --- inspect 5.4   2.9   260   .65 0   error (invalid witness file) 0 --- inspect .98 .65 50 0   0   error (invalid witness file) 0 --- inspect .0019 .0028 .53 0     0      - --- inspect - --- inspect
array-examples/standard_init5_false-unreach-call_ground.i timeout 0 wit inspect 970 490   5300 7800 0      0     error (invalid witness file) 0 --- inspect .79 .48 43 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   270   .61 0   error (invalid witness file) 0 --- inspect .99 .64 49 0   0   error (invalid witness file) 0 --- inspect .0054 .0065 .52 0     0      - --- inspect - --- inspect
array-examples/standard_init6_false-unreach-call_ground.i timeout 0 wit inspect 960 490   5000 8800 0      0     error (invalid witness file) 0 --- inspect .64 .42 42 0   0   error (invalid witness file) 0 --- inspect 5.2   2.8   270   .65 0   error (invalid witness file) 0 --- inspect .99 .62 50 0   0   error (invalid witness file) 0 --- inspect .0051 .0069 .52 0     0      - --- inspect - --- inspect
array-examples/standard_init7_false-unreach-call_ground.i timeout 0 wit inspect 960 490   5200 7900 0      0     error (invalid witness file) 0 --- inspect .64 .39 42 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   260   .65 0   error (invalid witness file) 0 --- inspect 1.0  .67 49 0   0   error (invalid witness file) 0 --- inspect .0037 .0062 .52 0     0      - --- inspect - --- inspect
array-examples/standard_init8_false-unreach-call_ground.i timeout 0 wit inspect 970 490   5100 8600 0      0     error (invalid witness file) 0 --- inspect .71 .42 42 0   0   error (invalid witness file) 0 --- inspect 6.4   3.8   270   .65 0   error (invalid witness file) 0 --- inspect .97 .63 49 0   0   error (invalid witness file) 0 --- inspect .0016 .0021 .53 0     0      - --- inspect - --- inspect
array-examples/standard_init9_false-unreach-call_ground.i timeout 0 wit inspect 970 490   7000 7800 0      0     error (invalid witness file) 0 --- inspect .63 .39 43 0   0   error (invalid witness file) 0 --- inspect 5.1   3.3   260   .65 0   error (invalid witness file) 0 --- inspect .96 .62 49 0   0   error (invalid witness file) 0 --- inspect .0059 .0080 .52 0     0      - --- inspect - --- inspect
array-examples/standard_minInArray_false-unreach-call_ground.i timeout 0 wit inspect 960 490   4800 9000 0      0     error (invalid witness file) 0 --- inspect .66 .41 42 0   0   error (invalid witness file) 0 --- inspect 5.7   3.0   270   .61 0   error (invalid witness file) 0 --- inspect .98 .63 49 0   0   error (invalid witness file) 0 --- inspect .0065 .0084 .52 0     0      - --- inspect - --- inspect
array-examples/standard_partition_false-unreach-call_ground.i timeout 0 wit inspect 960 510   4300 7600 0      0     error (invalid witness file) 0 --- inspect .66 .42 43 0   0   error (invalid witness file) 0 --- inspect 5.4   2.9   260   .61 0   error (invalid witness file) 0 --- inspect .94 .60 49 0   0   error (invalid witness file) 0 --- inspect .0045 .0054 .53 0     0      - --- inspect - --- inspect
array-examples/standard_running_false-unreach-call.i timeout 0 wit inspect 960 500   4800 10000 0      0     error (invalid witness file) 0 --- inspect .77 .48 42 0   0   error (invalid witness file) 0 --- inspect 5.7   3.5   270   .65 0   error (invalid witness file) 0 --- inspect 1.0  .68 49 0   0   error (invalid witness file) 0 --- inspect .0059 .0064 .39 0     0      - --- inspect - --- inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i true 2 wit inspect 11 3.6 1200 80 0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 770    670    7000 0   0   true 2 --- inspect 9.5   5.4   310   .66 0     
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unknown 0 --- inspect 100 83   2000 1300 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 43 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0     
array-examples/relax_true-unreach-call.i timeout 0 wit inspect 960 440   5100 10000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .85 .50 43 0   0   error (invalid witness file) 0 --- inspect 5.5   3.3   270   .61 0     
array-examples/sanfoundry_02_true-unreach-call_ground.i timeout 0 wit inspect 960 500   4100 9000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .85 .50 43 0   0   error (invalid witness file) 0 --- inspect 6.3   3.7   260   .65 0     
array-examples/sanfoundry_10_true-unreach-call_ground.i out of memory 0 --- inspect 840 810   15000 11000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .40 42 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0     
array-examples/sanfoundry_24_true-unreach-call_true-termination.i true 2 wit inspect 18 4.7 1400 130 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.8  4.6  530 0   0   false(unreach-call) -16 --- inspect 39     25     580   .62 0     
array-examples/sanfoundry_27_true-unreach-call_ground.i timeout 0 wit inspect 960 500   5200 9100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 42 0   0   error (invalid witness file) 0 --- inspect 5.6   3.0   270   .65 0     
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect 13 3.6 1000 93 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  270 0   0   true 2 --- inspect 6.5   3.7   300   .62 0     
array-examples/sorting_bubblesort_true-unreach-call_ground.i timeout 0 wit inspect 960 500   4500 7700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 43 0   0   error (invalid witness file) 0 --- inspect 5.3   3.2   270   .65 0     
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 0 wit inspect 960 470   6800 9700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .41 43 0   0   error (invalid witness file) 0 --- inspect 6.1   3.3   270   .65 0     
array-examples/standard_compareModified_true-unreach-call_ground.i timeout 0 wit inspect 900 870   7300 12000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    880    4400 0   0   timeout 0 --- inspect 960     870     6300   .64 0     
array-examples/standard_compare_true-unreach-call_ground.i timeout 0 wit inspect 900 880   1800 11000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    4300 0   0   timeout 0 --- inspect 960     900     1400   .64 0     
array-examples/standard_copy1_true-unreach-call_ground.i timeout 0 wit inspect 960 490   4900 11000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 43 0   0   error (invalid witness file) 0 --- inspect 5.6   3.1   260   .65 0     
array-examples/standard_copy2_true-unreach-call_ground.i timeout 0 wit inspect 960 490   5300 8800 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .47 44 0   0   error (invalid witness file) 0 --- inspect 5.5   3.0   250   .65 0     
array-examples/standard_copy3_true-unreach-call_ground.i timeout 0 wit inspect 970 500   5800 8100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 43 0   0   error (invalid witness file) 0 --- inspect 5.5   3.0   260   .61 0     
array-examples/standard_copy4_true-unreach-call_ground.i timeout 0 wit inspect 900 880   7800 14000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4500 0   0   timeout 0 --- inspect 960     920     5400   .67 0     
array-examples/standard_copy5_true-unreach-call_ground.i timeout 0 wit inspect 960 490   6000 9900 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 42 0   0   error (invalid witness file) 0 --- inspect 5.3   3.3   260   .65 0     
array-examples/standard_copy6_true-unreach-call_ground.i timeout 0 wit inspect 970 490   7300 9200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 43 0   0   error (invalid witness file) 0 --- inspect 5.9   3.2   260   .65 0     
array-examples/standard_copy7_true-unreach-call_ground.i timeout 0 wit inspect 960 490   6000 9400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .94 .58 44 0   0   error (invalid witness file) 0 --- inspect 5.1   2.8   270   .65 0     
array-examples/standard_copy8_true-unreach-call_ground.i timeout 0 wit inspect 960 490   7200 9200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 43 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   270   .65 0     
array-examples/standard_copy9_true-unreach-call_ground.i timeout 0 wit inspect 960 490   6200 10000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .50 44 0   0   error (invalid witness file) 0 --- inspect 6.9   4.0   270   .65 0     
array-examples/standard_copyInitSum2_true-unreach-call_ground.i timeout 0 wit inspect 970 490   5900 8500 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .52 43 0   0   error (invalid witness file) 0 --- inspect 4.9   2.7   260   .65 0     
array-examples/standard_copyInitSum3_true-unreach-call_ground.i timeout 0 wit inspect 960 490   4400 8600 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .50 43 0   0   error (invalid witness file) 0 --- inspect 5.4   2.9   250   .65 0     
array-examples/standard_copyInitSum_true-unreach-call_ground.i timeout 0 wit inspect 970 490   3800 8400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 42 0   0   error (invalid witness file) 0 --- inspect 5.5   3.0   260   .65 0     
array-examples/standard_copyInit_true-unreach-call_ground.i timeout 0 wit inspect 970 490   7700 7700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 43 0   0   error (invalid witness file) 0 --- inspect 5.3   2.8   270   .65 0     
array-examples/standard_find_true-unreach-call_ground.i timeout 0 wit inspect 900 870   7400 13000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    870    4500 0   0   timeout 0 --- inspect 960     830     6800   .72 0     
array-examples/standard_init1_true-unreach-call_ground.i timeout 0 wit inspect 960 500   6700 8400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .40 43 0   0   error (invalid witness file) 0 --- inspect 6.5   3.8   270   .65 0     
array-examples/standard_init2_true-unreach-call_ground.i timeout 0 wit inspect 970 490   7700 8400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 43 0   0   error (invalid witness file) 0 --- inspect 5.0   2.8   270   .65 0     
array-examples/standard_init3_true-unreach-call_ground.i timeout 0 wit inspect 960 490   7500 8200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .50 43 0   0   error (invalid witness file) 0 --- inspect 5.7   3.4   270   .65 0     
array-examples/standard_init4_true-unreach-call_ground.i timeout 0 wit inspect 960 490   5500 8500 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .49 42 0   0   error (invalid witness file) 0 --- inspect 5.6   3.1   260   .65 0     
array-examples/standard_init5_true-unreach-call_ground.i timeout 0 wit inspect 960 490   4900 8000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .50 43 0   0   error (invalid witness file) 0 --- inspect 5.5   3.0   270   .65 0     
array-examples/standard_init6_true-unreach-call_ground.i timeout 0 wit inspect 960 490   5200 7800 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 43 0   0   error (invalid witness file) 0 --- inspect 5.5   3.0   260   .65 0     
array-examples/standard_init7_true-unreach-call_ground.i timeout 0 wit inspect 970 490   7300 9400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 43 0   0   error (invalid witness file) 0 --- inspect 5.2   2.8   260   .65 0     
array-examples/standard_init8_true-unreach-call_ground.i timeout 0 wit inspect 970 490   6900 9200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 44 0   0   error (invalid witness file) 0 --- inspect 5.5   2.9   280   .65 0     
array-examples/standard_init9_true-unreach-call_ground.i timeout 0 wit inspect 960 490   7100 8400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0   error (invalid witness file) 0 --- inspect 5.4   3.3   260   .65 0     
array-examples/standard_maxInArray_true-unreach-call_ground.i timeout 0 wit inspect 960 490   4700 7200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 42 0   0   error (invalid witness file) 0 --- inspect 6.0   3.2   260   .65 0     
array-examples/standard_minInArray_true-unreach-call_ground.i timeout 0 wit inspect 970 500   6100 9900 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .92 .55 42 0   0   error (invalid witness file) 0 --- inspect 5.7   3.1   270   .65 0     
array-examples/standard_palindrome_true-unreach-call_ground.i timeout 0 wit inspect 970 490   7400 10000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 42 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   270   .65 0     
array-examples/standard_partial_init_true-unreach-call_ground.i timeout 0 wit inspect 960 520   4800 7600 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .39 43 0   0   error (invalid witness file) 0 --- inspect 6.2   3.6   260   .65 0     
array-examples/standard_partition_original_true-unreach-call_ground.i timeout 0 wit inspect 960 520   5400 9100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 42 0   0   error (invalid witness file) 0 --- inspect 5.3   3.3   270   .65 0     
array-examples/standard_partition_true-unreach-call_ground.i timeout 0 wit inspect 960 520   4000 9200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 43 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   270   .65 0     
array-examples/standard_password_true-unreach-call_ground.i timeout 0 wit inspect 900 880   2300 12000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    4500 0   0   timeout 0 --- inspect 960     900     1200   .66 0     
array-examples/standard_reverse_true-unreach-call_ground.i unknown 0 --- inspect 100 91   1500 1300 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 40 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0     
array-examples/standard_running_true-unreach-call.i timeout 0 wit inspect 970 490   3900 8200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 44 0   0   error (invalid witness file) 0 --- inspect 5.4   2.9   260   .65 0     
array-examples/standard_sentinel_true-unreach-call_true-termination.i true 2 wit inspect 15 4.6 1200 98 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1700 0   0   true 2 --- inspect 15     8.8   530   .66 0     
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 0 wit inspect 900 870   7600 11000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3700 0   0   timeout 0 --- inspect 960     860     6400   1.6  0     
array-examples/standard_strcmp_true-unreach-call_ground.i timeout 0 wit inspect 970 480   7000 8400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 43 0   0   error (invalid witness file) 0 --- inspect 5.1   3.2   260   .65 0     
array-examples/standard_strcpy_original_true-unreach-call.i timeout 0 wit inspect 960 490   6900 7500 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 43 0   0   error (invalid witness file) 0 --- inspect 5.2   3.3   270   .65 0     
array-examples/standard_strcpy_true-unreach-call_ground.i timeout 0 wit inspect 970 490   6400 9200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .51 42 0   0   error (invalid witness file) 0 --- inspect 6.4   3.4   260   .65 0     
array-examples/standard_two_index_01_true-unreach-call.i timeout 0 wit inspect 960 420   9900 10000 30      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 42 0   0   error (invalid witness file) 0 --- inspect 6.0   3.3   260   .65 0     
array-examples/standard_two_index_02_true-unreach-call.i timeout 0 wit inspect 960 500   5800 9100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 42 0   0   error (invalid witness file) 0 --- inspect 5.1   2.8   250   .65 0     
array-examples/standard_two_index_03_true-unreach-call.i timeout 0 wit inspect 960 450   7600 8200 18      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .84 .50 43 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   270   .65 0     
array-examples/standard_two_index_04_true-unreach-call.i timeout 0 wit inspect 960 500   6500 9800 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 45 0   0   error (invalid witness file) 0 --- inspect 5.1   3.2   270   .65 0     
array-examples/standard_two_index_05_true-unreach-call.i timeout 0 wit inspect 960 490   7700 9400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 43 0   0   error (invalid witness file) 0 --- inspect 6.2   3.7   270   .61 0     
array-examples/standard_two_index_06_true-unreach-call.i timeout 0 wit inspect 970 440   8000 9200 15      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 44 0   0   error (invalid witness file) 0 --- inspect 5.9   3.5   270   .65 0     
array-examples/standard_two_index_07_true-unreach-call.i timeout 0 wit inspect 960 490   5400 8400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 43 0   0   error (invalid witness file) 0 --- inspect 5.8   3.1   260   .65 0     
array-examples/standard_two_index_08_true-unreach-call.i timeout 0 wit inspect 960 490   4900 8500 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 43 0   0   error (invalid witness file) 0 --- inspect 5.5   3.0   270   .65 0     
array-examples/standard_two_index_09_true-unreach-call.i timeout 0 wit inspect 970 490   7900 8700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 42 0   0   error (invalid witness file) 0 --- inspect 5.2   2.8   260   .65 0     
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i timeout 0 wit inspect 940 460   5900 7100 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 580    550    7000 0   0   error (7) 0 --- inspect 16     9.4   300   .75 0     
array-examples/standard_vector_difference_true-unreach-call_ground.i timeout 0 wit inspect 960 490   6100 7700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 43 0   0   error (invalid witness file) 0 --- inspect 5.1   3.3   270   .61 0     
array-examples/standard_sentinel_true-unreach-call.i.v+cfa-reducer.c timeout 0 wit inspect 960 460   5100 12000 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 42 0   0   error (invalid witness file) 0 --- inspect 5.3   3.3   270   .65 0     
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i timeout 0 wit inspect 960 490   5400 8900 0      0     error (invalid witness file) 0 --- inspect .86 .52 43 0   0   error (invalid witness file) 0 --- inspect 5.5   3.0   270   .65 0   error (invalid witness file) 0 --- inspect 1.0  .64 49 0   0   error (invalid witness file) 0 --- inspect .0048 .0062 .54 0     0      - --- inspect - --- inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i timeout 0 wit inspect 960 500   6900 7100 0      0     error (invalid witness file) 0 --- inspect .67 .41 43 0   0   error (invalid witness file) 0 --- inspect 5.0   2.7   260   .61 0   error (invalid witness file) 0 --- inspect .99 .64 49 0   0   error (invalid witness file) 0 --- inspect .0047 .0057 .53 0     0      - --- inspect - --- inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i timeout 0 wit inspect 900 870   6500 12000 0      0     timeout 0 wit inspect 92    80    1600 0   0   timeout 0 --- inspect 97     73     790   1.6  0   unknown 0 --- inspect 1.1  .68 50 0   0   error (1) 0 --- inspect .10   .10   11    0     .0041 - --- inspect - --- inspect
array-industry-pattern/array_range_init_false-unreach-call.i timeout 0 wit inspect 960 500   6200 7900 0      0     exception 0 --- inspect 7.6  4.3  270 0   0   error (7) 0 --- inspect 15     8.7   550   .71 0   unknown 0 --- inspect 1.2  .75 51 0   0   error (1) 0 --- inspect .11   .10   11    0     0      - --- inspect - --- inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i timeout 0 wit inspect 900 870   6800 11000 0      0     timeout 0 wit inspect 92    80    1500 0   0   timeout 0 --- inspect 97     73     730   1.6  0   unknown 0 --- inspect 1.1  .70 50 0   0   error (1) 0 --- inspect .072  .073  11    0     0      - --- inspect - --- inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i timeout 0 wit inspect 910 870   7900 12000 0      0     timeout 0 wit inspect 93    70    2600 0   0   timeout 0 --- inspect 97     67     3900   1.4  0   unknown 0 --- inspect 1.3  .79 57 0   0   error (1) 0 --- inspect .080  .081  12    0     0      - --- inspect - --- inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i timeout 0 wit inspect 960 490   4800 9100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .48 44 0   0   error (invalid witness file) 0 --- inspect 5.4   3.0   260   .61 0     
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i timeout 0 wit inspect 910 870   7900 11000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4300 0   0   timeout 0 --- inspect 960     950     1400   .66 0     
array-industry-pattern/array_of_struct_break_true-unreach-call.i timeout 0 wit inspect 960 460   6900 8100 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .51 42 0   0   error (invalid witness file) 0 --- inspect 6.5   3.8   270   .65 0     
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 0 wit inspect 910 450   5300 6800 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4900 0   0   error (7) 0 --- inspect 17     8.7   620   .75 0     
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i timeout 0 wit inspect 970 490   7600 8600 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .87 .53 43 0   0   error (invalid witness file) 0 --- inspect 5.4   3.0   260   .65 0     
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 0 wit inspect 930 450   5700 6900 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5000 0   0   error (7) 0 --- inspect 16     9.1   570   .71 0     
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i timeout 0 wit inspect 960 500   6300 10000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .86 .52 43 0   0   error (invalid witness file) 0 --- inspect 5.2   2.9   270   .65 0     
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i timeout 0 wit inspect 900 890   6900 13000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 690    690    7000 0   0   timeout 0 --- inspect 960     940     1500   .64 0     
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 0 wit inspect 900 880   5600 8600 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    3800 0   0   timeout 0 --- inspect 960     940     1300   2.1  0     
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 0 wit inspect 960 470   5700 7000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .50 42 0   0   error (invalid witness file) 0 --- inspect 5.3   2.8   260   .61 0     
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i timeout 0 wit inspect 960 480   6000 9500 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .41 42 0   0   error (invalid witness file) 0 --- inspect 5.1   3.2   270   .65 0     
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16 5.5 1200 120 0      0     false(unreach-call) 1 wit inspect 6.7  4.1  350 0   0   false(unreach-call) 1 --- inspect 18     9.9   500   .66 0   unknown 0 --- inspect 4.5  2.6  260 0   0   false(unreach-call) 1 --- inspect .64   .64   21    .066 0      - --- inspect - --- inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16 5.6 1300 110 0      0     false(unreach-call) 1 wit inspect 8.2  5.1  380 0   0   timeout 0 --- inspect 98     61     6900   1.4  0   unknown 0 --- inspect 5.1  2.8  270 0   0   false(unreach-call) 1 --- inspect .67   .67   22    .066 0      - --- inspect - --- inspect
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 18 6.7 1300 120 0      0     false(unreach-call) 1 wit inspect 12    7.7  460 0   0   out of memory 0 --- inspect 71     46     7000   1.7  0   unknown 0 --- inspect 6.3  3.4  320 0   0   false(unreach-call) 1 --- inspect .72   .72   24    .066 0      - --- inspect - --- inspect
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 29 17   1500 230 0      0     false(unreach-call) 1 wit inspect 23    18    660 0   0   out of memory 0 --- inspect 84     53     7000   1.9  0   unknown 0 --- inspect 8.6  4.6  380 0   0   false(unreach-call) 1 --- inspect .85   .84   28    .074 0      - --- inspect - --- inspect
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect 68 54   1800 670 0      0     false(unreach-call) 1 wit inspect 23    17    960 0   0   out of memory 0 --- inspect 79     51     7000   .73 0   unknown 0 --- inspect 7.5  4.1  390 0   0   false(unreach-call) 1 --- inspect .95   .95   31    .078 0      - --- inspect - --- inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 40 26   1400 400 0      0     false(unreach-call) 1 wit inspect 6.0  3.6  350 0   0   false(unreach-call) 1 --- inspect 15     9.1   490   .62 0   unknown 0 --- inspect 4.4  2.5  260 0   0   false(unreach-call) 1 --- inspect .64   .64   21    .066 0      - --- inspect - --- inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i timeout 0 wit inspect 900 880   3600 7600 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 610    610    2200 0   0   timeout 0 --- inspect 960     930     5300   .65 0     
reducercommutativity/avg10_true-unreach-call_true-termination.i timeout 0 wit inspect 900 880   3600 8300 .057  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2200 0   0   timeout 0 --- inspect 960     920     1800   1.6  0     
reducercommutativity/avg20_true-unreach-call.i timeout 0 wit inspect 900 870   4300 8000 .098  .070 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2800 0   0   timeout 0 --- inspect 960     840     1800   .66 0     
reducercommutativity/avg40_true-unreach-call.i timeout 0 wit inspect 900 870   6000 7600 .19   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4000 0   0   timeout 0 --- inspect 960     850     990   .71 0     
reducercommutativity/avg60_true-unreach-call.i timeout 0 wit inspect 900 870   5400 9700 .28   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3200 0   0   timeout 0 --- inspect 960     920     870   1.5  0     
reducercommutativity/avg_true-unreach-call_true-termination.i timeout 0 wit inspect 930 460   4100 9200 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 920    890    4200 0   0   error (7) 0 --- inspect 15     8.1   300   .75 0     
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 240 220   2300 1900 .041  0     - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 100    98    980 0   0   timeout 0 --- inspect 960     920     2100   1.6  0     
reducercommutativity/max10_true-unreach-call_true-termination.i timeout 0 wit inspect 900 880   2900 7200 .070  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2100 0   0   timeout 0 --- inspect 960     840     3100   .65 0     
reducercommutativity/max20_true-unreach-call.i timeout 0 wit inspect 900 880   2900 6500 .13   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1900 0   0   timeout 0 --- inspect 960     820     1200   .64 0     
reducercommutativity/max40_true-unreach-call.i timeout 0 wit inspect 900 870   2900 11000 .25   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1400 0   0   timeout 0 --- inspect 960     850     980   .75 0     
reducercommutativity/max60_true-unreach-call.i timeout 0 wit inspect 900 860   3400 7900 .36   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1700 0   0   timeout 0 --- inspect 960     930     690   .63 0     
reducercommutativity/max_true-unreach-call_true-termination.i timeout 0 wit inspect 960 480   4600 6800 .016  0     - --- inspect