Tool VerifierIntegerAssignmentPrograms 1.1.12(Date 28/11/2018) 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*
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-09 18:49:43 CET 2018-12-09 21:23:04 CET 2018-12-09 22:02:00 CET 2018-12-09 22:04:11 CET 2018-12-12 22:08:25 CET 2018-12-09 21:05:40 CET 2018-12-09 21:25:32 CET
Run set viap.sv-comp19_prop-reachsafety.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Arrays uautomizer-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Arrays
Options -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/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/viap.2018-12-09_1849.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/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/viap.2018-12-09_1849.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 42   42   130 550 .76 0      error (invalid witness file) 0 --- inspect .64 .42 41 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0      error (invalid witness file) 0 --- inspect .92 .59 47 0   0      error (invalid witness file) 0 --- inspect .0052 .0067 .54 0     0      - --- inspect - --- inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unknown 0 --- inspect 330   330   470 3700 .65 0      error (invalid witness file) 0 --- inspect .59 .39 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .94 .61 47 0   0      error (invalid witness file) 0 --- inspect .0052 .0063 .53 0     0      - --- inspect - --- inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i unknown 0 --- inspect 330   330   450 3400 .65 1.4    error (invalid witness file) 0 --- inspect .60 .38 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .96 .61 47 0   0      error (invalid witness file) 0 --- inspect .0068 .0086 .41 0     0      - --- inspect - --- inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unknown 0 --- inspect 580   580   390 6500 .82 0      error (invalid witness file) 0 --- inspect .58 .35 40 0   0      error (2) 0 --- inspect .020 .022 5.7 0    0      error (invalid witness file) 0 --- inspect .94 .61 47 0   0      error (invalid witness file) 0 --- inspect .0023 .0029 .53 0     0      - --- inspect - --- inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i unknown 0 --- inspect 890   890   440 11000 1.2  0      error (invalid witness file) 0 --- inspect .58 .36 41 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0      error (invalid witness file) 0 --- inspect .98 .62 48 0   0      error (invalid witness file) 0 --- inspect .0054 .0085 .52 0     0      - --- inspect - --- inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i unknown 0 --- inspect 420   420   400 4700 .61 2.5    error (invalid witness file) 0 --- inspect .62 .40 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .95 .63 48 0   0      error (invalid witness file) 0 --- inspect .0061 .0076 .53 0     0      - --- inspect - --- inspect
array-examples/standard_copy1_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 7.4 7.4 130 100 1.4  .63   exception 0 --- inspect 3.2  1.7  210 0   0      true -32 --- inspect 8.9   4.8   520   .62 0      exception 0 --- inspect 3.7  2.0  210 0   0      false(unreach-call) 1 --- inspect .60   .60   23    .049 0      - --- inspect - --- inspect
array-examples/standard_copy2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 8.6 8.6 130 120 1.6  .63   exception 0 --- inspect 3.1  1.7  200 0   0      true -32 --- inspect 11     5.8   530   .66 0      exception 0 --- inspect 3.8  2.1  210 0   0      false(unreach-call) 1 --- inspect .62   .62   25    .049 0      - --- inspect - --- inspect
array-examples/standard_copy3_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 9.7 9.7 130 140 1.9  1.0    exception 0 --- inspect 3.2  1.7  210 0   0      true -32 --- inspect 12     6.1   530   .66 .0041 exception 0 --- inspect 3.8  2.2  210 0   0      false(unreach-call) 1 --- inspect .65   .65   27    .049 .0041 - --- inspect - --- inspect
array-examples/standard_copy4_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 11   11   130 160 2.1  .62   exception 0 --- inspect 3.2  1.7  200 0   0      true -32 --- inspect 13     6.8   690   .66 0      exception 0 --- inspect 3.7  2.1  210 0   0      false(unreach-call) 1 --- inspect .68   .67   28    .049 0      - --- inspect - --- inspect
array-examples/standard_copy5_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 12   12   140 160 2.3  0      exception 0 --- inspect 3.4  1.8  200 0   0      true -32 --- inspect 12     6.7   720   .66 0      exception 0 --- inspect 3.9  2.1  210 0   0      false(unreach-call) 1 --- inspect .68   .68   30    .049 0      - --- inspect - --- inspect
array-examples/standard_copy6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 13   13   150 210 2.5  0      exception 0 --- inspect 3.4  1.9  200 0   0      true -32 --- inspect 13     7.0   640   .66 0      exception 0 --- inspect 4.1  2.3  210 0   0      false(unreach-call) 1 --- inspect .70   .70   31    .049 0      - --- inspect - --- inspect
array-examples/standard_copy7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 14   14   160 210 2.8  .62   exception 0 --- inspect 3.6  1.9  200 0   0      true -32 --- inspect 14     7.4   750   .66 0      exception 0 --- inspect 4.1  2.3  210 0   0      false(unreach-call) 1 --- inspect .72   .71   33    .053 0      - --- inspect - --- inspect
array-examples/standard_copy8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 15   15   170 200 3.0  .037  exception 0 --- inspect 3.5  1.9  200 0   0      true -32 --- inspect 15     8.0   810   .66 0      exception 0 --- inspect 4.1  2.3  210 0   0      false(unreach-call) 1 --- inspect .74   .74   34    .057 .0041 - --- inspect - --- inspect
array-examples/standard_copy9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 16   16   180 220 3.2  0      exception 0 --- inspect 3.8  2.0  200 0   0      true -32 --- inspect 17     9.2   720   .66 0      exception 0 --- inspect 4.5  2.4  210 0   0      false(unreach-call) 1 --- inspect .76   .76   36    .057 0      - --- inspect - --- inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 8.1 8.1 130 120 1.6  0      true -32 wit inspect 7.6  4.5  450 0   0      true -32 --- inspect 9.4   5.5   450   .62 0      unknown 0 --- inspect 4.8  2.6  250 0   0      false(unreach-call) 1 --- inspect .63   .63   26    .045 0      - --- inspect - --- inspect
array-examples/standard_init1_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.0 6.0 130 81 1.2  0      true -32 wit inspect 6.8  3.8  430 0   0      out of memory 0 --- inspect 76     51     7000   .63 0      false(unreach-call) 1 --- inspect 4.7  2.6  260 0   0      false(unreach-call) 1 --- inspect .60   .59   22    .045 0      - --- inspect - --- inspect
array-examples/standard_init2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.9 7.0 130 88 1.4  0      true -32 wit inspect 7.0  3.9  430 0   .0041 true -32 --- inspect 9.1   5.0   450   .66 0      unknown 0 --- inspect 4.4  2.4  260 0   0      false(unreach-call) 1 --- inspect .63   .63   24    .045 0      - --- inspect - --- inspect
array-examples/standard_init3_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 7.9 7.9 130 99 1.6  0      true -32 wit inspect 7.2  4.0  430 0   0      true -32 --- inspect 11     5.6   510   .66 0      unknown 0 --- inspect 4.7  2.6  260 0   0      false(unreach-call) 1 --- inspect .63   .63   26    .045 0      - --- inspect - --- inspect
array-examples/standard_init4_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 8.8 8.8 130 140 1.9  0      true -32 wit inspect 7.1  4.0  430 0   0      true -32 --- inspect 9.3   5.0   460   .66 0      unknown 0 --- inspect 4.8  2.7  260 0   0      false(unreach-call) 1 --- inspect .68   .69   28    .045 0      - --- inspect - --- inspect
array-examples/standard_init5_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 9.8 9.9 140 130 2.1  .62   true -32 wit inspect 7.0  4.0  430 0   0      true -32 --- inspect 9.8   5.3   450   .62 0      unknown 0 --- inspect 5.0  2.7  260 0   0      false(unreach-call) 1 --- inspect .69   .68   30    .045 0      - --- inspect - --- inspect
array-examples/standard_init6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 11   11   160 130 2.3  .11   true -32 wit inspect 7.3  4.1  430 0   0      true -32 --- inspect 10     5.4   530   .66 0      unknown 0 --- inspect 4.9  2.7  260 0   0      false(unreach-call) 1 --- inspect .68   .68   32    .045 0      - --- inspect - --- inspect
array-examples/standard_init7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 12   12   170 160 2.5  0      true -32 wit inspect 7.5  4.2  430 0   0      true -32 --- inspect 10     5.4   450   .66 0      unknown 0 --- inspect 5.2  2.9  260 0   0      false(unreach-call) 1 --- inspect .72   .72   34    .045 0      - --- inspect - --- inspect
array-examples/standard_init8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 13   13   180 190 2.7  0      true -32 wit inspect 7.7  4.3  440 0   0      true -32 --- inspect 10     5.5   450   .66 0      unknown 0 --- inspect 5.5  3.0  260 0   0      false(unreach-call) 1 --- inspect .77   .77   36    .045 0      - --- inspect - --- inspect
array-examples/standard_init9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 14   14   190 190 3.0  0      true -32 wit inspect 7.6  4.2  440 0   0      true -32 --- inspect 10     5.5   530   .66 0      unknown 0 --- inspect 5.6  3.0  260 0   0      false(unreach-call) 1 --- inspect .77   .78   39    .045 0      - --- inspect - --- inspect
array-examples/standard_minInArray_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.6 6.6 130 100 1.4  .62   timeout 0 wit inspect 98    85    2000 0   0      true -32 --- inspect 7.7   4.4   320   .66 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0      false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
array-examples/standard_partition_false-unreach-call_ground.i unknown 0 --- inspect 290   290   530 3900 .79 0      error (invalid witness file) 0 --- inspect .62 .38 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0      error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0      error (invalid witness file) 0 --- inspect .0056 .0083 .54 0     0      - --- inspect - --- inspect
array-examples/standard_running_false-unreach-call.i unknown 0 --- inspect 280   280   760 3200 .61 .86   error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .93 .60 47 0   0      error (invalid witness file) 0 --- inspect .0030 .0044 .53 0     0      - --- inspect - --- inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unknown 0 --- inspect 75   75   130 1100 1.1  1.1    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .023 .023 5.6 0    0     
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unknown 0 --- inspect 42   42   130 570 .76 1.7    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0      error (2) 0 --- inspect .027 .031 5.7 0    0     
array-examples/relax_true-unreach-call.i unknown 0 --- inspect 41   42   130 580 1.1  .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0      error (2) 0 --- inspect .019 .020 5.6 0    0     
array-examples/sanfoundry_02_true-unreach-call_ground.i true 2 wit inspect 20   20   240 230 .52 1.1    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2600 0   0      timeout 0 --- inspect 960     830     2100   .62 0     
array-examples/sanfoundry_10_true-unreach-call_ground.i true 2 wit inspect 19   21   240 210 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5100 0   0      timeout 0 --- inspect 960     930     1800   .99 0     
array-examples/sanfoundry_24_true-unreach-call_true-termination.i true 2 wit inspect 14   16   130 170 .50 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.5  4.6  500 0   0      true 2 --- inspect 8.9   5.1   310   .62 0     
array-examples/sanfoundry_27_true-unreach-call_ground.i true 2 wit inspect 30   31   240 370 .48 .13   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2700 0   0      timeout 0 --- inspect 960     810     2100   .63 0     
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 --- inspect 21   22   130 270 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 42 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
array-examples/sorting_bubblesort_true-unreach-call_ground.i true 2 wit inspect 12   12   250 130 .49 1.4    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3200 0   0      timeout 0 --- inspect 960     890     1700   1.0  0     
array-examples/sorting_selectionsort_true-unreach-call_ground.i unknown 0 --- inspect 470   470   440 5300 .79 .11   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .050 .051 5.5 0    0     
array-examples/standard_compareModified_true-unreach-call_ground.i true 2 wit inspect 21   21   340 240 .50 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4800 0   0      timeout 0 --- inspect 960     930     840   .62 0     
array-examples/standard_compare_true-unreach-call_ground.i true 2 wit inspect 24   25   240 300 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4700 0   0      timeout 0 --- inspect 960     900     1300   1.3  0     
array-examples/standard_copy1_true-unreach-call_ground.i true 2 wit inspect 40   42   270 540 .49 1.7    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4200 0   0      timeout 0 --- inspect 960     930     830   1.1  0     
array-examples/standard_copy2_true-unreach-call_ground.i true 2 wit inspect 49   50   250 500 .50 1.7    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4000 0   0      timeout 0 --- inspect 960     940     810   .63 0     
array-examples/standard_copy3_true-unreach-call_ground.i true 2 wit inspect 65   66   340 830 .50 1.1    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3600 0   0      timeout 0 --- inspect 960     940     690   .63 0     
array-examples/standard_copy4_true-unreach-call_ground.i true 2 wit inspect 120   120   550 1600 .55 1.8    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3900 0   0      timeout 0 --- inspect 960     940     710   .63 0     
array-examples/standard_copy5_true-unreach-call_ground.i true 2 wit inspect 130   130   430 1400 .57 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4800 0   0      timeout 0 --- inspect 960     940     780   .98 0     
array-examples/standard_copy6_true-unreach-call_ground.i true 2 wit inspect 140   140   480 1300 .59 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4600 0   0      timeout 0 --- inspect 960     940     730   .63 0     
array-examples/standard_copy7_true-unreach-call_ground.i true 2 wit inspect 140   140   490 1600 .60 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4100 0   0      timeout 0 --- inspect 960     940     750   .62 0     
array-examples/standard_copy8_true-unreach-call_ground.i true 2 wit inspect 150   150   420 1900 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4200 0   0      timeout 0 --- inspect 960     940     750   .63 0     
array-examples/standard_copy9_true-unreach-call_ground.i true 2 wit inspect 160   160   430 1900 .69 1.9    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4300 0   0      timeout 0 --- inspect 960     940     700   .63 0     
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true 2 wit inspect 81   81   650 830 .52 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2900 0   0      timeout 0 --- inspect 960     940     680   .62 0     
array-examples/standard_copyInitSum3_true-unreach-call_ground.i true 2 wit inspect 84   84   430 980 .53 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2900 0   0      timeout 0 --- inspect 960     940     880   .97 0     
array-examples/standard_copyInitSum_true-unreach-call_ground.i true 2 wit inspect 38   38   350 430 .50 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3300 0   0      timeout 0 --- inspect 960     940     900   .65 0     
array-examples/standard_copyInit_true-unreach-call_ground.i true 2 wit inspect 40   40   310 480 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4100 0   .0041 timeout 0 --- inspect 960     940     820   .63 0     
array-examples/standard_find_true-unreach-call_ground.i true 2 wit inspect 26   28   270 320 .48 1.7    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4500 0   0      timeout 0 --- inspect 960     890     1200   1.0  0     
array-examples/standard_init1_true-unreach-call_ground.i true 2 wit inspect 23   24   260 300 .48 2.5    - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 870    860    7000 0   0      timeout 0 --- inspect 960     930     680   .63 0     
array-examples/standard_init2_true-unreach-call_ground.i true 2 wit inspect 23   24   260 350 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3900 0   0      timeout 0 --- inspect 960     940     760   .63 0     
array-examples/standard_init3_true-unreach-call_ground.i true 2 wit inspect 24   25   250 330 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5100 0   0      timeout 0 --- inspect 960     940     680   .63 0     
array-examples/standard_init4_true-unreach-call_ground.i true 2 wit inspect 24   25   250 350 .50 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4600 0   0      timeout 0 --- inspect 960     940     660   .64 0     
array-examples/standard_init5_true-unreach-call_ground.i true 2 wit inspect 33   33   330 430 .50 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4800 0   0      timeout 0 --- inspect 960     940     820   .62 0     
array-examples/standard_init6_true-unreach-call_ground.i true 2 wit inspect 26   27   260 360 .51 1.6    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5300 0   0      timeout 0 --- inspect 960     940     890   .62 .0041
array-examples/standard_init7_true-unreach-call_ground.i true 2 wit inspect 27   28   260 370 .51 .13   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5200 0   0      timeout 0 --- inspect 960     940     1300   .97 0     
array-examples/standard_init8_true-unreach-call_ground.i true 2 wit inspect 27   28   250 360 .52 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    4600 0   0      timeout 0 --- inspect 960     940     690   .98 0     
array-examples/standard_init9_true-unreach-call_ground.i true 2 wit inspect 28   29   260 400 .52 2.1    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5300 0   0      timeout 0 --- inspect 960     930     840   .63 0     
array-examples/standard_maxInArray_true-unreach-call_ground.i true 2 wit inspect 30   30   250 340 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2500 0   .0041 timeout 0 --- inspect 960     820     1900   .64 0     
array-examples/standard_minInArray_true-unreach-call_ground.i true 2 wit inspect 28   29   240 370 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3900 0   0      timeout 0 --- inspect 960     810     2000   .63 0     
array-examples/standard_palindrome_true-unreach-call_ground.i true 2 wit inspect 17   19   130 210 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4800 0   0      timeout 0 --- inspect 960     930     850   .64 0     
array-examples/standard_partial_init_true-unreach-call_ground.i true 2 wit inspect 50   50   610 530 .50 .0041 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2700 0   0      timeout 0 --- inspect 960     930     890   .64 0     
array-examples/standard_partition_original_true-unreach-call_ground.i true 2 wit inspect 490   490   530 5700 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4400 0   0      timeout 0 --- inspect 960     930     870   .63 0     
array-examples/standard_partition_true-unreach-call_ground.i true 2 wit inspect 200   200   440 2800 .68 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5600 0   0      timeout 0 --- inspect 960     920     1700   .95 0     
array-examples/standard_password_true-unreach-call_ground.i true 2 wit inspect 24   25   240 340 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    5200 0   0      timeout 0 --- inspect 960     900     1100   .64 0     
array-examples/standard_reverse_true-unreach-call_ground.i true 2 wit inspect 79   80   610 810 .50 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5500 0   0      timeout 0 --- inspect 960     920     890   1.0  0     
array-examples/standard_running_true-unreach-call.i true 2 wit inspect 230   230   1100 2200 .61 2.4    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3000 0   0      timeout 0 --- inspect 960     940     1600   1.0  0     
array-examples/standard_sentinel_true-unreach-call_true-termination.i true 2 wit inspect 14   16   140 180 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1800 0   0      true 2 --- inspect 15     8.9   500   .62 0     
array-examples/standard_seq_init_true-unreach-call_ground.i true 2 wit inspect 22   23   240 270 .48 2.3    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3000 0   0      timeout 0 --- inspect 960     930     780   .76 0     
array-examples/standard_strcmp_true-unreach-call_ground.i true 2 wit inspect 130   130   660 1300 .54 2.4    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4700 0   0      timeout 0 --- inspect 960     900     1200   1.0  0     
array-examples/standard_strcpy_original_true-unreach-call.i true 2 wit inspect 37   38   280 450 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4000 0   0      timeout 0 --- inspect 960     910     820   1.0  0     
array-examples/standard_strcpy_true-unreach-call_ground.i true 2 wit inspect 32   33   240 410 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4800 0   0      timeout 0 --- inspect 960     920     860   1.0  0     
array-examples/standard_two_index_01_true-unreach-call.i true 2 wit inspect 16   17   240 170 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4000 0   0      timeout 0 --- inspect 960     930     690   1.1  .0041
array-examples/standard_two_index_02_true-unreach-call.i true 2 wit inspect 34   34   130 390 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4500 0   0      timeout 0 --- inspect 960     930     790   .63 .0041
array-examples/standard_two_index_03_true-unreach-call.i true 2 wit inspect 61   62   400 780 .51 1.9    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4900 0   0      timeout 0 --- inspect 960     930     820   .63 0     
array-examples/standard_two_index_04_true-unreach-call.i true 2 wit inspect 32   33   130 410 .49 1.9    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5000 0   0      timeout 0 --- inspect 960     930     820   1.1  0     
array-examples/standard_two_index_05_true-unreach-call.i true 2 wit inspect 31   32   130 440 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5200 0   0      timeout 0 --- inspect 960     930     810   1.1  0     
array-examples/standard_two_index_06_true-unreach-call.i true 2 wit inspect 8.5 9.1 130 100 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4900 0   0      timeout 0 --- inspect 960     920     890   .62 0     
array-examples/standard_two_index_07_true-unreach-call.i true 2 wit inspect 83   84   630 960 .51 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4800 0   0      timeout 0 --- inspect 960     920     890   .62 .0041
array-examples/standard_two_index_08_true-unreach-call.i true 2 wit inspect 31   32   130 440 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4800 0   .053  timeout 0 --- inspect 960     920     920   .63 .0041
array-examples/standard_two_index_09_true-unreach-call.i true 2 wit inspect 83   84   700 950 .51 1.7    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5100 0   0      timeout 0 --- inspect 960     920     870   1.0  0     
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i true 2 wit inspect 130   130   340 1700 .50 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 730    710    7000 0   0      timeout 0 --- inspect 960     930     1100   .97 0     
array-examples/standard_vector_difference_true-unreach-call_ground.i true 2 wit inspect 56   57   260 810 .50 2.3    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4200 0   0      timeout 0 --- inspect 960     930     770   .63 0     
array-examples/standard_sentinel_true-unreach-call.i.v+cfa-reducer.c unknown 0 --- inspect 18   20   130 220 .59 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .41 41 0   0      error (2) 0 --- inspect .020 .021 5.7 0    0     
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.6 6.7 130 92 1.4  0      timeout 0 wit inspect 98    88    960 0   0      out of memory 0 --- inspect 59     38     7000   .63 .033  false(unreach-call) 1 --- inspect 4.9  2.7  260 0   0      false(unreach-call) 1 --- inspect .61   .60   22    .045 0      - --- inspect - --- inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unknown 0 --- inspect 60   60   280 690 .54 2.5    error (invalid witness file) 0 --- inspect .63 .40 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .95 .61 46 0   0      error (invalid witness file) 0 --- inspect .0042 .0060 .53 0     0      - --- inspect - --- inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.5 9.6 130 140 2.3  0      timeout 0 wit inspect 98    83    2200 0   0      true -32 --- inspect 7.1   4.5   310   .66 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0      false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
array-industry-pattern/array_range_init_false-unreach-call.i false(unreach-call) 1 wit inspect 6.9 6.9 130 91 1.6  0      timeout 0 wit inspect 97    88    2100 0   0      true -32 --- inspect 11     5.9   620   .62 0      false(unreach-call) 1 --- inspect 3.6  2.1  240 0   0      false(unreach-call) 1 --- inspect .58   .58   20    .045 .0041 - --- inspect - --- inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 9.5 9.5 130 130 2.3  0      timeout 0 wit inspect 96    81    2200 0   0      true -32 --- inspect 7.3   4.2   310   .66 0      true -32 --- inspect 3.6  2.1  250 0   0      true -32 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i out of memory 0 --- inspect 55   41   15000 670 3.4  .96   error (invalid witness file) 0 --- inspect .64 .40 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .93 .60 47 0   0      error (invalid witness file) 0 --- inspect .0036 .0047 .53 0     0      - --- inspect - --- inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i true 2 wit inspect 25   26   130 290 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3500 0   0      timeout 0 --- inspect 960     940     850   .62 0     
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i true 2 wit inspect 62   62   240 680 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3500 0   0      timeout 0 --- inspect 960     950     670   .64 0     
array-industry-pattern/array_of_struct_break_true-unreach-call.i unknown 0 --- inspect 59   59   150 750 .52 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 42 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i error (1) 0 --- inspect 2.4 2.4 130 33 .22 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 41 0   0      error (2) 0 --- inspect .028 .028 5.5 0    0     
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unknown 0 --- inspect 2.4 2.4 130 34 .22 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .042 .043 5.5 0    0     
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i error (1) 0 --- inspect 2.5 2.5 130 31 .22 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .36 40 0   0      error (2) 0 --- inspect .052 .053 5.5 0    0     
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unknown 0 --- inspect 2.4 2.4 130 31 .22 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unknown 0 --- inspect 62   62   200 740 .60 2.1    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i true 2 wit inspect 8.3 8.4 130 120 .49 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    3800 0   0      timeout 0 --- inspect 960     940     1400   1.0  0     
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i error (1) 0 --- inspect 2.5 2.5 130 33 .22 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 42 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i true 2 wit inspect 7.5 7.5 240 86 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6200 0   0      timeout 0 --- inspect 960     840     1100   .63 0     
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.1 5.1 130 77 .32 .62   exception 0 --- inspect 2.7  1.5  200 0   .0041 true -32 --- inspect 7.2   4.4   300   .66 0      exception 0 --- inspect 2.9  1.7  200 0   .0041 false(unreach-call) 1 --- inspect .58   .58   21    .057 0      - --- inspect - --- inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.1 5.1 130 76 .32 0      exception 0 --- inspect 2.9  1.6  210 0   .0041 true -32 --- inspect 8.5   4.6   310   .66 0      exception 0 --- inspect 3.2  1.8  210 0   0      false(unreach-call) 1 --- inspect .62   .64   22    .057 0      - --- inspect - --- inspect
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 5.1 5.1 130 65 .32 0      exception 0 --- inspect 3.0  1.6  200 0   0      true -32 --- inspect 8.6   4.6   360   .66 0      exception 0 --- inspect 3.5  1.9  210 0   0      false(unreach-call) 1 --- inspect .67   .67   23    .057 0      - --- inspect - --- inspect
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 5.2 5.2 130 68 .32 .0041 exception 0 --- inspect 3.2  1.7  200 0   0      true -32 --- inspect 11     5.9   490   .66 0      exception 0 --- inspect 3.5  2.0  210 0   0      false(unreach-call) 1 --- inspect .63   .63   26    .057 0      - --- inspect - --- inspect
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect 5.2 5.3 130 74 .32 .037  exception 0 --- inspect 3.4  1.9  200 0   0      true -32 --- inspect 14     7.4   820   .66 0      exception 0 --- inspect 3.9  2.2  210 0   0      false(unreach-call) 1 --- inspect .65   .65   28    .057 0      - --- inspect - --- inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i unknown 0 --- inspect 190   190   400 2500 1.1  2.2    error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .023 .024 5.7 0    0      error (invalid witness file) 0 --- inspect .93 .59 47 0   0      error (invalid witness file) 0 --- inspect .0052 .0068 .53 0     0      - --- inspect - --- inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i true 2 wit inspect 28   28   240 340 .48 1.1    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    2000 0   0      timeout 0 --- inspect 960     940     990   1.0  0     
reducercommutativity/avg10_true-unreach-call_true-termination.i true 2 wit inspect 21   21   230 250 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3400 0   0      timeout 0 --- inspect 960     930     1300   .63 0     
reducercommutativity/avg20_true-unreach-call.i true 2 wit inspect 16   16   220 220 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3200 0   0      timeout 0 --- inspect 960     920     5000   1.1  0     
reducercommutativity/avg40_true-unreach-call.i true 2 wit inspect 24   24   240 330 .48 1.1    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4000 0   0      timeout 0 --- inspect 960     930     990   .63 0     
reducercommutativity/avg60_true-unreach-call.i true 2 wit inspect 32   32   240 330 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4300 0   0      timeout 0 --- inspect 960     920     870   .63 0     
reducercommutativity/avg_true-unreach-call_true-termination.i true 2 wit inspect 11   11   240 160 .49 .0041 - --- inspect - --- inspect - --- inspect - --- inspect exception 0 --- inspect 11    8.3  560 0   0      timeout 0 --- inspect 960     950     550   .64 0     
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 12   12   230 150 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 510    500    1200 0   0      timeout 0 --- inspect 960     920     2700   1.0  0     
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 19   19   330 210 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1800 0   0      timeout 0 --- inspect 960     840     6300   .64 0     
reducercommutativity/max20_true-unreach-call.i true 2 wit inspect 11   11   230 140 .48 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1800 0   0      timeout 0 --- inspect 960     920     4100   .64 0     
reducercommutativity/max40_true-unreach-call.i true 2 wit inspect 23   24   240 260 .48 2.2    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1200 0   0      timeout 0 --- inspect 960     920     1600   1.0  0     
reducercommutativity/max60_true-unreach-call.i true 2 wit inspect 24   24   240 280 .48 0      - --- inspect - --- inspect