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 - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .50 42 0   0   error (invalid witness file) 0 --- inspect 5.4   3.0   260   .65 0     
reducercommutativity/sep05_true-unreach-call_true-termination.i true 2 wit inspect 16 6.3 1100 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 600    590    1500 0   0   timeout 0 --- inspect 960     910     3900   .73 0     
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect 31 22   1400 350 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1600 0   0   timeout 0 --- inspect 960     820     6600   .71 0     
reducercommutativity/sep20_true-unreach-call.i true 2 wit inspect 240 230   1900 1800 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1300 0   0   timeout 0 --- inspect 960     830     6300   1.7  0     
reducercommutativity/sep40_true-unreach-call.i timeout 0 wit inspect 900 890   2800 8200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1300 0   0   timeout 0 --- inspect 960     910     1400   1.6  0     
reducercommutativity/sep60_true-unreach-call.i timeout 0 wit inspect 900 890   3600 6600 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1300 0   0   timeout 0 --- inspect 960     920     910   .68 0     
reducercommutativity/sep_true-unreach-call_true-termination.i timeout 0 wit inspect 910 890   3200 8800 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3100 0   0   timeout 0 --- inspect 960     900     1800   .64 0     
reducercommutativity/sum05_true-unreach-call_true-termination.i timeout 0 wit inspect 900 880   2200 10000 .033  .090 - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 200    190    1300 0   0   true 2 --- inspect 570     540     1300   .62 0     
reducercommutativity/sum10_true-unreach-call_true-termination.i timeout 0 wit inspect 900 880   4300 6400 .057  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2700 0   0   timeout 0 --- inspect 960     900     1600   .64 0     
reducercommutativity/sum20_true-unreach-call.i timeout 0 wit inspect 900 880   4200 6600 .098  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2800 0   0   timeout 0 --- inspect 960     850     1600   .66 0     
reducercommutativity/sum40_true-unreach-call.i timeout 0 wit inspect 900 870   6800 7500 .19   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4400 0   0   timeout 0 --- inspect 960     860     890   .63 0     
reducercommutativity/sum60_true-unreach-call.i timeout 0 wit inspect 910 870   5300 6700 .28   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3400 0   0   timeout 0 --- inspect 960     930     700   .65 0     
reducercommutativity/sum_true-unreach-call_true-termination.i timeout 0 wit inspect 970 480   4500 9100 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .84 .51 42 0   0   error (invalid witness file) 0 --- inspect 6.7   3.9   260   .65 0     
array-tiling/mlceu_false-unreach-call.i timeout 0 wit inspect 960 480   5900 7000 .0082 0     error (invalid witness file) 0 --- inspect .79 .48 44 0   0   error (invalid witness file) 0 --- inspect 5.4   3.4   260   .65 0   error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0   error (invalid witness file) 0 --- inspect .0018 .0024 .53 0     0      - --- inspect - --- inspect
array-tiling/skippedu_false-unreach-call.i false(unreach-call) 1 wit inspect 16 4.3 1200 110 .025  0     false(unreach-call) 1 wit inspect 4.8  2.7  260 0   0   false(unreach-call) 1 --- inspect 11     6.5   380   .66 0   unknown 0 --- inspect 3.7  2.2  250 0   0   true -32 --- inspect .59   .59   20    .053 0      - --- inspect - --- inspect
array-tiling/mbpr2_true-unreach-call.i timeout 0 wit inspect 960 470   5100 7500 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .84 .51 43 0   0   error (invalid witness file) 0 --- inspect 7.0   3.7   260   .65 0     
array-tiling/mbpr3_true-unreach-call.i timeout 0 wit inspect 970 430   7100 9000 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .84 .52 42 0   0   error (invalid witness file) 0 --- inspect 5.6   3.0   270   .65 0     
array-tiling/mbpr4_true-unreach-call.i timeout (exception) 0 --- inspect 910 400   7200 9800 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0     
array-tiling/mbpr5_true-unreach-call.i timeout 0 wit inspect 930 380   7500 8700 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    900    2100 0   0   error (7) 0 --- inspect 14     8.7   300   .75 0     
array-tiling/nr2_true-unreach-call.i timeout 0 wit inspect 960 460   4400 9700 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 45 0   0   error (invalid witness file) 0 --- inspect 5.6   3.0   270   .65 0     
array-tiling/nr3_true-unreach-call.i timeout 0 wit inspect 970 460   6500 8800 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 42 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   260   .65 0     
array-tiling/nr4_true-unreach-call.i timeout 0 wit inspect 960 460   5200 8200 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .46 43 0   0   error (invalid witness file) 0 --- inspect 5.4   2.9   260   .65 0     
array-tiling/nr5_true-unreach-call.i timeout 0 wit inspect 960 460   5100 8100 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 43 0   0   error (invalid witness file) 0 --- inspect 5.7   3.4   260   .65 0     
array-tiling/pnr2_true-unreach-call.i timeout 0 wit inspect 970 480   3300 8300 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 42 0   0   error (invalid witness file) 0 --- inspect 5.4   2.8   270   .65 0     
array-tiling/pnr3_true-unreach-call.i timeout 0 --- inspect 960 420   6500 7600 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 41 0   0   error (2) 0 --- inspect .026 .028 5.6 0    0     
array-tiling/pnr4_true-unreach-call.i timeout 0 wit inspect 970 480   3100 8200 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .49 43 0   0   error (invalid witness file) 0 --- inspect 6.1   3.7   270   .65 0     
array-tiling/pnr5_true-unreach-call.i timeout 0 --- inspect 960 420   6100 8900 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .41 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0     
array-tiling/poly1_true-unreach-call.i timeout 0 wit inspect 900 890   1700 11000 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5300 0   0   timeout 0 --- inspect 960     940     800   .72 0     
array-tiling/poly2_true-unreach-call.i timeout 0 wit inspect 950 460   5400 7300 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect exception 0 --- inspect 11    6.2  450 0   0   error (7) 0 --- inspect 12     6.4   290   .75 0     
array-tiling/pr2_true-unreach-call.i timeout 0 wit inspect 960 460   4000 6800 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 43 0   0   error (invalid witness file) 0 --- inspect 5.1   3.2   250   .61 0     
array-tiling/pr3_true-unreach-call.i timeout 0 wit inspect 960 470   4100 7000 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 43 0   0   error (invalid witness file) 0 --- inspect 5.4   3.0   260   .65 0     
array-tiling/pr4_true-unreach-call.i timeout 0 wit inspect 960 470   3800 7800 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 920    890    2400 0   0   error (7) 0 --- inspect 17     9.8   300   .75 0     
array-tiling/pr5_true-unreach-call.i timeout 0 wit inspect 960 480   3500 8500 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 43 0   0   error (invalid witness file) 0 --- inspect 5.4   3.4   260   .65 0     
array-tiling/revcpyswp2_true-unreach-call.i timeout 0 wit inspect 960 480   3400 8100 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .50 43 0   0   error (invalid witness file) 0 --- inspect 5.6   3.0   270   .61 0     
array-tiling/rew_true-unreach-call.i timeout 0 wit inspect 970 480   4100 7400 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .49 43 0   0   error (invalid witness file) 0 --- inspect 5.2   2.8   260   .65 0     
array-tiling/rewnif_true-unreach-call.i timeout 0 wit inspect 960 480   5300 6900 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 42 0   0   error (invalid witness file) 0 --- inspect 5.2   2.8   260   .65 0     
array-tiling/rewnifrev2_true-unreach-call.i timeout 0 --- inspect 970 480   3400 8700 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0     
array-tiling/rewnifrev_true-unreach-call.i timeout 0 wit inspect 960 480   4100 7700 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 43 0   0   error (invalid witness file) 0 --- inspect 6.1   3.3   280   .61 0     
array-tiling/rewrev_true-unreach-call.i timeout 0 --- inspect 960 490   5000 7700 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0     
array-tiling/skipped_true-unreach-call.i timeout 0 wit inspect 970 470   4300 9400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 44 0   0   error (invalid witness file) 0 --- inspect 5.4   2.9   270   .65 0     
array-tiling/tcpy_true-unreach-call.i timeout 0 wit inspect 960 470   3000 7700 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 43 0   0   error (invalid witness file) 0 --- inspect 6.1   3.5   260   .65 0     
array-programs/copysome1_false-unreach-call.i timeout 0 wit inspect 970 500   6200 9600 0      0     error (invalid witness file) 0 --- inspect .72 .45 43 0   0   error (invalid witness file) 0 --- inspect 5.6   3.0   260   .65 0   error (invalid witness file) 0 --- inspect .96 .62 50 0   0   error (invalid witness file) 0 --- inspect .0025 .0032 .40 0     0      - --- inspect - --- inspect
array-programs/copysome2_false-unreach-call.i timeout 0 wit inspect 900 870   9100 11000 0      0     timeout 0 wit inspect 92    75    2100 0   0   timeout 0 --- inspect 97     76     2800   .76 0   unknown 0 --- inspect 1.6  .97 57 0   0   error (1) 0 --- inspect .072  .073  11    0     .0041 - --- inspect - --- inspect
array-programs/copysome1_true-unreach-call.i timeout 0 wit inspect 970 500   6500 8300 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 43 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   270   .65 0     
array-programs/copysome2_true-unreach-call.i timeout 0 wit inspect 900 880   8200 12000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    870    5300 0   0   timeout 0 --- inspect 960     920     5000   .26 0     
array-crafted/bAnd1_true-unreach-call.i timeout 0 wit inspect 900 870   5100 8000 .45   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4400 0   0   timeout 0 --- inspect 960     930     670   .66 0     
array-crafted/bAnd2_true-unreach-call.i timeout 0 wit inspect 910 770   6500 8200 6.1    0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    880    5600 0   0   error (7) 0 --- inspect 13     7.1   290   .71 0     
array-crafted/bAnd3_true-unreach-call.i timeout 0 wit inspect 970 490   6600 8500 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 42 0   0   error (invalid witness file) 0 --- inspect 6.0   3.6   260   .65 0     
array-crafted/bAnd4_true-unreach-call.i timeout 0 wit inspect 960 490   4700 8400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .50 42 0   0   error (invalid witness file) 0 --- inspect 5.4   2.9   270   .65 0     
array-crafted/bAnd5_true-unreach-call.i timeout 0 wit inspect 970 480   4600 8100 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 43 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   270   .65 0     
array-crafted/bor1_true-unreach-call.i timeout 0 wit inspect 900 860   5900 7600 .45   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4100 0   0   timeout 0 --- inspect 960     920     700   .63 0     
array-crafted/bor2_true-unreach-call.i timeout 0 wit inspect 910 780   6300 8500 6.0    0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5200 0   0   error (7) 0 --- inspect 12     6.7   290   .71 0     
array-crafted/bor3_true-unreach-call.i timeout 0 wit inspect 960 490   6200 8300 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 42 0   0   error (invalid witness file) 0 --- inspect 5.1   3.3   260   .65 0     
array-crafted/bor4_true-unreach-call.i timeout 0 wit inspect 960 490   7300 8700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .45 42 0   0   error (invalid witness file) 0 --- inspect 5.7   3.4   260   .65 0     
array-crafted/bor5_true-unreach-call.i timeout 0 wit inspect 960 480   5400 7500 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 42 0   0   error (invalid witness file) 0 --- inspect 6.8   3.9   260   .65 0     
array-crafted/mapavg1_true-unreach-call.i timeout 0 wit inspect 900 870   5500 8300 .46   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4200 0   0   timeout 0 --- inspect 960     930     730   .66 0     
array-crafted/mapavg2_true-unreach-call.i timeout 0 wit inspect 920 780   6500 7800 6.1    0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    880    6000 0   0   error (7) 0 --- inspect 13     7.4   300   .75 0     
array-crafted/mapavg3_true-unreach-call.i timeout 0 wit inspect 960 500   6200 8600 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .42 45 0   0   error (invalid witness file) 0 --- inspect 5.6   3.1   260   .65 0     
array-crafted/mapavg4_true-unreach-call.i timeout 0 wit inspect 970 500   5900 9800 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0   error (invalid witness file) 0 --- inspect 5.1   3.2   270   .65 0     
array-crafted/mapavg5_true-unreach-call.i timeout 0 wit inspect 900 890   2800 7100 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect exception 0 --- inspect 6.6  4.1  470 0   0   false(unreach-call) -16 --- inspect 23     14     590   .62 0     
array-crafted/mapsum1_true-unreach-call.i timeout 0 wit inspect 910 870   6100 7100 .46   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4100 0   0   timeout 0 --- inspect 960     930     750   .66 0     
array-crafted/mapsum2_true-unreach-call.i timeout 0 wit inspect 920 710   6600 9300 6.1    0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    880    5800 0   0   error (7) 0 --- inspect 15     8.4   290   .75 0     
array-crafted/mapsum3_true-unreach-call.i timeout 0 wit inspect 970 490   6000 8600 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   3.0   260   .65 .0041
array-crafted/mapsum4_true-unreach-call.i timeout 0 wit inspect 970 490   6900 8200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 42 0   0   error (invalid witness file) 0 --- inspect 6.3   3.7   260   .65 0     
array-crafted/mapsum5_true-unreach-call.i timeout 0 wit inspect 900 890   2300 9800 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3200 0   0   false(unreach-call) -16 --- inspect 320     300     760   .62 0     
array-crafted/xor1_true-unreach-call.i timeout 0 wit inspect 900 870   6600 8600 .45   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4500 0   0   timeout 0 --- inspect 960     930     670   .64 0     
array-crafted/xor2_true-unreach-call.i timeout 0 wit inspect 910 710   6500 9000 6.0    0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6000 0   0   error (7) 0 --- inspect 14     8.0   280   .75 0     
array-crafted/xor3_true-unreach-call.i timeout 0 wit inspect 960 490   5100 8800 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 43 0   0   error (invalid witness file) 0 --- inspect 5.2   3.3   260   .65 0     
array-crafted/xor4_true-unreach-call.i timeout 0 wit inspect 960 490   6100 8300 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 43 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   270   .65 0     
array-crafted/xor5_true-unreach-call.i timeout 0 wit inspect 960 470   5400 8800 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 42 0   0   error (invalid witness file) 0 --- inspect 5.2   2.8   270   .65 0     
array-crafted/zero_sum1_true-unreach-call.c timeout 0 wit inspect 900 890   1700 5600 .0082 .090 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    650 0   0   timeout 0 --- inspect 960     870     2000   .63 0     
array-crafted/zero_sum2_true-unreach-call.c exception 0 --- inspect 17 7.2 1200 140 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0     
array-crafted/zero_sum3_true-unreach-call.c exception 0 --- inspect 22 11   1300 230 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 42 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0     
array-crafted/zero_sum4_true-unreach-call.c exception 0 --- inspect 22 13   1400 250 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0     
array-crafted/zero_sum5_true-unreach-call.c exception 0 --- inspect 32 22   1400 320 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0   error (2) 0 --- inspect .026 .027 5.7 0    0     
array-crafted/zero_sum_const1_true-unreach-call.c timeout 0 wit inspect 900 890   1600 12000 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4500 0   0   out of memory 0 --- inspect 370     280     7000   .66 0     
array-crafted/zero_sum_const2_true-unreach-call.c exception 0 --- inspect 20 9.5 1200 190 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0     
array-crafted/zero_sum_const3_true-unreach-call.c exception 0 --- inspect 20 10   1200 160 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 42 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0     
array-crafted/zero_sum_const4_true-unreach-call.c exception 0 --- inspect 23 13   1300 220 .016  .090 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0     
array-crafted/zero_sum_const5_true-unreach-call.c exception 0 --- inspect 24 15   1200 240 0      .061 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .45 40 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0     
array-crafted/zero_sum_const_m2_true-unreach-call.c timeout 0 wit inspect 900 890   1900 10000 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    860    6000 0   0   out of memory 0 --- inspect 460     370     7000   .64 0     
array-crafted/zero_sum_const_m3_true-unreach-call.c exception 0 --- inspect 40 29   1600 400 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0     
array-crafted/zero_sum_const_m4_true-unreach-call.c exception 0 --- inspect 310 290   2300 3600 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     
array-crafted/zero_sum_const_m5_true-unreach-call.c timeout 0 --- inspect 910 900   2000 10000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     
array-crafted/zero_sum_m2_true-unreach-call.c timeout 0 wit inspect 900 880   2900 8200 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    750 0   0   timeout 0 --- inspect 960     880     1200   .66 0     
array-crafted/zero_sum_m3_true-unreach-call.c timeout 0 --- inspect 910 900   2000 9400 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0     
array-crafted/zero_sum_m4_true-unreach-call.c timeout 0 --- inspect 910 900   2700 9500 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .42 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0     
array-crafted/zero_sum_m5_true-unreach-call.c timeout 0 --- inspect 910 900   14000 9300 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0     
array-multidimensional/add-2-n-u_true-unreach-call.i timeout 0 wit inspect 900 850   7300 11000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 460    430    7000 0   0   timeout 0 --- inspect 960     950     1600   .64 0     
array-multidimensional/add-3-n-u_true-unreach-call.i timeout 0 wit inspect 960 420   7500 10000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 910    900    2200 0   0   error (7) 0 --- inspect 12     6.8   290   .71 0     
array-multidimensional/copy-2-u_true-unreach-call.i timeout 0 wit inspect 910 830   8200 12000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    860    6900 0   0   timeout 0 --- inspect 960     940     2900   .81 0     
array-multidimensional/copy-3-n-u_true-unreach-call.i timeout 0 wit inspect 960 420   7000 9300 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .37 42 0   0   error (invalid witness file) 0 --- inspect 6.3   3.6   260   .65 0     
array-multidimensional/copy-partial-2-n-u_true-unreach-call.i timeout 0 wit inspect 910 870   6300 11000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 710    660    7000 0   0   timeout 0 --- inspect 960     940     3200   .71 0     
array-multidimensional/copy-partial-3-u_true-unreach-call.i true 2 wit inspect 130 85   2800 1200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    9.6  490 0   0   timeout 0 --- inspect 960     920     1200   .64 0     
array-multidimensional/diff-2-n-u_true-unreach-call.i timeout 0 wit inspect 960 410   8100 9500 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 42 0   0   error (invalid witness file) 0 --- inspect 5.8   3.4   250   .65 0     
array-multidimensional/diff-3-n-u_true-unreach-call.i timeout 0 wit inspect 960 420   7700 8700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 44 0   0   error (invalid witness file) 0 --- inspect 5.7   3.1   270   .65 0     
array-multidimensional/init-2-n-u_true-unreach-call.i timeout 0 wit inspect 960 460   7500 8700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 42 0   0   error (invalid witness file) 0 --- inspect 5.6   3.0   260   .61 0     
array-multidimensional/init-3-u_true-unreach-call.i timeout 0 wit inspect 960 450   8500 8100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .48 42 0   0   error (invalid witness file) 0 --- inspect 6.0   3.2   270   .65 0     
array-multidimensional/init-4-n-u_true-unreach-call.i timeout 0 wit inspect 900 870   6100 11000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 590    560    7000 0   0   timeout 0 --- inspect 960     940     850   .66 0     
array-multidimensional/init-non-constant-2-n-u_true-unreach-call.i timeout 0 wit inspect 960 480   4800 6500 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 42 0   0   error (invalid witness file) 0 --- inspect 5.2   2.8   270   .65 0     
array-multidimensional/init-non-constant-3-u_true-unreach-call.i timeout 0 wit inspect 960 460   8700 9000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 42 0   0   error (invalid witness file) 0 --- inspect 5.8   3.1   260   .65 0     
array-multidimensional/max-2-u_true-unreach-call.i timeout 0 wit inspect 970 460   5300 9700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 43 0   0   error (invalid witness file) 0 --- inspect 5.4   2.9   270   .65 0     
array-multidimensional/max-3-n-u_true-unreach-call.i timeout 0 wit inspect 960 450   6300 8300 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 43 0   0   error (invalid witness file) 0 --- inspect 6.1   3.3   270   .65 0     
array-multidimensional/min-2-u_true-unreach-call.i timeout 0 wit inspect 900 870   6200 11000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4700 0   0   timeout 0 --- inspect 960     920     3000   .69 0     
array-multidimensional/min-3-n-u_true-unreach-call.i timeout 0 wit inspect 960 440   6500 8700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 44 0   0   error (invalid witness file) 0 --- inspect 6.0   3.5   260   .65 0     
array-multidimensional/rev-2-n-u_true-unreach-call.i timeout 0 wit inspect 960 440   8500 8700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 43 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   270   .65 0     
array-multidimensional/rev-3-u_true-unreach-call.i timeout 0 wit inspect 960 440   6800 9200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .84 .50 43 0   0   error (invalid witness file) 0 --- inspect 5.2   2.8   270   .65 0     
array-multidimensional/transpose-u_true-unreach-call.i timeout 0 wit inspect 960 450   8600 8100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 42 0   0   error (invalid witness file) 0 --- inspect 5.4   2.9   270   .61 0     
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)
total 231 25 190000 120000 1200000 1800000 99     .40 44 7 670 530 17000 0   0   44 3 1100 770 49000 35   0   44 0 79 47 4000 0   0   44 -26 5.8  5.8  260 .47  .0082 187 8 52000 50000 240000 0   0   187 -40 45000 42000 150000 110   .0041
    correct results 16 25 910 700 24000 7600 .066 0    7 7 84 58 3400 0   0   3 3 45 26 1400 1.9 0   0 6 6 4.5  4.5  150 .41  0      4 8 630 600 2800 0   0   4 8 610 560 2500 2.6 0     
        correct true 9 18 710 580 14000 5800 .041 0    0 0 0 0 4 8 630 600 2800 0   0   4 8 610 560 2500 2.6 0     
        correct false 7 7 200 120 9700 1800 .025 0    7 7 84 58 3400 0   0   3 3 45 26 1400 1.9 0   0 6 6 4.5  4.5  150 .41  0      0 0
    incorrect results 0 0 0 0 1 -32 .59 .59 20 .053 0      0 3 -48 380 340 1900 1.9 0     
        incorrect true 0 0 0 0 1 -32 .59 .59 20 .053 0      0 0
        incorrect false 0 0 0 0 0 0 3 -48 380 340 1900 1.9 0     
score (231 tasks, max score: 418) 25 7 3 0 -26 8 -40
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