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; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive] cpa-seq-validate-violation-witnesses-viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive] uautomizer-validate-violation-witnesses-viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive] cpa-witness2test-validate-violation-witnesses-viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive] fshell-witness2test-validate-violation-witnesses-viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive] cpa-seq-validate-correctness-witnesses-viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive] uautomizer-validate-correctness-witnesses-viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive]
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 cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score 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 42   42   130 550 .76 0      error (invalid witness file) 0 .64 .42 41 0   0      error (2) 0 .024 .024 5.6 0    0      error (invalid witness file) 0 .92 .59 47 0      0      error (invalid witness file) 0 .0052 .0067 .54 0      0      - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unknown 0 330   330   470 3700 .65 0      error (invalid witness file) 0 .59 .39 40 0   0      error (2) 0 .021 .022 5.6 0    0      error (invalid witness file) 0 .94 .61 47 0      0      error (invalid witness file) 0 .0052 .0063 .53 0      0      - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i unknown 0 330   330   450 3400 .65 1.4    error (invalid witness file) 0 .60 .38 40 0   0      error (2) 0 .020 .021 5.6 0    0      error (invalid witness file) 0 .96 .61 47 0      0      error (invalid witness file) 0 .0068 .0086 .41 0      0      - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unknown 0 580   580   390 6500 .82 0      error (invalid witness file) 0 .58 .35 40 0   0      error (2) 0 .020 .022 5.7 0    0      error (invalid witness file) 0 .94 .61 47 0      0      error (invalid witness file) 0 .0023 .0029 .53 0      0      - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i unknown 0 890   890   440 11000 1.2  0      error (invalid witness file) 0 .58 .36 41 0   0      error (2) 0 .020 .020 5.6 0    0      error (invalid witness file) 0 .98 .62 48 0      0      error (invalid witness file) 0 .0054 .0085 .52 0      0      - -
array-examples/standard_allDiff2_false-unreach-call_ground.i unknown 0 420   420   400 4700 .61 2.5    error (invalid witness file) 0 .62 .40 41 0   0      error (2) 0 .020 .021 5.6 0    0      error (invalid witness file) 0 .95 .63 48 0      0      error (invalid witness file) 0 .0061 .0076 .53 0      0      - -
array-examples/standard_copy1_false-unreach-call_ground.i false(unreach-call) 1 7.4 7.4 130 100 1.4  .63   exception 0 3.2  1.7  210 0   0      true -32 8.9   4.8   520   .62 0      exception 0 3.7  2.0  210 0      0      false(unreach-call) 1 .60   .60   23    .049  0      - -
array-examples/standard_copy2_false-unreach-call_ground.i false(unreach-call) 1 8.6 8.6 130 120 1.6  .63   exception 0 3.1  1.7  200 0   0      true -32 11     5.8   530   .66 0      exception 0 3.8  2.1  210 0      0      false(unreach-call) 1 .62   .62   25    .049  0      - -
array-examples/standard_copy3_false-unreach-call_ground.i false(unreach-call) 1 9.7 9.7 130 140 1.9  1.0    exception 0 3.2  1.7  210 0   0      true -32 12     6.1   530   .66 .0041 exception 0 3.8  2.2  210 0      0      false(unreach-call) 1 .65   .65   27    .049  .0041 - -
array-examples/standard_copy4_false-unreach-call_ground.i false(unreach-call) 1 11   11   130 160 2.1  .62   exception 0 3.2  1.7  200 0   0      true -32 13     6.8   690   .66 0      exception 0 3.7  2.1  210 0      0      false(unreach-call) 1 .68   .67   28    .049  0      - -
array-examples/standard_copy5_false-unreach-call_ground.i false(unreach-call) 1 12   12   140 160 2.3  0      exception 0 3.4  1.8  200 0   0      true -32 12     6.7   720   .66 0      exception 0 3.9  2.1  210 0      0      false(unreach-call) 1 .68   .68   30    .049  0      - -
array-examples/standard_copy6_false-unreach-call_ground.i false(unreach-call) 1 13   13   150 210 2.5  0      exception 0 3.4  1.9  200 0   0      true -32 13     7.0   640   .66 0      exception 0 4.1  2.3  210 0      0      false(unreach-call) 1 .70   .70   31    .049  0      - -
array-examples/standard_copy7_false-unreach-call_ground.i false(unreach-call) 1 14   14   160 210 2.8  .62   exception 0 3.6  1.9  200 0   0      true -32 14     7.4   750   .66 0      exception 0 4.1  2.3  210 0      0      false(unreach-call) 1 .72   .71   33    .053  0      - -
array-examples/standard_copy8_false-unreach-call_ground.i false(unreach-call) 1 15   15   170 200 3.0  .037  exception 0 3.5  1.9  200 0   0      true -32 15     8.0   810   .66 0      exception 0 4.1  2.3  210 0      0      false(unreach-call) 1 .74   .74   34    .057  .0041 - -
array-examples/standard_copy9_false-unreach-call_ground.i false(unreach-call) 1 16   16   180 220 3.2  0      exception 0 3.8  2.0  200 0   0      true -32 17     9.2   720   .66 0      exception 0 4.5  2.4  210 0      0      false(unreach-call) 1 .76   .76   36    .057  0      - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i false(unreach-call) 1 8.1 8.1 130 120 1.6  0      true -32 7.6  4.5  450 0   0      true -32 9.4   5.5   450   .62 0      unknown 0 4.8  2.6  250 0      0      false(unreach-call) 1 .63   .63   26    .045  0      - -
array-examples/standard_init1_false-unreach-call_ground.i false(unreach-call) 1 6.0 6.0 130 81 1.2  0      true -32 6.8  3.8  430 0   0      out of memory 0 76     51     7000   .63 0      false(unreach-call) 1 4.7  2.6  260 0      0      false(unreach-call) 1 .60   .59   22    .045  0      - -
array-examples/standard_init2_false-unreach-call_ground.i false(unreach-call) 1 6.9 7.0 130 88 1.4  0      true -32 7.0  3.9  430 0   .0041 true -32 9.1   5.0   450   .66 0      unknown 0 4.4  2.4  260 0      0      false(unreach-call) 1 .63   .63   24    .045  0      - -
array-examples/standard_init3_false-unreach-call_ground.i false(unreach-call) 1 7.9 7.9 130 99 1.6  0      true -32 7.2  4.0  430 0   0      true -32 11     5.6   510   .66 0      unknown 0 4.7  2.6  260 0      0      false(unreach-call) 1 .63   .63   26    .045  0      - -
array-examples/standard_init4_false-unreach-call_ground.i false(unreach-call) 1 8.8 8.8 130 140 1.9  0      true -32 7.1  4.0  430 0   0      true -32 9.3   5.0   460   .66 0      unknown 0 4.8  2.7  260 0      0      false(unreach-call) 1 .68   .69   28    .045  0      - -
array-examples/standard_init5_false-unreach-call_ground.i false(unreach-call) 1 9.8 9.9 140 130 2.1  .62   true -32 7.0  4.0  430 0   0      true -32 9.8   5.3   450   .62 0      unknown 0 5.0  2.7  260 0      0      false(unreach-call) 1 .69   .68   30    .045  0      - -
array-examples/standard_init6_false-unreach-call_ground.i false(unreach-call) 1 11   11   160 130 2.3  .11   true -32 7.3  4.1  430 0   0      true -32 10     5.4   530   .66 0      unknown 0 4.9  2.7  260 0      0      false(unreach-call) 1 .68   .68   32    .045  0      - -
array-examples/standard_init7_false-unreach-call_ground.i false(unreach-call) 1 12   12   170 160 2.5  0      true -32 7.5  4.2  430 0   0      true -32 10     5.4   450   .66 0      unknown 0 5.2  2.9  260 0      0      false(unreach-call) 1 .72   .72   34    .045  0      - -
array-examples/standard_init8_false-unreach-call_ground.i false(unreach-call) 1 13   13   180 190 2.7  0      true -32 7.7  4.3  440 0   0      true -32 10     5.5   450   .66 0      unknown 0 5.5  3.0  260 0      0      false(unreach-call) 1 .77   .77   36    .045  0      - -
array-examples/standard_init9_false-unreach-call_ground.i false(unreach-call) 1 14   14   190 190 3.0  0      true -32 7.6  4.2  440 0   0      true -32 10     5.5   530   .66 0      unknown 0 5.6  3.0  260 0      0      false(unreach-call) 1 .77   .78   39    .045  0      - -
array-examples/standard_minInArray_false-unreach-call_ground.i false(unreach-call) 1 6.6 6.6 130 100 1.4  .62   timeout 0 98    85    2000 0   0      true -32 7.7   4.4   320   .66 0      false(unreach-call) 1 3.6  2.1  250 0      0      false(unreach-call) 1 .59   .59   20    .045  0      - -
array-examples/standard_partition_false-unreach-call_ground.i unknown 0 290   290   530 3900 .79 0      error (invalid witness file) 0 .62 .38 41 0   0      error (2) 0 .021 .021 5.6 0    0      error (invalid witness file) 0 1.0  .65 48 0      0      error (invalid witness file) 0 .0056 .0083 .54 0      0      - -
array-examples/standard_running_false-unreach-call.i unknown 0 280   280   760 3200 .61 .86   error (invalid witness file) 0 .59 .37 41 0   0      error (2) 0 .021 .022 5.6 0    0      error (invalid witness file) 0 .93 .60 47 0      0      error (invalid witness file) 0 .0030 .0044 .53 0      0      - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unknown 0 75   75   130 1100 1.1  1.1    - - - - error (invalid witness file) 0 .61 .38 41 0   0      error (2) 0 .023 .023 5.6 0    0     
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unknown 0 42   42   130 570 .76 1.7    - - - - error (invalid witness file) 0 .58 .35 40 0   0      error (2) 0 .027 .031 5.7 0    0     
array-examples/relax_true-unreach-call.i unknown 0 41   42   130 580 1.1  .13   - - - - error (invalid witness file) 0 .58 .35 41 0   0      error (2) 0 .019 .020 5.6 0    0     
array-examples/sanfoundry_02_true-unreach-call_ground.i true 2 20   20   240 230 .52 1.1    - - - - timeout 0 900    890    2600 0   0      timeout 0 960     830     2100   .62 0     
array-examples/sanfoundry_10_true-unreach-call_ground.i true 2 19   21   240 210 .49 0      - - - - timeout 0 900    890    5100 0   0      timeout 0 960     930     1800   .99 0     
array-examples/sanfoundry_24_true-unreach-call_true-termination.i true 2 14   16   130 170 .50 0      - - - - true 2 7.5  4.6  500 0   0      true 2 8.9   5.1   310   .62 0     
array-examples/sanfoundry_27_true-unreach-call_ground.i true 2 30   31   240 370 .48 .13   - - - - timeout 0 900    890    2700 0   0      timeout 0 960     810     2100   .63 0     
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 21   22   130 270 .48 0      - - - - error (invalid witness file) 0 .61 .38 42 0   0      error (2) 0 .020 .021 5.6 0    0     
array-examples/sorting_bubblesort_true-unreach-call_ground.i true 2 12   12   250 130 .49 1.4    - - - - timeout 0 900    890    3200 0   0      timeout 0 960     890     1700   1.0  0     
array-examples/sorting_selectionsort_true-unreach-call_ground.i unknown 0 470   470   440 5300 .79 .11   - - - - error (invalid witness file) 0 .59 .36 40 0   0      error (2) 0 .050 .051 5.5 0    0     
array-examples/standard_compareModified_true-unreach-call_ground.i true 2 21   21   340 240 .50 0      - - - - timeout 0 900    890    4800 0   0      timeout 0 960     930     840   .62 0     
array-examples/standard_compare_true-unreach-call_ground.i true 2 24   25   240 300 .48 0      - - - - timeout 0 900    890    4700 0   0      timeout 0 960     900     1300   1.3  0     
array-examples/standard_copy1_true-unreach-call_ground.i true 2 40   42   270 540 .49 1.7    - - - - timeout 0 900    890    4200 0   0      timeout 0 960     930     830   1.1  0     
array-examples/standard_copy2_true-unreach-call_ground.i true 2 49   50   250 500 .50 1.7    - - - - timeout 0 900    890    4000 0   0      timeout 0 960     940     810   .63 0     
array-examples/standard_copy3_true-unreach-call_ground.i true 2 65   66   340 830 .50 1.1    - - - - timeout 0 900    890    3600 0   0      timeout 0 960     940     690   .63 0     
array-examples/standard_copy4_true-unreach-call_ground.i true 2 120   120   550 1600 .55 1.8    - - - - timeout 0 900    890    3900 0   0      timeout 0 960     940     710   .63 0     
array-examples/standard_copy5_true-unreach-call_ground.i true 2 130   130   430 1400 .57 0      - - - - timeout 0 900    890    4800 0   0      timeout 0 960     940     780   .98 0     
array-examples/standard_copy6_true-unreach-call_ground.i true 2 140   140   480 1300 .59 0      - - - - timeout 0 900    890    4600 0   0      timeout 0 960     940     730   .63 0     
array-examples/standard_copy7_true-unreach-call_ground.i true 2 140   140   490 1600 .60 0      - - - - timeout 0 900    890    4100 0   0      timeout 0 960     940     750   .62 0     
array-examples/standard_copy8_true-unreach-call_ground.i true 2 150   150   420 1900 .62 0      - - - - timeout 0 900    890    4200 0   0      timeout 0 960     940     750   .63 0     
array-examples/standard_copy9_true-unreach-call_ground.i true 2 160   160   430 1900 .69 1.9    - - - - timeout 0 900    890    4300 0   0      timeout 0 960     940     700   .63 0     
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true 2 81   81   650 830 .52 0      - - - - timeout 0 900    890    2900 0   0      timeout 0 960     940     680   .62 0     
array-examples/standard_copyInitSum3_true-unreach-call_ground.i true 2 84   84   430 980 .53 0      - - - - timeout 0 900    890    2900 0   0      timeout 0 960     940     880   .97 0     
array-examples/standard_copyInitSum_true-unreach-call_ground.i true 2 38   38   350 430 .50 0      - - - - timeout 0 900    890    3300 0   0      timeout 0 960     940     900   .65 0     
array-examples/standard_copyInit_true-unreach-call_ground.i true 2 40   40   310 480 .49 0      - - - - timeout 0 900    890    4100 0   .0041 timeout 0 960     940     820   .63 0     
array-examples/standard_find_true-unreach-call_ground.i true 2 26   28   270 320 .48 1.7    - - - - timeout 0 900    880    4500 0   0      timeout 0 960     890     1200   1.0  0     
array-examples/standard_init1_true-unreach-call_ground.i true 2 23   24   260 300 .48 2.5    - - - - out of memory 0 870    860    7000 0   0      timeout 0 960     930     680   .63 0     
array-examples/standard_init2_true-unreach-call_ground.i true 2 23   24   260 350 .49 0      - - - - timeout 0 900    890    3900 0   0      timeout 0 960     940     760   .63 0     
array-examples/standard_init3_true-unreach-call_ground.i true 2 24   25   250 330 .49 0      - - - - timeout 0 900    890    5100 0   0      timeout 0 960     940     680   .63 0     
array-examples/standard_init4_true-unreach-call_ground.i true 2 24   25   250 350 .50 0      - - - - timeout 0 900    890    4600 0   0      timeout 0 960     940     660   .64 0     
array-examples/standard_init5_true-unreach-call_ground.i true 2 33   33   330 430 .50 0      - - - - timeout 0 900    890    4800 0   0      timeout 0 960     940     820   .62 0     
array-examples/standard_init6_true-unreach-call_ground.i true 2 26   27   260 360 .51 1.6    - - - - timeout 0 900    890    5300 0   0      timeout 0 960     940     890   .62 .0041
array-examples/standard_init7_true-unreach-call_ground.i true 2 27   28   260 370 .51 .13   - - - - timeout 0 900    890    5200 0   0      timeout 0 960     940     1300   .97 0     
array-examples/standard_init8_true-unreach-call_ground.i true 2 27   28   250 360 .52 0      - - - - timeout 0 910    890    4600 0   0      timeout 0 960     940     690   .98 0     
array-examples/standard_init9_true-unreach-call_ground.i true 2 28   29   260 400 .52 2.1    - - - - timeout 0 900    890    5300 0   0      timeout 0 960     930     840   .63 0     
array-examples/standard_maxInArray_true-unreach-call_ground.i true 2 30   30   250 340 .48 0      - - - - timeout 0 900    890    2500 0   .0041 timeout 0 960     820     1900   .64 0     
array-examples/standard_minInArray_true-unreach-call_ground.i true 2 28   29   240 370 .48 0      - - - - timeout 0 900    890    3900 0   0      timeout 0 960     810     2000   .63 0     
array-examples/standard_palindrome_true-unreach-call_ground.i true 2 17   19   130 210 .48 0      - - - - timeout 0 900    890    4800 0   0      timeout 0 960     930     850   .64 0     
array-examples/standard_partial_init_true-unreach-call_ground.i true 2 50   50   610 530 .50 .0041 - - - - timeout 0 900    890    2700 0   0      timeout 0 960     930     890   .64 0     
array-examples/standard_partition_original_true-unreach-call_ground.i true 2 490   490   530 5700 1.0  0      - - - - timeout 0 900    890    4400 0   0      timeout 0 960     930     870   .63 0     
array-examples/standard_partition_true-unreach-call_ground.i true 2 200   200   440 2800 .68 0      - - - - timeout 0 900    890    5600 0   0      timeout 0 960     920     1700   .95 0     
array-examples/standard_password_true-unreach-call_ground.i true 2 24   25   240 340 .48 0      - - - - timeout 0 900    880    5200 0   0      timeout 0 960     900     1100   .64 0     
array-examples/standard_reverse_true-unreach-call_ground.i true 2 79   80   610 810 .50 0      - - - - timeout 0 900    890    5500 0   0      timeout 0 960     920     890   1.0  0     
array-examples/standard_running_true-unreach-call.i true 2 230   230   1100 2200 .61 2.4    - - - - timeout 0 900    890    3000 0   0      timeout 0 960     940     1600   1.0  0     
array-examples/standard_sentinel_true-unreach-call_true-termination.i true 2 14   16   140 180 .48 0      - - - - timeout 0 900    890    1800 0   0      true 2 15     8.9   500   .62 0     
array-examples/standard_seq_init_true-unreach-call_ground.i true 2 22   23   240 270 .48 2.3    - - - - timeout 0 900    890    3000 0   0      timeout 0 960     930     780   .76 0     
array-examples/standard_strcmp_true-unreach-call_ground.i true 2 130   130   660 1300 .54 2.4    - - - - timeout 0 900    880    4700 0   0      timeout 0 960     900     1200   1.0  0     
array-examples/standard_strcpy_original_true-unreach-call.i true 2 37   38   280 450 .48 0      - - - - timeout 0 900    890    4000 0   0      timeout 0 960     910     820   1.0  0     
array-examples/standard_strcpy_true-unreach-call_ground.i true 2 32   33   240 410 .48 0      - - - - timeout 0 900    890    4800 0   0      timeout 0 960     920     860   1.0  0     
array-examples/standard_two_index_01_true-unreach-call.i true 2 16   17   240 170 .49 0      - - - - timeout 0 900    890    4000 0   0      timeout 0 960     930     690   1.1  .0041
array-examples/standard_two_index_02_true-unreach-call.i true 2 34   34   130 390 .49 0      - - - - timeout 0 900    890    4500 0   0      timeout 0 960     930     790   .63 .0041
array-examples/standard_two_index_03_true-unreach-call.i true 2 61   62   400 780 .51 1.9    - - - - timeout 0 900    890    4900 0   0      timeout 0 960     930     820   .63 0     
array-examples/standard_two_index_04_true-unreach-call.i true 2 32   33   130 410 .49 1.9    - - - - timeout 0 900    890    5000 0   0      timeout 0 960     930     820   1.1  0     
array-examples/standard_two_index_05_true-unreach-call.i true 2 31   32   130 440 .49 0      - - - - timeout 0 900    890    5200 0   0      timeout 0 960     930     810   1.1  0     
array-examples/standard_two_index_06_true-unreach-call.i true 2 8.5 9.1 130 100 .49 0      - - - - timeout 0 900    890    4900 0   0      timeout 0 960     920     890   .62 0     
array-examples/standard_two_index_07_true-unreach-call.i true 2 83   84   630 960 .51 0      - - - - timeout 0 900    890    4800 0   0      timeout 0 960     920     890   .62 .0041
array-examples/standard_two_index_08_true-unreach-call.i true 2 31   32   130 440 .49 0      - - - - timeout 0 900    890    4800 0   .053  timeout 0 960     920     920   .63 .0041
array-examples/standard_two_index_09_true-unreach-call.i true 2 83   84   700 950 .51 1.7    - - - - timeout 0 900    890    5100 0   0      timeout 0 960     920     870   1.0  0     
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i true 2 130   130   340 1700 .50 0      - - - - out of memory 0 730    710    7000 0   0      timeout 0 960     930     1100   .97 0     
array-examples/standard_vector_difference_true-unreach-call_ground.i true 2 56   57   260 810 .50 2.3    - - - - timeout 0 900    890    4200 0   0      timeout 0 960     930     770   .63 0     
array-examples/standard_sentinel_true-unreach-call.i.v+cfa-reducer.c unknown 0 18   20   130 220 .59 0      - - - - error (invalid witness file) 0 .64 .41 41 0   0      error (2) 0 .020 .021 5.7 0    0     
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i false(unreach-call) 1 6.6 6.7 130 92 1.4  0      timeout 0 98    88    960 0   0      out of memory 0 59     38     7000   .63 .033  false(unreach-call) 1 4.9  2.7  260 0      0      false(unreach-call) 1 .61   .60   22    .045  0      - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unknown 0 60   60   280 690 .54 2.5    error (invalid witness file) 0 .63 .40 40 0   0      error (2) 0 .021 .021 5.6 0    0      error (invalid witness file) 0 .95 .61 46 0      0      error (invalid witness file) 0 .0042 .0060 .53 0      0      - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i false(unreach-call) 1 9.5 9.6 130 140 2.3  0      timeout 0 98    83    2200 0   0      true -32 7.1   4.5   310   .66 0      false(unreach-call) 1 3.6  2.1  250 0      0      false(unreach-call) 1 .59   .59   20    .049  0      - -
array-industry-pattern/array_range_init_false-unreach-call.i false(unreach-call) 1 6.9 6.9 130 91 1.6  0      timeout 0 97    88    2100 0   0      true -32 11     5.9   620   .62 0      false(unreach-call) 1 3.6  2.1  240 0      0      false(unreach-call) 1 .58   .58   20    .045  .0041 - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i false(unreach-call) 0 9.5 9.5 130 130 2.3  0      timeout 0 96    81    2200 0   0      true -32 7.3   4.2   310   .66 0      true -32 3.6  2.1  250 0      0      true -32 .59   .59   20    .049  0      - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i out of memory 0 55   41   15000 670 3.4  .96   error (invalid witness file) 0 .64 .40 41 0   0      error (2) 0 .021 .022 5.6 0    0      error (invalid witness file) 0 .93 .60 47 0      0      error (invalid witness file) 0 .0036 .0047 .53 0      0      - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i true 2 25   26   130 290 .48 0      - - - - timeout 0 900    890    3500 0   0      timeout 0 960     940     850   .62 0     
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i true 2 62   62   240 680 .49 0      - - - - timeout 0 900    890    3500 0   0      timeout 0 960     950     670   .64 0     
array-industry-pattern/array_of_struct_break_true-unreach-call.i unknown 0 59   59   150 750 .52 .0041 - - - - error (invalid witness file) 0 .73 .44 42 0   0      error (2) 0 .027 .028 5.6 0    0     
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i error (1) 0 2.4 2.4 130 33 .22 0      - - - - error (invalid witness file) 0 .64 .38 41 0   0      error (2) 0 .028 .028 5.5 0    0     
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unknown 0 2.4 2.4 130 34 .22 0      - - - - error (invalid witness file) 0 .60 .37 40 0   0      error (2) 0 .042 .043 5.5 0    0     
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i error (1) 0 2.5 2.5 130 31 .22 .0041 - - - - error (invalid witness file) 0 .57 .36 40 0   0      error (2) 0 .052 .053 5.5 0    0     
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unknown 0 2.4 2.4 130 31 .22 0      - - - - error (invalid witness file) 0 .60 .38 41 0   0      error (2) 0 .021 .022 5.6 0    0     
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unknown 0 62   62   200 740 .60 2.1    - - - - error (invalid witness file) 0 .63 .40 41 0   0      error (2) 0 .021 .021 5.6 0    0     
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i true 2 8.3 8.4 130 120 .49 0      - - - - timeout 0 900    900    3800 0   0      timeout 0 960     940     1400   1.0  0     
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i error (1) 0 2.5 2.5 130 33 .22 0      - - - - error (invalid witness file) 0 .62 .39 42 0   0      error (2) 0 .020 .021 5.6 0    0     
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i true 2 7.5 7.5 240 86 .48 0      - - - - timeout 0 910    890    6200 0   0      timeout 0 960     840     1100   .63 0     
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 1 5.1 5.1 130 77 .32 .62   exception 0 2.7  1.5  200 0   .0041 true -32 7.2   4.4   300   .66 0      exception 0 2.9  1.7  200 0      .0041 false(unreach-call) 1 .58   .58   21    .057  0      - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 1 5.1 5.1 130 76 .32 0      exception 0 2.9  1.6  210 0   .0041 true -32 8.5   4.6   310   .66 0      exception 0 3.2  1.8  210 0      0      false(unreach-call) 1 .62   .64   22    .057  0      - -
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 5.1 5.1 130 65 .32 0      exception 0 3.0  1.6  200 0   0      true -32 8.6   4.6   360   .66 0      exception 0 3.5  1.9  210 0      0      false(unreach-call) 1 .67   .67   23    .057  0      - -
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 5.2 5.2 130 68 .32 .0041 exception 0 3.2  1.7  200 0   0      true -32 11     5.9   490   .66 0      exception 0 3.5  2.0  210 0      0      false(unreach-call) 1 .63   .63   26    .057  0      - -
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 5.2 5.3 130 74 .32 .037  exception 0 3.4  1.9  200 0   0      true -32 14     7.4   820   .66 0      exception 0 3.9  2.2  210 0      0      false(unreach-call) 1 .65   .65   28    .057  0      - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i unknown 0 190   190   400 2500 1.1  2.2    error (invalid witness file) 0 .61 .37 41 0   0      error (2) 0 .023 .024 5.7 0    0      error (invalid witness file) 0 .93 .59 47 0      0      error (invalid witness file) 0 .0052 .0068 .53 0      0      - -
reducercommutativity/avg05_true-unreach-call_true-termination.i true 2 28   28   240 340 .48 1.1    - - - - timeout 0 900    900    2000 0   0      timeout 0 960     940     990   1.0  0     
reducercommutativity/avg10_true-unreach-call_true-termination.i true 2 21   21   230 250 .48 0      - - - - timeout 0 900    890    3400 0   0      timeout 0 960     930     1300   .63 0     
reducercommutativity/avg20_true-unreach-call.i true 2 16   16   220 220 .48 0      - - - - timeout 0 900    890    3200 0   0      timeout 0 960     920     5000   1.1  0     
reducercommutativity/avg40_true-unreach-call.i true 2 24   24   240 330 .48 1.1    - - - - timeout 0 900    890    4000 0   0      timeout 0 960     930     990   .63 0     
reducercommutativity/avg60_true-unreach-call.i true 2 32   32   240 330 .48 0      - - - - timeout 0 900    890    4300 0   0      timeout 0 960     920     870   .63 0     
reducercommutativity/avg_true-unreach-call_true-termination.i true 2 11   11   240 160 .49 .0041 - - - - exception 0 11    8.3  560 0   0      timeout 0 960     950     550   .64 0     
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 12   12   230 150 .48 0      - - - - true 2 510    500    1200 0   0      timeout 0 960     920     2700   1.0  0     
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 19   19   330 210 .48 0      - - - - timeout 0 900    890    1800 0   0      timeout 0 960     840     6300   .64 0     
reducercommutativity/max20_true-unreach-call.i true 2 11   11   230 140 .48 0      - - - - timeout 0 900    890    1800 0   0      timeout 0 960     920     4100   .64 0     
reducercommutativity/max40_true-unreach-call.i true 2 23   24   240 260 .48 2.2    - - - - timeout 0 900    890    1200 0   0      timeout 0 960     920     1600   1.0  0     
reducercommutativity/max60_true-unreach-call.i true 2 24   24   240 280 .48 0      - - - - timeout 0 900    890    1500 0   0      timeout 0 960     920     1000   .97 0     
reducercommutativity/max_true-unreach-call_true-termination.i true 2 17   17   310 210 .49 0      - - - - timeout 0 900    890    2800 0   .0041 timeout 0 960     940     4700   .63 0     
reducercommutativity/sep05_true-unreach-call_true-termination.i true 2 14   14   230 170 .48 0      - - - - true 2 380    370    1200 0   0      timeout 0 960     910     3900   1.8  0     
reducercommutativity/sep10_true-unreach-call.i true 2 56   56   250 570 .48 0      - - - - timeout 0 900    890    1200 0   0      out of memory 0 890     760     7000   .63 0     
reducercommutativity/sep20_true-unreach-call.i true 2 11   11   230 140 .48 0      - - - - timeout 0 900    890    1200 0   0      timeout 0 960     830     6500   .64 0     
reducercommutativity/sep40_true-unreach-call.i true 2 11   12   230 150 .48 0      - - - - timeout 0 900    890    1200 0   0      timeout 0 960     920     1400   1.1  0     
reducercommutativity/sep60_true-unreach-call.i true 2 35   35   240 410 .48 0      - - - - timeout 0 900    890    1200 0   0      timeout 0 960     920     930   1.0  0     
reducercommutativity/sep_true-unreach-call_true-termination.i true 2 17   17   280 200 .49 0      - - - - timeout 0 900    890    2600 0   0      timeout 0 960     900     1900   .65 .0041
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 24   24   240 300 .48 .13   - - - - timeout 0 900    900    1300 0   0      timeout 0 960     950     4600   .64 0     
reducercommutativity/sum10_true-unreach-call_true-termination.i true 2 40   40   250 380 .48 2.3    - - - - timeout 0 900    900    3400 0   0      timeout 0 960     930     1100   1.1  0     
reducercommutativity/sum20_true-unreach-call.i true 2 13   13   220 180 .48 1.1    - - - - timeout 0 900    890    3400 0   0      timeout 0 960     920     5100   .63 0     
reducercommutativity/sum40_true-unreach-call.i true 2 20   20   240 250 .48 0      - - - - timeout 0 900    890    4400 0   0      timeout 0 960     930     960   .62 0     
reducercommutativity/sum60_true-unreach-call.i true 2 26   26   240 330 .48 0      - - - - timeout 0 900    890    4400 0   0      timeout 0 960     930     830   .65 0     
reducercommutativity/sum_true-unreach-call_true-termination.i true 2 11   11   250 140 .49 2.1    - - - - timeout 0 900    890    2700 0   0      timeout 0 960     940     600   .63 0     
array-tiling/mlceu_false-unreach-call.i unknown 0 9.9 10   130 120 .56 0      error (invalid witness file) 0 .60 .38 40 0   0      error (2) 0 .021 .022 5.6 0    0      error (invalid witness file) 0 .92 .59 47 0      0      error (invalid witness file) 0 .0019 .0025 .40 0      0      - -
array-tiling/skippedu_false-unreach-call.i unknown 0 110   110   580 1400 .56 .13   error (invalid witness file) 0 .64 .39 43 0   0      error (2) 0 .020 .021 5.6 0    0      error (invalid witness file) 0 .96 .62 48 0      0      error (invalid witness file) 0 .0059 .0076 .52 0      0      - -
array-tiling/mbpr2_true-unreach-call.i true 2 10   11   240 120 .50 0      - - - - timeout 0 900    870    4200 0   0      timeout 0 960     930     1100   .63 0     
array-tiling/mbpr3_true-unreach-call.i true 2 8.1 8.1 130 97 .50 0      - - - - timeout 0 900    870    5300 0   0      timeout 0 960     930     800   .63 0     
array-tiling/mbpr4_true-unreach-call.i true 2 17   17   240 220 .52 2.3    - - - - out of memory 0 510    450    7000 0   0      timeout 0 960     910     1000   .63 0     
array-tiling/mbpr5_true-unreach-call.i true 2 26   26   130 390 .54 1.9    - - - - out of memory 0 610    520    7000 0   0      timeout 0 960     900     1100   .99 0     
array-tiling/nr2_true-unreach-call.i true 2 12   12   260 140 .49 1.1    - - - - timeout 0 900    880    5700 0   0      timeout 0 960     940     1200   .62 0     
array-tiling/nr3_true-unreach-call.i true 2 6.6 6.8 130 83 .49 0      - - - - timeout 0 900    880    5000 0   0      timeout 0 960     940     1200   .63 0     
array-tiling/nr4_true-unreach-call.i true 2 8.9 9.0 240 96 .49 0      - - - - timeout 0 900    880    4400 0   0      timeout 0 960     930     2400   1.0  0     
array-tiling/nr5_true-unreach-call.i true 2 6.7 6.9 130 83 .49 0      - - - - timeout 0 900    880    4300 0   0      timeout 0 960     920     2100   1.0  0     
array-tiling/pnr2_true-unreach-call.i true 2 7.4 7.5 230 92 .49 0      - - - - timeout 0 900    890    1200 0   0      timeout 0 960     930     1100   .64 0     
array-tiling/pnr3_true-unreach-call.i true 2 5.8 6.1 130 74 .49 0      - - - - timeout 0 900    900    900 0   0      timeout 0 960     920     990   1.0  0     
array-tiling/pnr4_true-unreach-call.i true 2 13   13   240 140 .49 0      - - - - timeout 0 900    900    610 0   0      timeout 0 960     920     910   .63 0     
array-tiling/pnr5_true-unreach-call.i true 2 15   16   130 200 .50 0      - - - - timeout 0 900    900    650 0   0      timeout 0 960     910     2500   .97 0     
array-tiling/poly1_true-unreach-call.i true 2 10   10   230 100 .48 0      - - - - timeout 0 900    890    5600 0   0      timeout 0 960     940     770   .98 0     
array-tiling/poly2_true-unreach-call.i true 2 9.9 10   240 130 .49 0      - - - - timeout 0 900    890    4800 0   0      timeout 0 960     950     560   .62 0     
array-tiling/pr2_true-unreach-call.i true 2 12   12   230 120 .49 0      - - - - timeout 0 900    890    2300 0   0      timeout 0 960     910     1400   .68 0     
array-tiling/pr3_true-unreach-call.i true 2 5.9 5.9 130 70 .49 2.4    - - - - timeout 0 900    890    2300 0   0      timeout 0 960     930     1500   .95 0     
array-tiling/pr4_true-unreach-call.i true 2 14   14   230 150 .49 2.1    - - - - timeout 0 900    890    2100 0   .0041 timeout 0 960     930     1000   .98 0     
array-tiling/pr5_true-unreach-call.i true 2 23   23   130 300 .50 0      - - - - timeout 0 900    890    2100 0   0      timeout 0 960     910     1200   .63 0     
array-tiling/revcpyswp2_true-unreach-call.i true 2 120   120   530 1300 .64 2.1    - - - - timeout 0 900    890    1900 0   0      timeout 0 960     920     800   .63 0     
array-tiling/rew_true-unreach-call.i true 2 7.2 7.2 230 100 .48 0      - - - - timeout 0 900    890    2700 0   0      timeout 0 960     940     1600   .62 0     
array-tiling/rewnif_true-unreach-call.i true 2 7.9 8.1 240 95 .48 0      - - - - timeout 0 900    890    2400 0   0      timeout 0 960     930     1000   1.0  0     
array-tiling/rewnifrev2_true-unreach-call.i true 2 11   11   290 140 .48 0      - - - - timeout 0 900    890    2000 0   0      timeout 0 960     920     2500   .68 .39  
array-tiling/rewnifrev_true-unreach-call.i true 2 10   11   250 110 .48 0      - - - - timeout 0 900    890    2300 0   0      timeout 0 960     770     1100   1.2  0     
array-tiling/rewrev_true-unreach-call.i true 2 7.4 7.4 230 84 .48 0      - - - - timeout 0 900    890    2300 0   0      timeout 0 960     900     1700   1.1  0     
array-tiling/skipped_true-unreach-call.i true 2 10   10   240 110 .49 .13   - - - - timeout 0 900    900    1200 0   0      timeout 0 960     920     2900   1.0  0     
array-tiling/tcpy_true-unreach-call.i true 2 19   20   480 250 .49 0      - - - - timeout 0 900    900    1200 0   0      timeout 0 960     930     1400   1.0  .020 
array-programs/copysome1_false-unreach-call.i false(unreach-call) 0 9.7 9.7 160 150 1.9  0      exception 0 3.6  2.0  200 0   0      true -32 12     6.2   650   .62 0      exception 0 3.8  2.1  210 0      0      true -32 .69   .69   32    .049  .0041 - -
array-programs/copysome2_false-unreach-call.i false(unreach-call) 0 12   12   180 180 2.3  1.0    exception 0 3.7  2.0  200 0   0      true -32 13     7.5   720   .66 0      exception 0 4.3  2.3  210 0      0      true -32 .74   .76   36    .049  0      - -
array-programs/copysome1_true-unreach-call.i true 2 88   88   270 1000 .49 1.7    - - - - timeout 0 900    890    5100 0   .0041 timeout 0 960     930     2300   .97 0     
array-programs/copysome2_true-unreach-call.i true 2 120   120   250 1700 .50 0      - - - - timeout 0 900    890    4200 0   0      timeout 0 960     930     2000   .62 0     
array-crafted/bAnd1_true-unreach-call.i true 2 13   13   240 150 .48 0      - - - - timeout 0 900    890    3800 0   0      timeout 0 960     930     960   1.1  0     
array-crafted/bAnd2_true-unreach-call.i true 2 13   14   240 150 .48 .13   - - - - timeout 0 900    890    4100 0   0      timeout 0 960     920     990   .94 0     
array-crafted/bAnd3_true-unreach-call.i true 2 15   16   250 180 .48 2.0    - - - - timeout 0 900    890    4100 0   0      timeout 0 960     900     850   .90 0     
array-crafted/bAnd4_true-unreach-call.i true 2 29   31   240 430 .48 0      - - - - timeout 0 900    890    4400 0   0      timeout 0 960     920     960   .63 0     
array-crafted/bAnd5_true-unreach-call.i true 2 15   15   270 190 .49 0      - - - - timeout 0 900    890    3800 0   0      timeout 0 960     940     1100   .68 0     
array-crafted/bor1_true-unreach-call.i true 2 14   14   260 190 .48 0      - - - - timeout 0 900    890    4700 0   0      timeout 0 960     930     950   .63 0     
array-crafted/bor2_true-unreach-call.i true 2 15   16   260 180 .48 0      - - - - timeout 0 900    890    4600 0   0      timeout 0 960     920     860   .63 0     
array-crafted/bor3_true-unreach-call.i true 2 16   17   260 190 .48 1.7    - - - - timeout 0 900    890    4400 0   0      timeout 0 960     930     950   .97 0     
array-crafted/bor4_true-unreach-call.i true 2 31   32   260 370 .48 1.3    - - - - timeout 0 900    890    4500 0   0      timeout 0 960     920     930   .62 0     
array-crafted/bor5_true-unreach-call.i true 2 14   14   250 150 .49 0      - - - - timeout 0 900    890    3500 0   0      timeout 0 960     940     1000   .69 0     
array-crafted/mapavg1_true-unreach-call.i true 2 23   23   230 310 .48 1.3    - - - - timeout 0 900    890    3900 0   0      timeout 0 960     920     880   .63 0     
array-crafted/mapavg2_true-unreach-call.i true 2 23   23   230 280 .48 .0041 - - - - timeout 0 900    890    3800 0   0      timeout 0 960     920     1000   .63 0     
array-crafted/mapavg3_true-unreach-call.i true 2 24   25   240 290 .48 2.0    - - - - timeout 0 900    890    3900 0   0      timeout 0 960     920     890   .63 0     
array-crafted/mapavg4_true-unreach-call.i true 2 39   40   230 510 .48 1.1    - - - - timeout 0 900    890    4000 0   0      timeout 0 960     920     940   .64 0     
array-crafted/mapavg5_true-unreach-call.i true 2 12   12   240 140 .49 0      - - - - exception 0 5.8  3.7  470 0   0      timeout 0 960     950     610   .98 0     
array-crafted/mapsum1_true-unreach-call.i true 2 40   40   240 480 .48 0      - - - - timeout 0 900    890    4300 0   0      timeout 0 960     920     890   1.0  0     
array-crafted/mapsum2_true-unreach-call.i true 2 40   40   240 450 .48 0      - - - - timeout 0 900    890    4900 0   0      timeout 0 960     920     950   .63 0     
array-crafted/mapsum3_true-unreach-call.i true 2 43   44   240 480 .48 2.1    - - - - timeout 0 900    890    5100 0   0      timeout 0 960     920     870   .63 0     
array-crafted/mapsum4_true-unreach-call.i true 2 55   57   240 770 .48 0      - - - - timeout 0 900    890    4900 0   0      timeout 0 960     930     900   1.0  0     
array-crafted/mapsum5_true-unreach-call.i true 2 11   11   220 140 .49 1.7    - - - - timeout 0 900    890    2100 0   0      timeout 0 960     950     4700   .63 .0041
array-crafted/xor1_true-unreach-call.i true 2 46   46   330 720 .48 0      - - - - timeout 0 900    890    4900 0   0      timeout 0 960     920     890   .64 0     
array-crafted/xor2_true-unreach-call.i true 2 47   48   330 670 .48 0      - - - - timeout 0 900    890    4600 0   0      timeout 0 960     920     920   .97 0     
array-crafted/xor3_true-unreach-call.i true 2 48   49   340 620 .48 1.1    - - - - timeout 0 900    890    4700 0   .0041 timeout 0 960     920     940   .63 0     
array-crafted/xor4_true-unreach-call.i true 2 63   64   330 890 .48 0      - - - - timeout 0 900    890    4900 0   0      timeout 0 960     920     930   .62 0     
array-crafted/xor5_true-unreach-call.i true 2 38   38   290 540 .49 0      - - - - timeout 0 900    880    4100 0   0      timeout 0 960     930     990   .68 0     
array-crafted/zero_sum1_true-unreach-call.c true 2 63   63   220 840 .50 0      - - - - timeout 0 900    900    780 0   0      timeout 0 960     870     1700   .98 0     
array-crafted/zero_sum2_true-unreach-call.c true 2 73   73   230 870 .52 0      - - - - timeout 0 900    890    1300 0   0      timeout 0 960     870     1900   .63 0     
array-crafted/zero_sum3_true-unreach-call.c true 2 81   81   240 1200 .54 0      - - - - timeout 0 900    880    2900 0   0      timeout 0 960     860     1900   .63 0     
array-crafted/zero_sum4_true-unreach-call.c true 2 89   89   250 1300 .56 .13   - - - - timeout 0 900    860    6000 0   0      timeout 0 960     850     2000   .63 0     
array-crafted/zero_sum5_true-unreach-call.c true 2 98   98   260 1500 .58 0      - - - - timeout 0 910    650    6900 0   0      timeout 0 960     860     2600   .63 0     
array-crafted/zero_sum_const1_true-unreach-call.c true 2 65   65   450 780 .51 1.1    - - - - timeout 0 900    890    5100 0   0      timeout 0 960     870     1800   .62 0     
array-crafted/zero_sum_const2_true-unreach-call.c true 2 73   73   480 950 .53 0      - - - - timeout 0 900    860    5400 0   0      out of memory 0 530     430     7000   .63 0     
array-crafted/zero_sum_const3_true-unreach-call.c true 2 81   81   450 990 .55 0      - - - - out of memory 0 820    740    7000 0   0      out of memory 0 340     250     7000   .65 0     
array-crafted/zero_sum_const4_true-unreach-call.c true 2 88   89   240 1300 .57 1.7    - - - - timeout 0 920    630    6200 0   0      timeout 0 960     870     1800   .65 0     
array-crafted/zero_sum_const5_true-unreach-call.c true 2 97   97   270 1300 .59 0      - - - - timeout 0 910    620    5900 0   0      timeout 0 960     860     2900   .82 0     
array-crafted/zero_sum_const_m2_true-unreach-call.c true 2 73   73   440 900 .53 1.7    - - - - timeout 0 900    860    6000 0   0      timeout 0 960     900     2500   1.3  0     
array-crafted/zero_sum_const_m3_true-unreach-call.c true 2 81   81   440 970 .55 2.4    - - - - out of memory 0 750    670    7000 0   0      timeout 0 960     880     2300   .84 0     
array-crafted/zero_sum_const_m4_true-unreach-call.c true 2 88   88   410 1200 .57 1.1    - - - - timeout 0 910    630    6300 0   0      timeout 0 960     900     2400   1.1  .0041
array-crafted/zero_sum_const_m5_true-unreach-call.c true 2 96   96   330 1500 .59 0      - - - - timeout 0 900    610    6000 0   0      timeout 0 960     880     1100   .63 0     
array-crafted/zero_sum_m2_true-unreach-call.c true 2 73   73   230 1000 .52 1.9    - - - - timeout 0 900    890    750 0   0      timeout 0 960     890     1700   1.0  0     
array-crafted/zero_sum_m3_true-unreach-call.c true 2 81   81   230 1000 .54 1.7    - - - - timeout 0 900    890    2400 0   0      timeout 0 960     890     1400   2.0  0     
array-crafted/zero_sum_m4_true-unreach-call.c true 2 89   89   230 1400 .56 0      - - - - timeout 0 900    850    5200 0   0      timeout 0 960     880     1500   .63 0     
array-crafted/zero_sum_m5_true-unreach-call.c true 2 98   98   270 1400 .58 1.7    - - - - timeout 0 900    840    5800 0   0      timeout 0 960     890     1400   1.1  0     
array-multidimensional/add-2-n-u_true-unreach-call.i true 2 65   65   470 670 .54 0      - - - - out of memory 0 400    380    7000 0   0      timeout 0 960     940     870   .63 0     
array-multidimensional/add-3-n-u_true-unreach-call.i true 2 73   73   540 820 .59 2.2    - - - - out of memory 0 460    410    7000 0   .0041 timeout 0 960     950     510   .63 0     
array-multidimensional/copy-2-u_true-unreach-call.i true 2 62   63   610 680 .54 .13   - - - - timeout 0 910    870    6900 0   0      timeout 0 960     950     1200   .64 0     
array-multidimensional/copy-3-n-u_true-unreach-call.i true 2 70   70   620 760 .57 0      - - - - out of memory 0 540    470    7000 0   0      timeout 0 960     950     730   .63 0     
array-multidimensional/copy-partial-2-n-u_true-unreach-call.i true 2 63   63   510 670 .54 0      - - - - out of memory 0 500    470    7000 0   0      timeout 0 960     950     1000   .63 0     
array-multidimensional/copy-partial-3-u_true-unreach-call.i true 2 14   14   130 190 .52 0      - - - - true 2 12    6.6  470 0   0      true 2 12     6.5   400   .62 0     
array-multidimensional/diff-2-n-u_true-unreach-call.i true 2 67   67   520 780 .56 .13   - - - - out of memory 0 530    490    7000 0   0      timeout 0 960     950     750   .98 0     
array-multidimensional/diff-3-n-u_true-unreach-call.i true 2 73   73   540 820 .59 1.7    - - - - out of memory 0 480    430    7000 0   0      timeout 0 960     950     480   1.0  0     
array-multidimensional/init-2-n-u_true-unreach-call.i true 2 60   60   620 710 .51 2.3    - - - - timeout 0 900    880    7000 0   0      timeout 0 960     950     1000   .63 0     
array-multidimensional/init-3-u_true-unreach-call.i true 2 64   64   660 800 .52 0      - - - - out of memory 0 620    590    7000 0   0      timeout 0 960     950     630   .62 0     
array-multidimensional/init-4-n-u_true-unreach-call.i true 2 70   70   650 870 .51 1.7    - - - - out of memory 0 470    440    7000 0   .0041 timeout 0 960     950     740   .63 .016 
array-multidimensional/init-non-constant-2-n-u_true-unreach-call.i true 2 60   60   810 560 .52 0      - - - - timeout 0 900    880    5500 0   0      timeout 0 960     940     1100   .63 0     
array-multidimensional/init-non-constant-3-u_true-unreach-call.i true 2 65   65   720 790 .52 .13   - - - - out of memory 0 400    380    7000 0   0      timeout 0 960     950     1100   .63 0     
array-multidimensional/max-2-u_true-unreach-call.i true 2 150   150   1300 1600 .66 1.7    - - - - timeout 0 900    880    4300 0   0      timeout 0 960     950     1000   .62 0     
array-multidimensional/max-3-n-u_true-unreach-call.i true 2 190   190   1100 2100 .79 0      - - - - out of memory 0 890    840    7000 0   0      timeout 0 960     940     1800   .68 0     
array-multidimensional/min-2-u_true-unreach-call.i true 2 150   150   2300 1800 .66 0      - - - - out of memory 0 870    840    7000 0   0      timeout 0 960     950     980   .98 0     
array-multidimensional/min-3-n-u_true-unreach-call.i true 2 190   190   1000 2000 .79 .13   - - - - out of memory 0 610    540    7000 0   0      timeout 0 960     950     1900   .68 0     
array-multidimensional/rev-2-n-u_true-unreach-call.i true 2 64   64   590 730 .54 1.1    - - - - out of memory 0 700    670    7000 0   0      out of memory 0 440     410     7000   .63 .025 
array-multidimensional/rev-3-u_true-unreach-call.i true 2 70   71   620 690 .57 .13   - - - - out of memory 0 480    420    7000 0   0      timeout 0 960     960     630   .63 0     
array-multidimensional/transpose-u_true-unreach-call.i true 2 63   63   540 670 .54 0      - - - - out of memory 0 610    580    7000 0   0      timeout 0 960     950     480   .63 0     
loops/array_false-unreach-call_true-termination.i false(unreach-call) 1 5.3 5.3 130 70 1.2  0      false(unreach-call) 1 3.5  2.0  250 0   0      false(unreach-call) 1 7.3   4.6   320   .66 0      unknown 0 3.5  2.1  250 0      0      true -32 .60   .60   20    .049  0      - -
loops/bubble_sort_false-unreach-call.i unknown 0 2.4 2.4 130 31 .22 .70   error (invalid witness file) 0 .59 .36 40 0   0      error (2) 0 .020 .021 5.6 0    0      error (invalid witness file) 0 .94 .61 47 0      0      error (invalid witness file) 0 .0018 .0031 .54 0      0      - -
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 4.9 4.9 130 66 .95 .0041 false(unreach-call) 1 7.9  4.4  350 0   0      false(unreach-call) 1 16     8.6   860   .66 0      unknown 0 5.3  3.0  270 0      0      false(unreach-call) 1 .61   .61   25    .045  0      - -
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 0 14   14   130 210 3.9  1.0    timeout 0 98    85    1300 0   0      true -32 7.0   4.0   300   .35 0      unknown 0 3.6  2.1  250 0      0      true -32 .59   .59   20    .057  0      - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 6.7 6.7 130 94 1.4  0      false(unreach-call) 1 3.6  2.0  250 0   0      true -32 7.7   4.4   310   .66 0      unknown 0 3.8  2.2  250 0      0      true -32 .57   .57   20    .049  0      - -
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 0 10   10   510 120 1.6  .17   timeout 0 98    83    2000 0   0      timeout 0 96     55     7000   1.5  0      unknown 0 84    71    1900 0      0      true -32 1.4    1.4    90    .049  0      - -
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 0 8.1 8.1 310 110 1.4  0      exception 0 4.6  2.4  200 0   0      true -32 29     18     2100   .62 0      exception 0 5.2  2.8  210 0      0      true -32 .97   .99   57    .057  0      - -
loops/linear_search_false-unreach-call.i unknown 0 2.4 2.4 130 37 .22 0      error (invalid witness file) 0 .61 .40 43 0   0      error (2) 0 .021 .021 5.6 0    0      error (invalid witness file) 0 .94 .60 47 0      0      error (invalid witness file) 0 .0055 .0071 .53 0      0      - -
loops/ludcmp_false-unreach-call.i false(unreach-call) 1 30   30   140 410 5.2  .96   false(unreach-call) 1 9.6  7.3  520 0   0      true -32 41     31     840   .71 0      false(unreach-call) 1 3.9  2.3  250 0      0      false(unreach-call) 1 .59   .59   21    .061  0      - -
loops/matrix_false-unreach-call_true-termination.i unknown 0 430   430   900 5000 .69 1.7    error (invalid witness file) 0 .63 .41 41 0   0      error (2) 0 .021 .021 5.6 0    0      error (invalid witness file) 0 .91 .58 47 0      0      error (invalid witness file) 0 .0053 .0059 .39 0      0      - -
loops/n.c24_false-unreach-call.i unknown 0 2.5 2.5 130 34 .22 0      error (invalid witness file) 0 .61 .39 40 0   0      error (2) 0 .021 .022 5.6 0    0      error (invalid witness file) 0 .96 .61 47 0      0      error (invalid witness file) 0 .0051 .0069 .40 0      0      - -
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 5.0 5.0 130 83 1.2  .62   exception 0 2.3  1.3  170 0   0      false(unreach-call) 1 7.1   4.0   310   .66 .0041 exception 0 2.8  1.6  200 0      0      false(unreach-call) 1 .61   .61   20    .049  0      - -
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 7.7 7.7 130 120 2.1  0      false(unreach-call) 1 3.8  2.1  260 0   0      true -32 6.8   4.3   310   .62 .0041 unknown 0 3.7  2.2  250 0      0      false(unreach-call) 1 .59   .59   20    .053  0      - -
loops/s3_false-unreach-call.i unknown 0 2.5 2.5 130 31 .22 .066  error (invalid witness file) 0 .60 .36 40 0   0      error (2) 0 .020 .021 5.6 0    0      error (invalid witness file) 0 .93 .59 47 0      0      error (invalid witness file) 0 .0021 .0026 .53 0      0      - -
loops/string_false-unreach-call_true-termination.i unknown 0 17   17   130 260 .65 0      error (invalid witness file) 0 .61 .37 41 0   0      error (2) 0 .021 .022 5.6 0    0      error (invalid witness file) 0 .94 .61 47 0      0      error (invalid witness file) 0 .0060 .0077 .39 0      0      - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 5.3 5.3 130 69 1.2  0      false(unreach-call) 1 4.6  2.5  260 0   0      true -32 7.5   4.2   310   .66 0      unknown 0 3.7  2.1  250 0      0      true -32 .59   .61   20    .049  0      - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 0 5.5 5.5 140 68 1.2  0      true -32 13    6.7  430 0   0      timeout 0 91     58     7000   .63 0      unknown 0 9.7  5.2  280 0      .0041 true -32 .69   .68   30    .049  0      - -
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 0 5.6 5.6 150 78 1.2  0      true -32 6.0  3.2  260 0   0      out of memory 0 74     47     7000   1.4  0      unknown 0 11    5.6  340 0      0      true -32 .71   .70   32    .045  0      - -
loops/sum03_false-unreach-call_true-termination.i unknown 0 98   82   15000 1500 .27 .0041 error (invalid witness file) 0 .61 .37 42 0   0      error (2) 0 .020 .021 5.6 0    0      error (invalid witness file) 0 .96 .61 48 0      0      error (invalid witness file) 0 .0063 .0081 .52 0      0      - -
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 5.2 5.3 130 71 1.2  .64   true -32 4.4  2.4  260 0   0      out of memory 0 59     38     7000   .63 0      false(unreach-call) 1 5.0  2.8  260 0      0      false(unreach-call) 1 .61   .61   22    .045  0      - -
loops/sum_array_false-unreach-call.i false(unreach-call) 0 8.0 8.1 200 110 1.6  0      timeout 0 95    89    1000 0   .0041 timeout 0 91     58     7000   .62 0      unknown 0 12    6.3  360 0      0      true -32 .82   .84   40    .057  0      - -
loops/terminator_01_false-unreach-call_true-termination.i unknown 0 2.4 2.4 130 34 .22 0      error (invalid witness file) 0 .61 .38 41 0   0      error (2) 0 .020 .021 5.6 0    0      error (invalid witness file) 0 .92 .60 47 0      0      error (invalid witness file) 0 .0037 .0048 .41 0      0      - -
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 5.8 5.8 130 72 1.4  .0041 exception 0 2.7  1.5  190 0   0      false(unreach-call) 1 7.0   4.0   310   .66 0      exception 0 2.8  1.6  200 0      0      false(unreach-call) 1 .65   .65   20    .049  0      - -
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 5.3 5.3 130 81 1.2  0      exception 0 2.4  1.4  190 0   0      false(unreach-call) 1 8.1   4.9   310   .66 0      exception 0 2.8  1.6  180 0      0      true -32 .58   .59   20    .045  0      - -
loops/trex01_false-unreach-call_true-termination.i error (1) 0 4.8 4.9 130 69 .46 0      error (invalid witness file) 0 .60 .38 41 0   0      error (2) 0 .020 .021 5.6 0    0      error (invalid witness file) 0 .95 .62 47 0      0      error (invalid witness file) 0 .0030 .0033 .40 0      0      - -
loops/trex02_false-unreach-call_true-termination.i unknown 0 5.9 5.9 130 74 .49 0      error (invalid witness file) 0 .62 .39 41 0   0      error (2) 0 .020 .022 5.6 0    0      error (invalid witness file) 0 .91 .60 46 0      0      error (invalid witness file) 0 .0066 .0083 .52 0      0      - -
loops/trex03_false-unreach-call_true-termination.i witness invalid (false(unreach-call)) 0 6.5 6.5 130 92 1.6  0      error (invalid witness file) 0 2.5  1.4  200 0   0      error (invalid witness file) 0 5.2   2.8   270   .65 0      error (invalid witness file) 0 2.9  1.7  180 0      0      error (invalid witness file) 0 .56   .58   20    .0041 0      - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i unknown 0 2.4 2.4 130 34 .22 .48   error (invalid witness file) 0 .58 .37 40 0   0      error (2) 0 .019 .020 5.6 0    0      error (invalid witness file) 0 .98 .63 48 0      0      error (invalid witness file) 0 .0062 .0078 .52 0      0      - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i unknown 0 2.5 2.5 130 33 .22 0      error (invalid witness file) 0 .58 .36 40 0   0      error (2) 0 .024 .024 5.6 0    0      error (invalid witness file) 0 .92 .59 46 0      0      error (invalid witness file) 0 .0063 .0082 .52 0      0      - -
loops/vogal_false-unreach-call.i unknown 0 340   350   550 4100 .88 0      error (invalid witness file) 0 .58 .36 40 0   0      error (2) 0 .020 .021 5.6 0    0      error (invalid witness file) 0 .95 .62 47 0      0      error (invalid witness file) 0 .0054 .0067 .53 0      0      - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i unknown 0 97   81   15000 1600 .27 .0041 error (invalid witness file) 0 .58 .35 40 0   0      error (2) 0 .021 .021 5.6 0    0      error (invalid witness file) 0 .97 .63 48 0      0      error (invalid witness file) 0 .0067 .010  .53 0      0      - -
loops/array_true-unreach-call_true-termination.i true 2 18   18   250 180 .48 .0041 - - - - true 2 4.5  2.5  290 0   0      true 2 11     6.8   400   .62 0     
loops/bubble_sort_true-unreach-call_true-termination.i true 1 9.5 9.6 130 140 .46 0      - - - - error (invalid witness file) 0 .61 .38 41 0   0      error (2) 0 .022 .023 5.6 0    0     
loops/count_up_down_true-unreach-call_true-termination.i true 2 4.6 4.7 130 55 .48 2.2    - - - - out of memory 0 380    370    7000 0   0      true 2 11     6.7   370   .62 .0041
loops/eureka_01_true-unreach-call.i true 1 110   110   420 1500 .63 0      - - - - timeout 0 900    880    5200 0   0      timeout 0 960     930     5000   .70 0     
loops/eureka_05_true-unreach-call_true-termination.i true 1 8.4 8.4 230 95 .48 2.1    - - - - timeout 0 900    890    3600 0   0      timeout 0 960     930     1500   1.1  0     
loops/for_infinite_loop_1_true-unreach-call_false-termination.i unknown 0 110   98   15000 1600 .27 .0041 - - - - error (invalid witness file) 0 .64 .41 40 0   0      error (2) 0 .022 .023 5.7 0    0     
loops/for_infinite_loop_2_true-unreach-call_false-termination.i unknown 0 110   98   15000 1700 .27 1.0    - - - - error (invalid witness file) 0 .59 .36 41 0   0      error (2) 0 .036 .037 5.6 0    0     
loops/insertion_sort_true-unreach-call_true-termination.i true 1 35   35   530 360 .49 0      - - - - timeout 0 900    890    1200 0   0      timeout 0 960     900     1500   1.8  0     
loops/invert_string_true-unreach-call_true-termination.i true 2 59   59   430 670 .51 2.4    - - - - true 2 17    12    500 0   0      true 2 390     370     1300   .62 0     
loops/linear_sea.ch_true-unreach-call.i unknown 0 2.4 2.4 130 37 .22 .62   - - - - error (invalid witness file) 0 .59 .37 41 0   0      error (2) 0 .021 .021 5.6 0    0     
loops/lu.cmp_true-unreach-call.i error (1) 0 160   160   130 2100 5.1  0      - - - - error (invalid witness file) 0 .62 .38 40 0   0      error (2) 0 .020 .020 5.6 0    0     
loops/matrix_true-unreach-call_true-termination.i true 2 60   60   570 720 .50 0      - - - - true 2 4.4  2.5  290 0   0      true 2 11     6.9   430   .62 0     
loops/n.c11_true-unreach-call_false-termination.i true 2 56   56   150 830 .49 0      - - - - out of memory 0 760    740    7000 0   0      true 2 11     6.1   360   .62 0     
loops/n.c40_true-unreach-call_true-termination.i unknown 0 160   160   510 1800 .50 0      - - - - error (invalid witness file) 0 .59 .36 40 0   0      error (2) 0 .056 .057 5.5 0    0     
loops/nec40_true-unreach-call_true-termination.i unknown 0 160   160   570 1600 .52 .0041 - - - - error (invalid witness file) 0 .61 .38 41 0   0      error (2) 0 .021 .022 5.6 0    0     
loops/string_true-unreach-call_true-termination.i unknown 0 17   17   130 220 .65 1.7    - - - - error (invalid witness file) 0 .58 .37 41 0   0      error (2) 0 .024 .024 5.6 0    0     
loops/sum01_true-unreach-call_true-termination.i true 2 5.5 5.5 130 65 .52 0      - - - - out of memory 0 460    450    7000 0   0      true 2 11     6.3   390   .62 0     
loops/sum03_true-unreach-call_false-termination.i unknown 0 88   72   15000 1400 .27 .0041 - - - - error (invalid witness file) 0 .61 .37 40 0   0      error (2) 0 .048 .051 5.7 0    0     
loops/sum04_true-unreach-call_true-termination.i true 2 5.2 5.3 130 73 .48 0      - - - - true 2 6.1  3.3  290 0   0      true 2 11     6.9   430   .62 0     
loops/sum_array_true-unreach-call.i unknown 0 470   470   430 5800 .66 0      - - - - error (invalid witness file) 0 .62 .39 40 0   0      error (2) 0 .024 .034 5.7 0    0     
loops/terminator_02_true-unreach-call_true-termination.i true 2 5.8 6.0 130 81 .52 0      - - - - true 2 4.5  2.5  290 0   0      true 2 7.8   4.9   310   .62 0     
loops/terminator_03_true-unreach-call_true-termination.i unknown 0 7.5 7.7 130 96 .56 1.7    - - - - error (invalid witness file) 0 .62 .38 41 0   0      error (2) 0 .034 .038 5.6 0    0     
loops/trex01_true-unreach-call_true-termination.i true 2 9.5 9.6 150 140 .47 2.1    - - - - true 2 32    21    1100 0   0      true 2 7.4   4.6   310   .62 0     
loops/trex02_true-unreach-call_true-termination.i true 2 4.7 5.0 130 53 .48 0      - - - - true 2 4.2  2.3  280 0   0      true 2 7.0   4.4   310   .62 0     
loops/trex03_true-unreach-call_true-termination.i true 2 5.7 5.8 130 67 .48 1.1    - - - - true 2 5.3  3.0  290 0   0      true 2 7.3   4.6   310   .62 0     
loops/trex04_true-unreach-call_false-termination.i timeout 0 900   900   130 8600 .27 0      - - - - error (invalid witness file) 0 .60 .38 41 0   0      error (2) 0 .049 .051 5.5 0    0     
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i unknown 0 2.4 2.4 130 36 .22 0      - - - - error (invalid witness file) 0 .72 .44 42 0   0      error (2) 0 .040 .041 5.5 0    0     
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i unknown 0 2.5 2.5 130 37 .22 0      - - - - error (invalid witness file) 0 .61 .38 41 0   0      error (2) 0 .050 .051 5.5 0    0     
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i unknown 0 2.7 2.7 130 39 .22 .91   - - - - error (invalid witness file) 0 .66 .40 41 0   0      error (2) 0 .048 .049 5.5 0    0     
loops/vogal_true-unreach-call.i true 2 240   240   350 3500 .76 0      - - - - true 2 72    59    1000 0   0      timeout 0 960     920     1300   .63 0     
loops/while_infinite_loop_1_true-unreach-call_false-termination.i out of memory 0 96   81   15000 1600 .25 .64   - - - - error (invalid witness file) 0 .60 .37 40 0   0      error (2) 0 .021 .030 5.5 0    0     
loops/while_infinite_loop_2_true-unreach-call_false-termination.i out of memory 0 95   80   15000 1300 .25 .0041 - - - - error (invalid witness file) 0 .62 .40 41 0   0      error (2) 0 .041 .042 5.5 0    0     
loops/while_infinite_loop_3_true-unreach-call_false-termination.i out of memory 0 97   81   15000 1400 .25 .0041 - - - - error (invalid witness file) 0 .60 .37 41 0   0      error (2) 0 .023 .023 5.6 0    0     
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 1 4.7 4.7 130 67 .95 0      timeout 0 97    91    810 0   0      true -32 7.6   4.3   310   .66 0      false(unreach-call) 1 3.5  2.1  250 0      0      false(unreach-call) 1 .60   .60   20    .045  0      - -
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 1 4.7 4.7 130 70 .95 0      timeout 0 97    91    1100 0   0      true -32 7.6   4.3   310   .66 0      false(unreach-call) 1 3.4  2.0  240 0      0      false(unreach-call) 1 .59   .58   20    .045  0      - -
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 5.5 5.5 130 79 1.2  0      timeout 0 96    89    1000 0   0      true -32 7.3   4.6   310   .66 0      true -32 3.8  2.2  250 0      0      true -32 .57   .57   20    .049  0      - -
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 4.7 4.7 130 63 .95 0      true -32 5.5  2.9  260 0   0      out of memory 0 81     55     7000   .63 .0041 false(unreach-call) 1 4.7  2.6  260 0      .0041 false(unreach-call) 1 .58   .58   22    .045  0      - -
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 5.8 5.8 130 76 1.4  0      false(unreach-call) 1 43    34    800 0   0      true -32 8.5   5.4   320   .66 0      unknown 0 3.4  2.0  240 0      0      false(unreach-call) 1 .61   .61   20    .045  0      - -
loop-acceleration/functions_false-unreach-call1_true-termination.i false(unreach-call) 1 5.9 5.9 130 80 1.2  .041  exception 0 3.0  1.6  210 0   0      true -32 8.0   4.4   300   .66 0      exception 0 3.2  1.8  210 0      0      false(unreach-call) 1 1.0    1.0    22    .045  0      - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 4.7 4.7 130 70 .95 .078  exception 0 2.4  1.3  170 0   0      false(unreach-call) 1 6.8   4.3   300   .66 0      exception 0 3.0  1.7  170 0      0      false(unreach-call) 1 .56   .56   20    .045  0      - -
loop-acceleration/nested_false-unreach-call1.i false(unreach-call) 1 26   26   2600 240 1.2  0      exception 0 14    8.1  990 0   0      true -32 13     6.8   680   .66 0      exception 0 12    6.9  930 0      0      false(unreach-call) 1 8.6    8.6    450    .045  0      - -
loop-acceleration/phases_false-unreach-call1.i false(unreach-call) 1 6.1 6.1 130 81 1.4  .0041 exception 0 2.7  1.5  200 0   0      true -32 7.9   4.4   410   .62 .0041 exception 0 3.3  1.9  210 0      0      false(unreach-call) 1 .86   .86   22    .045  0      - -
loop-acceleration/phases_false-unreach-call2_false-termination.i timeout 0 900   900   130 14000 .27 .98   error (invalid witness file) 0 .61 .37 41 0   0      error (2) 0 .021 .022 5.6 0    0      error (invalid witness file) 0 .92 .60 47 0      0      error (invalid witness file) 0 .0047 .0054 .39 0      0      - -
loop-acceleration/simple_false-unreach-call1.i false(unreach-call) 1 4.9 4.9 130 73 .95 0      exception 0 2.6  1.4  190 0   0      true -32 7.8   4.3   340   .66 0      exception 0 3.2  1.8  200 0      0      false(unreach-call) 1 .80   .80   21    .045  0      - -
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 0 5.1 5.2 130 68 .95 0      exception 0 2.8  1.5  190 0   0      true -32 10     5.5   530   .66 .0041 exception 0 3.0  1.7  200 0      0      true -32 .57   .57   21    .045  0      - -
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 4.7 4.7 130 60 .95 .62   exception 0 2.6  1.5  200 0   0      true -32 8.0   4.8   430   .62 0      exception 0 3.1  1.8  200 0      0      false(unreach-call) 1 .57   .57   21    .045  0      - -
loop-acceleration/simple_false-unreach-call4.i out of memory 0 39   28   15000 500 .95 0      error (invalid witness file) 0 .61 .37 41 0   0      error (2) 0 .021 .021 5.6 0    0      error (invalid witness file) 0 .98 .64 49 0      0      error (invalid witness file) 0 .0049 .0061 .52 0      0      - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 4.8 4.8 130 60 .95 .0041 false(unreach-call) 1 3.8  2.1  250 0   0      true -32 9.4   5.8   310   .62 0      false(unreach-call) 1 3.4  2.0  250 0      0      false(unreach-call) 1 .61   .63   20    .045  0      - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 4.8 4.8 130 60 .95 .62   false(unreach-call) 1 3.5  2.0  250 0   .0041 true -32 8.9   5.5   310   .66 0      false(unreach-call) 1 3.5  2.0  250 0      0      false(unreach-call) 1 .58   .58   20    .045  0      - -
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 7.6 7.8 240 86 .48 0      - - - - true 2 4.3  2.4  280 0   0      true 2 12     8.1   340   .62 0     
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 55   55   200 640 .49 2.1    - - - - timeout 0 900    890    5000 0   0      timeout 0 960     930     800   .94 0     
loop-acceleration/array_true-unreach-call3_true-termination.i true 2 8.0 8.3 220 88 .48 0      - - - - true 2 4.6  2.5  280 0   0      true 2 10     6.0   380   .62 0     
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 6.6 6.6 140 80 .48 0      - - - - timeout 0 900    890    6000 0   0      timeout 0 960     930     940   .62 0     
loop-acceleration/const_true-unreach-call1.i true 2 4.4 4.4 130 70 .48 2.0    - - - - true 2 4.5  2.5  280 0   .0041 true 2 8.4   5.3   320   .62 0     
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 140   140   240 1900 .51 .13   - - - - true 2 17    12    590 0   0      timeout 0 960     940     560   .97 0     
loop-acceleration/diamond_true-unreach-call2.i true 2 310   310   230 4900 .55 0      - - - - true 2 7.4  4.3  330 0   0      true 2 270     260     660   .62 0     
loop-acceleration/functions_true-unreach-call1_true-termination.i true 1 23   25   130 340 .48 1.7    - - - - out of memory 0 430    420    7000 0   0      timeout 0 960     930     580   .63 0     
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 4.6 4.7 130 62 .48 1.7    - - - - out of memory 0 410    400    7000 0   0      true 2 7.3   4.6   310   .62 0     
loop-acceleration/nested_true-unreach-call1.i true 2 150   150   130 1700 .48 0      - - - - true 2 6.0  3.3  300 0   0      true 2 43     31     750   .62 0     
loop-acceleration/overflow_true-unreach-call1.i true 1 190   190   130 1800 .48 .0041 - - - - out of memory 0 520    510    7000 0   0      timeout 0 960     940     540   .99 .0041
loop-acceleration/phases_true-unreach-call1.i true 1 120   120   260 1600 .51 .0041 - - - - timeout 0 910    890    6100 0   .0041 timeout 0 960     940     540   .63 0     
loop-acceleration/phases_true-unreach-call2_false-termination.i timeout 0 900   900   130 12000 .27 0      - - - - error (invalid witness file) 0 .61 .37 41 0   0      error (2) 0 .030 .032 5.6 0    0     
loop-acceleration/simple_true-unreach-call1.i true 1 16   17   130 170 .48 0      - - - - out of memory 0 570    550    7000 0   0      timeout 0 960     940     650   .63 0     
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 26   28   130 320 .48 1.1    - - - - true 2 4.1  2.3  280 0   0      true 2 6.9   4.0   300   .62 0     
loop-acceleration/simple_true-unreach-call3_true-termination.i true 2 4.5 4.6 130 54 .48 2.4    - - - - out of memory 0 750    740    7000 0   0      true 2 9.4   6.2   330   .62 0     
loop-acceleration/simple_true-unreach-call4.i true 2 16   17   130 170 .48 0      - - - - true 2 4.2  2.4  280 0   0      true 2 8.6   4.9   310   .62 0     
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 6.0 6.0 130 85 .50 0      - - - - true 2 7.0  4.8  390 0   0      true 2 26     22     460   .62 0     
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 5.2 5.3 130 75 .48 2.0    - - - - true 2 4.2  2.3  280 0   0      true 2 8.5   5.2   320   .62 0     
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i timeout 0 900   900   130 11000 .27 .0041 error (invalid witness file) 0 .59 .39 41 0   0      error (2) 0 .021 .022 5.6 0    0      error (invalid witness file) 0 .91 .60 46 0      0      error (invalid witness file) 0 .0049 .0059 .39 0      0      - -
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i true 1 11   11   240 130 .50 2.2    - - - - timeout 0 900    890    4300 0   0      timeout 0 960     940     620   1.0  .0041
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i unknown 0 160   160   250 2000 .57 2.4    - - - - error (invalid witness file) 0 .61 .38 42 0   0      error (2) 0 .039 .042 5.7 0    0     
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i true 1 10   10   240 130 .48 2.3    - - - - timeout 0 910    890    5600 0   0      timeout 0 960     940     720   1.1  0     
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i true 2 14   14   130 180 .59 0      - - - - timeout 0 900    890    1800 0   0      true 2 31     26     430   .62 0     
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true 2 29   29   190 460 .48 0      - - - - true 2 4.3  2.4  280 0   0      true 2 7.3   4.1   320   .62 0     
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i true 2 28   29   190 450 .48 1.3    - - - - true 2 4.3  2.4  280 0   0      true 2 8.0   4.5   310   .62 0     
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+lhb-reducer.c unknown 0 2.6 2.6 130 34 .22 0      - - - - error (invalid witness file) 0 .60 .37 42 0   0      error (2) 0 .020 .021 5.6 0    0     
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+nlh-reducer.c unknown 0 2.5 2.5 130 39 .22 .63   - - - - error (invalid witness file) 0 .61 .37 40 0   0      error (2) 0 .040 .041 5.7 0    0     
loop-invgen/id_trans_false-unreach-call_true-termination.i unknown 0 7.3 7.5 130 110 .54 1.7    error (invalid witness file) 0 .60 .37 41 0   0      error (2) 0 .021 .021 5.6 0    0      error (invalid witness file) 0 .95 .61 48 0      0      error (invalid witness file) 0 .0066 .0085 .52 0      0      - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i error (1) 0 4.1 4.2 130 57 .46 0      - - - - error (invalid witness file) 0 .59 .35 40 0   0      error (2) 0 .020 .033 5.6 0    0     
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 6.7 6.7 140 81 .50 1.7    - - - - out of memory 0 550    540    7000 0   0      true 2 10     6.3   360   .62 0     
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i timeout 0 900   900   130 11000 .57 0      - - - - error (invalid witness file) 0 .60 .37 40 0   0      error (2) 0 .033 .034 5.6 0    0     
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i unknown 0 230   230   140 3300 3.3  2.0    - - - - error (invalid witness file) 0 .59 .36 41 0   0      error (2) 0 .021 .022 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i unknown 0 500   500   290 6400 3.6  0      - - - - error (invalid witness file) 0 .76 .47 41 0   0      error (2) 0 .021 .022 5.6 0    0     
loop-invgen/down_true-unreach-call_true-termination.i true 1 6.2 6.2 130 86 .49 0      - - - - out of memory 0 340    320    7000 0   .0041 timeout 0 960     790     3200   .63 0     
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i true 1 8.8 9.2 160 100 .48 1.4    - - - - out of memory 0 450    400    7000 0   0      timeout 0 960     800     3300   .66 .0041
loop-invgen/half_2_true-unreach-call_true-termination.i true 1 45   45   280 770 .52 0      - - - - out of memory 0 870    850    7000 0   0      timeout 0 960     800     1500   .63 0     
loop-invgen/heapsort_true-unreach-call_true-termination.i unknown 0 180   180   190 2400 .87 1.7    - - - - error (invalid witness file) 0 .60 .37 41 0   0      error (2) 0 .031 .031 5.6 0    0     
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 8.5 8.5 130 120 .50 0      - - - - true 2 4.8  2.7  290 0   0      true 2 8.1   4.6   310   .62 0     
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 34   34   160 370 .78 1.7    - - - - true 2 5.1  2.8  290 0   0      true 2 10     6.1   360   .66 0     
loop-invgen/nest-if3_true-unreach-call_true-termination.i unknown 0 110   120   450 1600 .56 2.2    - - - - error (invalid witness file) 0 .61 .38 40 0   0      error (2) 0 .050 .051 5.5 0    0     
loop-invgen/nested6_true-unreach-call_true-termination.i true 2 270   270   390 3000 .84 0      - - - - timeout 0 900    890    2300 0   0      true 2 10     6.1   390   .62 0     
loop-invgen/nested9_true-unreach-call_true-termination.i true 2 180   180   900 2000 .61 0      - - - - out of memory 0 490    470    7000 0   0      true 2 13     7.3   450   .62 0     
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i unknown 0 220   220   340 2800 .57 0      - - - - error (invalid witness file) 0 .61 .36 41 0   0      error (2) 0 .049 .050 5.5 0    0     
loop-invgen/seq_true-unreach-call_true-termination.i true 1 7.6 7.6 130 98 .53 .0041 - - - - out of memory 0 650    590    7000 0   0      timeout 0 960     780     1400   1.3  0     
loop-invgen/string_concat-noarr_true-unreach-call_false-termination.i unknown 0 2.4 2.4 130 32 .22 0      - - - - error (invalid witness file) 0 .57 .36 40 0   0      error (2) 0 .020 .021 5.7 0    0     
loop-invgen/up_true-unreach-call_true-termination.i true 1 6.1 6.1 130 72 .49 0      - - - - out of memory 0 320    300    7000 0   0      timeout 0 960     780     2900   1.2  0     
loop-invgen/SpamAssassin-loop_true-unreach-call.i.v+cfa-reducer.c unknown 0 9.3 9.4 130 120 .59 0      - - - - error (invalid witness file) 0 .60 .36 40 0   0      error (2) 0 .021 .022 5.6 0    0     
loop-invgen/apache-escape-absolute_true-unreach-call.i.v+cfa-reducer.c unknown 0 2.9 2.9 130 44 .22 0      - - - - error (invalid witness file) 0 .65 .42 42 0   0      error (2) 0 .020 .020 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call.i.p+lhb-reducer.c out of memory 0 720   720   15000 7500 .22 0      - - - - error (invalid witness file) 0 .59 .37 41 0   0      error (2) 0 .021 .023 5.7 0    0     
loop-invgen/apache-get-tag_true-unreach-call.i.p+nlh-reducer.c out of memory 0 820   820   15000 7300 .22 0      - - - - error (invalid witness file) 0 .60 .36 40 0   0      error (2) 0 .021 .021 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call.i.p+sep-reducer.c out of memory 0 760   760   15000 6900 .22 0      - - - - error (invalid witness file) 0 .61 .38 41 0   0      error (2) 0 .019 .020 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call.i.v+lhb-reducer.c unknown 0 14   14   160 170 .22 .83   - - - - error (invalid witness file) 0 .59 .36 40 0   0      error (2) 0 .020 .021 5.6 0    0     
loop-invgen/apache-get-tag_true-unreach-call.i.v+nlh-reducer.c unknown 0 6.8 6.8 130 100 .22 0      - - - - error (invalid witness file) 0 .62 .39 42 0   0      error (2) 0 .021 .021 5.6 0    0     
loop-invgen/id_build_true-unreach-call.i.p+nlh-reducer.c unknown 0 20   20   130 250 .22 0      - - - - error (invalid witness file) 0 .58 .36 40 0   0      error (2) 0 .021 .023 5.6 0    0     
loop-invgen/id_build_true-unreach-call.i.p+sep-reducer.c out of memory 0 590   590   15000 4700 .22 .63   - - - - error (invalid witness file) 0 .59 .37 40 0   0      error (2) 0 .021 .022 5.6 0    0     
loop-invgen/id_build_true-unreach-call.i.v+lhb-reducer.c unknown 0 2.5 2.5 130 30 .22 0      - - - - error (invalid witness file) 0 .59 .36 40 0   0      error (2) 0 .050 .051 5.7 0    0     
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 5.7 5.7 130 84 .48 1.1    - - - - out of memory 0 420    410    7000 0   0      true 2 8.4   4.8   320   .62 0     
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i true 2 260   260   330 3000 .58 0      - - - - timeout 0 900    900    850 0   0      true 2 10     6.2   420   .62 0     
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 4.9 4.9 130 57 .48 0      - - - - true 2 6.0  3.3  290 0   0      true 2 9.3   5.3   330   .62 0     
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 5.6 5.9 130 68 .52 0      - - - - out of memory 0 380    360    7000 0   0      true 2 9.8   6.0   340   .62 0     
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 13   13   160 200 .48 0      - - - - true 2 4.7  2.6  280 0   0      true 2 8.5   5.3   320   .62 0     
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 88   85   450 1300 .52 2.4    - - - - true 2 4.5  2.5  290 0   0      true 2 7.5   4.8   320   .62 0     
loop-lit/ddlm2013_true-unreach-call.i true 2 110   110   210 1300 .50 0      - - - - out of memory 0 370    360    7000 0   0      true 2 12     7.1   400   .62 0     
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 110   110   230 1300 .50 0      - - - - true 2 67    58    800 0   .0041 true 2 79     53     1100   .62 0     
loop-lit/gj2007b_true-unreach-call_true-termination.c.i unknown 0 190   190   270 2900 .54 1.9    - - - - error (invalid witness file) 0 .62 .37 42 0   0      error (2) 0 .027 .028 5.6 0    0     
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 160   160   200 1900 .52 0      - - - - true 2 110    97    1100 0   0      true 2 110     75     1200   .62 0     
loop-lit/gsv2008_true-unreach-call_true-termination.c.i true 2 8.5 8.7 130 120 .52 0      - - - - timeout 0 900    890    3200 0   0      true 2 8.1   4.5   310   .62 0     
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 5.4 5.5 130 60 .52 0      - - - - out of memory 0 440    430    7000 0   0      true 2 9.5   5.8   330   .62 0     
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 5.0 5.2 130 64 .52 2.2    - - - - out of memory 0 390    370    7000 0   0      true 2 12     6.9   420   .62 0     
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true 2 5.4 5.6 130 77 .52 2.2    - - - - out of memory 0 440    430    7000 0   0      true 2 11     7.1   440   .62 0     
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i true 1 7.9 8.0 230 92 .52 0      - - - - out of memory 0 670    660    7000 0   0      timeout 0 960     930     700   .64 .0041
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 7.2 7.2 130 91 1.8  0      timeout 0 97    83    2200 0   0      true -32 7.0   4.2   310   .66 .0041 unknown 0 3.6  2.1  250 0      0      false(unreach-call) 1 .61   .61   20    .049  0      - -
loop-lit/gj2007_true-unreach-call.c.i.p+lhb-reducer.c unknown 0 2.5 2.5 130 41 .22 .63   - - - - error (invalid witness file) 0 .59 .39 40 0   0      error (2) 0 .047 .049 5.5 0    0     
loop-lit/gj2007_true-unreach-call.c.i.p+nlh-reducer.c unknown 0 4.5 4.5 130 67 .22 0      - - - - error (invalid witness file) 0 .61 .38 42 0   0      error (2) 0 .028 .029 5.6 0    0     
loop-lit/gsv2008_true-unreach-call.c.i.p+cfa-reducer.c true 2 11   11   130 190 .50 1.1    - - - - timeout 0 900    890    3200 0   0      true 2 7.5   4.3   320   .62 0     
loop-lit/gsv2008_true-unreach-call.c.i.v+cfa-reducer.c true 2 11   11   130 140 .50 2.1    - - - - timeout 0 900    890    3500 0   0      true 2 7.2   4.1   310   .62 0     
loop-lit/gsv2008_true-unreach-call.c.i.v+lhb-reducer.c true 2 13   13   130 160 .49 0      - - - - timeout 0 900    890    3800 0   0      true 2 8.2   5.1   320   .62 0     
loop-lit/jm2006_true-unreach-call.c.i.v+cfa-reducer.c true 2 7.6 7.8 130 91 .54 0      - - - - out of memory 0 380    370    7000 0   0      true 2 9.9   5.7   340   .62 0     
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 4.6 4.9 130 62 .48 0      - - - - true 2 4.6  2.5  280 0   0      true 2 8.2   5.1   310   .62 0     
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 61   60   330 1000 .48 0      - - - - true 2 4.7  2.6  280 0   0      true 2 8.7   5.5   320   .62 0     
loop-new/count_by_2_true-unreach-call_true-termination.i true 1 4.5 4.6 130 60 .48 0      - - - - out of memory 0 360    350    7000 0   0      timeout 0 960     790     1500   .66 0     
loop-new/count_by_k_true-unreach-call_true-termination.i true 1 9.0 9.1 180 110 .52 2.2    - - - - timeout 0 900    890    2400 0   .0041 timeout 0 960     840     1400   .66 0     
loop-new/count_by_nondet_true-unreach-call_true-termination.i true 1 160   160   270 2000 .56 2.1    - - - - timeout 0 900    890    1900 0   0      timeout 0 960     790     3700   .64 0     
loop-new/gauss_sum_true-unreach-call_true-termination.i true 1 7.9 7.9 180 91 .52 .13   - - - - timeout 0 900    890    5100 0   0      timeout 0 960     830     1600   .63 0     
loop-new/half_true-unreach-call_true-termination.i true 2 200   200   150 2500 .57 0      - - - - timeout 0 910    890    6400 0   0      true 2 14     8.8   470   .62 0     
loop-new/nested_true-unreach-call_true-termination.i true 2 110   120   160 1400 .60 0      - - - - timeout 0 900    880    2000 0   0      true 2 31     20     750   .62 0     
loop-new/gauss_sum_true-unreach-call.i.p+cfa-reducer.c true 1 13   13   190 160 .54 0      - - - - timeout 0 900    890    5100 0   0      timeout 0 960     890     1000   .81 0     
loop-new/gauss_sum_true-unreach-call.i.p+lhb-reducer.c true 1 49   49   180 680 .56 1.7    - - - - timeout 0 900    890    5100 0   0      timeout 0 960     860     950   .64 0     
loop-new/gauss_sum_true-unreach-call.i.v+cfa-reducer.c true 1 13   13   190 150 .54 0      - - - - timeout 0 900    890    5200 0   0      timeout 0 960     880     740   .63 0     
loop-industry-pattern/aiob_1_true-unreach-call.c unknown 0 2.4 2.4 130 31 .22 .68   - - - - error (invalid witness file) 0 .62 .40 40 0   0      error (2) 0 .029 .031 5.7 0    0     
loop-industry-pattern/aiob_2_true-unreach-call.c unknown 0 2.4 2.4 130 34 .22 0      - - - - error (invalid witness file) 0 .58 .36 41 0   0      error (2) 0 .019 .020 5.6 0    0     
loop-industry-pattern/aiob_3_true-unreach-call.c unknown 0 2.4 2.4 130 36 .22 0      - - - - error (invalid witness file) 0 .68 .45 42 0   0      error (2) 0 .022 .022 5.6 0    0     
loop-industry-pattern/aiob_4_true-unreach-call.c unknown 0 2.4 2.4 130 35 .22 0      - - - - error (invalid witness file) 0 .61 .38 41 0   0      error (2) 0 .021 .021 5.6 0    0     
loop-industry-pattern/aiob_4_true-unreach-call.c.v+cfa-reducer.c unknown 0 2.4 2.4 130 31 .22 0      - - - - error (invalid witness file) 0 .61 .37 42 0   0      error (2) 0 .028 .031 5.6 0    0     
loop-industry-pattern/aiob_4_true-unreach-call.c.v+lh-reducer.c unknown 0 2.4 2.4 130 32 .22 .58   - - - - error (invalid witness file) 0 .63 .40 40 0   0      error (2) 0 .021 .022 5.6 0    0     
loop-industry-pattern/aiob_4_true-unreach-call.c.v+lhb-reducer.c unknown 0 2.4 2.4 130 40 .22 0      - - - - error (invalid witness file) 0 .68 .42 41 0   0      error (2) 0 .026 .030 5.7 0    0     
loop-industry-pattern/aiob_4_true-unreach-call.c.v+nlh-reducer.c unknown 0 2.4 2.4 130 35 .22 .48   - - - - error (invalid witness file) 0 .62 .37 41 0   0      error (2) 0 .050 .051 5.5 0    0     
loop-industry-pattern/mod3_true-unreach-call.c true 2 27   28   230 340 .48 0      - - - - true 2 6.4  4.4  320 0   0      true 2 8.5   5.1   310   .62 0     
loop-industry-pattern/mod3_true-unreach-call.c.v+cfa-reducer.c error (1) 0 4.6 4.6 130 57 .46 0      - - - - error (invalid witness file) 0 .57 .36 40 0   0      error (2) 0 .020 .021 5.6 0    0     
loop-industry-pattern/mod3_true-unreach-call.c.v+lhb-reducer.c unknown 0 2.5 2.5 130 32 .22 0      - - - - error (invalid witness file) 0 .62 .39 42 0   0      error (2) 0 .046 .047 5.5 0    0     
loop-industry-pattern/mod3_true-unreach-call.c.v+sep-reducer.c unknown 0 2.5 2.5 130 39 .22 0      - - - - error (invalid witness file) 0 .59 .37 40 0   0      error (2) 0 .020 .021 5.6 0    0     
loop-industry-pattern/nested_true-unreach-call.c timeout 0 900   900   230 13000 .26 0      - - - - error (invalid witness file) 0 .59 .35 40 0   0      error (2) 0 .052 .054 5.5 0    0     
loop-industry-pattern/ofuf_1_true-unreach-call.c unknown 0 2.4 2.4 130 35 .22 .58   - - - - error (invalid witness file) 0 .61 .37 41 0   0      error (2) 0 .021 .033 5.6 0    0     
loop-industry-pattern/ofuf_2_true-unreach-call.c unknown 0 2.4 2.4 130 33 .22 .012  - - - - error (invalid witness file) 0 .59 .36 41 0   0      error (2) 0 .026 .027 5.6 0    0     
loop-industry-pattern/ofuf_3_true-unreach-call.c unknown 0 2.4 2.4 130 36 .22 0      - - - - error (invalid witness file) 0 .63 .41 41 0   0      error (2) 0 .020 .021 5.6 0    0     
loop-industry-pattern/ofuf_4_true-unreach-call.c unknown 0 2.4 2.4 130 35 .22 .58   - - - - error (invalid witness file) 0 .74 .45 41 0   0      error (2) 0 .020 .021 5.6 0    0     
loop-industry-pattern/ofuf_5_true-unreach-call.c unknown 0 2.4 2.4 130 30 .22 0      - - - - error (invalid witness file) 0 .60 .36 41 0   0      error (2) 0 .024 .024 5.6 0    0     
loops/heavy_true-unreach-call.c unknown 0 2.4 2.4 130 39 .22 0      - - - - error (invalid witness file) 0 .65 .40 42 0   0      error (2) 0 .026 .027 5.6 0    0     
loops/compact_false-unreach-call.c unknown 0 2.4 2.4 130 32 .22 .62   error (invalid witness file) 0 .62 .39 41 0   0      error (2) 0 .020 .021 5.6 0    0      error (invalid witness file) 0 .93 .60 47 0      0      error (invalid witness file) 0 .0050 .0083 .40 0      0      - -
loops/heavy_false-unreach-call.c unknown 0 2.4 2.4 130 30 .22 .0041 error (invalid witness file) 0 .61 .38 41 0   0      error (2) 0 .021 .021 5.6 0    0      error (invalid witness file) 0 .94 .60 47 0      0      error (invalid witness file) 0 .0045 .0054 .41 0      0      - -
loops-crafted-1/Mono1_false-unreach-call1.c false(unreach-call) 1 5.9 6.0 130 82 1.4  0      true -32 5.6  3.0  260 0   0      out of memory 0 77     47     7000   .68 .0041 false(unreach-call) 1 4.9  2.8  260 0      0      false(unreach-call) 1 .73   .74   23    .045  0      - -
loops-crafted-1/Mono3_false-unreach-call1.c false(unreach-call) 1 5.8 5.8 130 93 1.4  0      timeout 0 98    85    1900 0   0      true -32 7.7   4.8   310   .66 0      false(unreach-call) 1 3.5  2.1  250 0      0      false(unreach-call) 1 .60   .59   20    .045  0      - -
loops-crafted-1/Mono4_false-unreach-call1.c false(unreach-call) 1 5.8 5.8 130 73 1.4  0      timeout 0 98    88    1900 0   0      true -32 7.1   4.1   310   .62 0      false(unreach-call) 1 3.5  2.0  250 0      0      false(unreach-call) 1 .57   .57   20    .045  .0041 - -
loops-crafted-1/Mono5_false-unreach-call1.c false(unreach-call) 1 64   63   11000 870 .95 .63   timeout 0 97    86    1900 0   0      true -32 7.7   4.8   310   .66 0      false(unreach-call) 1 3.4  2.0  250 0      0      false(unreach-call) 1 .61   .61   20    .045  0      - -
loops-crafted-1/Mono6_false-unreach-call1.c false(unreach-call) 1 63   62   11000 840 .95 0      timeout 0 98    87    1900 0   0      true -32 8.5   4.9   330   .66 0      false(unreach-call) 1 3.4  2.0  250 0      0      false(unreach-call) 1 .62   .62   20    .045  0      - -
loops-crafted-1/nested3_false-unreach-call.c unknown 0 65   66   170 850 .55 0      error (invalid witness file) 0 .63 .41 41 0   0      error (2) 0 .021 .022 5.6 0    0      error (invalid witness file) 0 .90 .59 46 0      0      error (invalid witness file) 0 .0036 .0047 .53 0      0      - -
loops-crafted-1/nested5_false-unreach-call.c unknown 0 190   190   310 2200 .58 .13   error (invalid witness file) 0 .58 .37 40 0   0      error (2) 0 .020 .021 5.6 0    0      error (invalid witness file) 0 .90 .58 47 0      0      error (invalid witness file) 0 .0058 .0074 .53 0      0      - -
loops-crafted-1/Mono1_true-unreach-call1.c unknown 0 160   170   280 2000 .52 0      - - - - error (invalid witness file) 0 .59 .36 41 0   0      error (2) 0 .047 .048 5.5 0    0     
loops-crafted-1/nested3_true-unreach-call.c true 1 16   16   150 220 .51 .13   - - - - timeout 0 900    880    3400 0   0      timeout 0 960     920     1000   1.0  0     
loops-crafted-1/nested5_true-unreach-call.c true 2 17   17   190 230 .47 1.7    - - - - true 2 4.7  2.6  280 0   0      true 2 19     15     370   .62 0     
loop-invariants/bin-suffix-5_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c true 2 4.7 4.7 130 55 .48 0      - - - - out of memory 0 390    380    7000 0   0      true 2 13     8.0   290   .68 0     
loop-invariants/const_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c true 2 110   110   200 1300 .52 1.1    - - - - timeout 0 900    890    5400 0   0      true 2 7.5   4.3   310   .62 .0041
loop-invariants/eq1_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c true 2 57   57   210 700 .49 1.1    - - - - timeout 0 910    910    790 0   0      true 2 7.6   4.6   310   .62 0     
loop-invariants/eq2_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c true 2 4.7 4.7 130 64 .48 0      - - - - out of memory 0 410    400    7000 0   0      true 2 8.1   4.8   310   .62 0     
loop-invariants/even_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c true 2 4.5 4.5 130 59 .48 0      - - - - out of memory 0 510    490    7000 0   0      true 2 7.1   4.0   310   .62 0     
loop-invariants/mod4_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c true 2 4.5 4.5 130 60 .48 0      - - - - out of memory 0 530    520    7000 0   0      true 2 7.5   4.7   310   .62 0     
loop-invariants/odd_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c true 2 4.6 4.8 130 58 .48 2.4    - - - - out of memory 0 580    560    7000 0   0      true 2 9.3   6.2   320   .62 0     
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 2.7 2.7 130 35 .33 1.2    false(unreach-call) 1 4.1  2.2  260 0   .029  false(unreach-call) 1 7.8   4.8   310   .66 0      unknown 0 3.7  2.2  250 0      0      true -32 .60   .60   20    .049  0      - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 2.6 2.6 130 37 .30 .0041 false(unreach-call) 1 4.8  2.6  270 0   0      false(unreach-call) 1 12     6.8   480   .62 0      unknown 0 3.8  2.2  240 0      0      true -32 .58   .58   21    .049  0      - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 2.6 2.6 130 34 .29 .11   true -32 3.6  2.0  250 0   0      true -32 6.2   3.5   300   .66 0      unknown 0 3.5  2.0  250 0      0      true -32 .62   .62   20    .049  0      - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 2.6 2.6 130 33 .30 0      false(unreach-call) 1 3.7  2.1  250 0   0      false(unreach-call) 1 6.9   3.9   300   .66 0      unknown 0 3.6  2.1  240 0      0      false(unreach-call) 1 .60   .60   20    .049  0      - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 2.6 2.6 130 34 .29 1.2    false(unreach-call) 1 4.5  2.5  270 0   0      false(unreach-call) 1 26     14     800   .66 0      unknown 0 3.9  2.3  250 0      0      true -32 .58   .60   21    .049  0      - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 2.6 2.6 130 40 .29 .54   false(unreach-call) 1 6.7  3.6  300 0   0      timeout 0 98     70     5000   1.5  .0041 unknown 0 4.9  2.7  260 0      0      true -32 .59   .59   22    .049  0      - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 2.6 2.6 130 34 .29 0      false(unreach-call) 1 3.6  2.0  250 0   0      false(unreach-call) 1 6.8   3.8   300   .66 0      unknown 0 3.6  2.1  250 0      0      true -32 .59   .59   20    .049  .0041 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c unknown 0 110   110   330 1300 .45 0      - - - - error (invalid witness file) 0 .61 .37 40 0   0      error (2) 0 .039 .039 5.5 0    0     
recursive/Ackermann03_true-unreach-call_true-no-overflow.c unknown 0 110   110   690 1100 .39 1.2    - - - - error (invalid witness file) 0 .64 .40 42 0   0      error (2) 0 .023 .034 5.5 0    0     
recursive/Ackermann04_true-unreach-call_true-no-overflow.c unknown 0 110   110   830 910 .39 2.3    - - - - error (invalid witness file) 0 .60 .38 42 0   0      error (2) 0 .020 .021 5.6 0    0     
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 110   110   310 1600 .39 0      - - - - error (invalid witness file) 0 .61 .39 42 0   0      error (2) 0 .046 .052 5.7 0    0     
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c true 2 57   57   310 690 .57 2.7    - - - - error (recursion) 0 4.0  2.2  250 0   0      true 2 410     320     2200   .62 .0041
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c true 1 56   56   190 660 .63 2.7    - - - - error (recursion) 0 3.8  2.1  250 0   0      timeout 0 960     810     1300   .63 .0041
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c true 2 36   36   210 530 .59 .18   - - - - error (recursion) 0 3.5  2.0  250 0   0      true 2 14     8.7   460   .62 0     
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 4.2 4.2 130 59 .52 1.9    - - - - error (recursion) 0 3.8  2.1  260 0   0      true 2 37     23     1700   .66 0     
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c true 2 19   19   230 250 .65 .0041 - - - - error (recursion) 0 3.8  2.1  260 0   0      true 2 28     16     820   .62 0     
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 6.8 6.9 130 89 .57 1.9    - - - - error (recursion) 0 3.8  2.0  250 0   0      true 2 9.7   6.0   330   .62 0     
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c true 1 78   78   220 1000 .67 2.2    - - - - error (recursion) 0 3.8  2.1  250 0   0      timeout 0 960     820     1100   .63 0     
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c unknown 0 4.4 4.4 130 60 .31 .18   - - - - error (invalid witness file) 0 .61 .38 42 0   0      error (2) 0 .045 .046 5.4 0    0     
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 12   12   150 190 .66 0      - - - - error (recursion) 0 3.4  1.9  250 0   0      true 2 10     6.3   360   .62 0     
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 110   110   730 1400 .66 0      - - - - error (recursion) 0 3.5  2.0  250 0   0      timeout 0 960     820     890   .63 0     
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 4.7 4.7 130 70 .46 .27   - - - - error (invalid witness file) 0 .60 .37 41 0   0      error (2) 0 .025 .037 5.5 0    0     
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 5.7 5.7 130 78 .63 .11   - - - - error (recursion) 0 3.4  1.9  250 0   0      true 2 6.9   4.0   310   .62 0     
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 5.9 5.9 130 77 .63 .11   - - - - error (recursion) 0 3.6  2.0  250 0   .0041 true 2 12     7.6   460   .62 0     
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 31 .29 0      true -32 3.5  1.9  250 0   0      false(unreach-call) 1 6.9   4.3   300   .66 0      false(unreach-call) 1 3.4  2.0  240 0      .0041 false(unreach-call) 1 .59   .59   20    .045  0      - -
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 34 .29 .58   true -32 3.4  1.9  250 0   0      false(unreach-call) 1 6.2   4.0   290   .66 0      false(unreach-call) 1 3.7  2.1  250 0      0      false(unreach-call) 1 .57   .57   20    .045  0      - -
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 2.7 2.7 130 41 .29 .11   false(unreach-call) 1 9.2  5.0  410 0   0      timeout 0 96     64     5200   1.4  0      false(unreach-call) 1 5.3  2.9  260 0      0      false(unreach-call) 1 .63   .63   25    .049  0      - -
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 5.0 5.0 420 54 .29 .28   false(unreach-call) 1 40    23    1500 0   0      timeout 0 97     64     7000   .63 0      false(unreach-call) 1 17    8.9  470 0      0      false(unreach-call) 1 1.2    1.3    77    .049  0      - -
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 29   29   4000 240 .29 0      timeout 0 96    67    2600 0   0      out of memory 0 88     56     7000   .66 0      timeout 0 97    77    2500 0      0      false(unreach-call) 1 8.1    8.1    680    .049  0      - -
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 5.6 5.6 1200 86 .29 .16   timeout 0 98    65    4000 0   .0041 true -32 7.4   4.2   310   .62 0      false(unreach-call) 1 3.4  2.0  240 0      0      false(unreach-call) 1 .59   .59   20    .049  0      - -
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 2.8 2.8 130 36 .30 0      false(unreach-call) 1 8.4  4.6  370 0   0      timeout 0 98     64     6000   1.5  0      false(unreach-call) 1 5.1  2.9  260 0      0      false(unreach-call) 1 .65   .66   25    .049  0      - -
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 5.0 5.0 420 52 .30 .11   false(unreach-call) 1 29    18    1300 0   0      out of memory 0 76     49     7000   .70 .0041 false(unreach-call) 1 13    6.9  350 0      0      false(unreach-call) 1 1.2    1.2    77    .049  0      - -
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 29   29   4000 280 .30 1.3    out of memory 0 82    53    7000 0   0      timeout 0 94     54     7000   1.5  0      timeout 0 97    79    2400 .020  0      false(unreach-call) 1 8.2    8.2    680    .049  0      - -
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 5.7 5.6 1200 75 .30 .11   timeout 0 97    61    4000 0   .012  true -32 7.5   4.3   310   .66 0      false(unreach-call) 1 3.5  2.1  250 0      0      false(unreach-call) 1 .60   .60   20    .049  0      - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 34 .30 .73   false(unreach-call) 1 3.6  2.0  250 0   0      false(unreach-call) 1 7.3   4.5   310   .66 0      false(unreach-call) 1 3.9  2.2  250 0      0      false(unreach-call) 1 .59   .59   20    .049  0      - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 37 .30 0      false(unreach-call) 1 4.3  2.4  260 0   0      false(unreach-call) 1 14     8.5   460   .66 0      false(unreach-call) 1 3.6  2.1  250 0      0      false(unreach-call) 1 .63   .65   21    .049  0      - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 33 .30 .11   false(unreach-call) 1 4.6  2.5  270 0   0      false(unreach-call) 1 30     16     890   .62 0      false(unreach-call) 1 3.8  2.2  250 0      0      false(unreach-call) 1 .63   .65   21    .049  0      - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 35 .30 0      false(unreach-call) 1 4.9  2.7  270 0   0      false(unreach-call) 1 47     26     2000   .62 0      false(unreach-call) 1 3.9  2.2  250 0      0      false(unreach-call) 1 .59   .58   21    .049  0      - -
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 32 .30 .36   false(unreach-call) 1 6.2  3.3  300 0   0      timeout 0 97     67     4800   1.5  .0041 false(unreach-call) 1 4.8  2.6  260 0      0      false(unreach-call) 1 .59   .59   22    .049  0      - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 35 .29 0      false(unreach-call) 1 4.7  2.6  270 0   0      false(unreach-call) 1 21     12     760   .66 0      false(unreach-call) 1 3.7  2.2  240 0      0      false(unreach-call) 1 .57   .57   21    .049  0      - -
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 37 .29 .11   false(unreach-call) 1 5.7  3.1  280 0   .12   timeout 0 96     67     3500   .66 0      false(unreach-call) 1 4.3  2.4  250 0      0      false(unreach-call) 1 .59   .59   22    .049  0      - -
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 2.7 2.7 130 38 .31 .25   false(unreach-call) 1 4.1  2.3  260 0   0      true -32 7.4   4.6   310   .66 0      unknown 0 3.5  2.0  240 0      0      true -32 .63   .64   20    .049  0      - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 34 .29 0      false(unreach-call) 1 3.9  2.2  260 0   0      false(unreach-call) 1 7.0   4.0   300   .66 0      false(unreach-call) 1 3.5  2.0  240 0      0      false(unreach-call) 1 .61   .61   20    .049  0      - -
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 2.6 2.6 130 32 .30 0      false(unreach-call) 1 4.0  2.2  260 0   0      true -32 7.5   4.5   310   .66 0      unknown 0 3.5  2.1  250 0      0      true -32 .58   .58   20    .049  0      - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 33 .29 0      false(unreach-call) 1 4.4  2.4  270 0   0      false(unreach-call) 1 8.6   5.2   350   .66 0      false(unreach-call) 1 3.8  2.2  250 0      0      false(unreach-call) 1 .60   .61   20    .045  .0041 - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 31 .29 0      false(unreach-call) 1 4.9  2.7  270 0   0      false(unreach-call) 1 12     6.9   520   .66 0      false(unreach-call) 1 4.0  2.3  250 0      0      false(unreach-call) 1 .59   .59   22    .045  0      - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 37 .29 .73   false(unreach-call) 1 5.3  2.8  270 0   0      false(unreach-call) 1 16     8.4   750   .66 .0041 false(unreach-call) 1 4.2  2.4  250 0      0      false(unreach-call) 1 .58   .58   21    .045  0      - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 35 .29 .33   false(unreach-call) 1 5.8  3.2  270 0   0      false(unreach-call) 1 21     12     830   .62 0      false(unreach-call) 1 4.5  2.6  250 0      0      false(unreach-call) 1 .61   .62   21    .045  0      - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 36 .29 .73   false(unreach-call) 1 4.4  2.4  260 0   0      false(unreach-call) 1 7.5   4.2   300   .66 0      false(unreach-call) 1 3.7  2.2  250 0      0      false(unreach-call) 1 .59   .59   20    .045  0      - -
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 3.6 3.7 200 41 .32 .95   exception 0 6.8  3.6  270 0   0      out of memory 0 89     63     7000   .63 0      timeout 0 6.3  130    260 .84   .0041 true -32 .83   .83   41    .049  0      - -
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 2.7 2.7 130 35 .32 1.1    false(unreach-call) 1 16    8.2  510 0   0      timeout 0 96     63     7000   .66 0      unknown 0 9.2  5.0  370 0      0      true -32 .61   .61   22    .049  .0041 - -
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 2.7 2.7 130 32 .32 .25   false(unreach-call) 1 4.8  2.6  270 0   0      false(unreach-call) 1 9.7   5.2   370   .66 0      unknown 0 3.9  2.3  250 0      0      true -32 .60   .60   21    .049  0      - -
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 2.8 2.8 130 34 .32 .28   false(unreach-call) 1 32    21    1100 0   0      timeout 0 98     65     6200   .66 0      unknown 0 16    8.7  490 0      0      true -32 .62   .62   24    .049  0      - -
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 2.7 2.7 130 34 .32 .11   false(unreach-call) 1 5.3  2.9  270 0   0      false(unreach-call) 1 16     8.7   760   .66 0      unknown 0 4.2  2.4  250 0      0      true -32 .61   .64   21    .049  .0041 - -
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 2.7 2.7 130 35 .32 0      false(unreach-call) 1 3.9  2.2  260 0   0      false(unreach-call) 1 7.1   4.0   300   .66 0      unknown 0 3.5  2.1  250 0      0      true -32 .57   .57   20    .049  .0041 - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 40 .29 0      false(unreach-call) 1 4.5  2.5  270 0   .016  false(unreach-call) 1 8.2   5.1   320   .66 0      false(unreach-call) 1 3.8  2.2  250 0      0      false(unreach-call) 1 .59   .60   21    .045  0      - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 30 .29 .40   false(unreach-call) 1 5.0  2.7  270 0   0      false(unreach-call) 1 11     6.6   520   .66 0      false(unreach-call) 1 4.3  2.5  250 0      0      false(unreach-call) 1 .59   .59   21    .045  0      - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 32 .29 0      false(unreach-call) 1 5.4  2.9  280 0   .0041 false(unreach-call) 1 15     8.5   630   .66 0      false(unreach-call) 1 4.0  2.3  250 0      0      false(unreach-call) 1 .57   .57   21    .045  0      - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 40 .29 .11   false(unreach-call) 1 5.6  3.1  280 0   0      false(unreach-call) 1 17     9.9   780   .62 0      false(unreach-call) 1 4.2  2.4  250 0      0      false(unreach-call) 1 .57   .57   21    .045  0      - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 2.6 2.6 130 29 .29 .74   false(unreach-call) 1 3.8  2.1  260 0   0      false(unreach-call) 1 7.7   4.4   310   .66 0      false(unreach-call) 1 3.9  2.3  250 0      0      false(unreach-call) 1 .59   .62   20    .045  .0041 - -
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 2.9 2.9 130 36 .29 .11   exception 0 6.4  3.5  270 0   0      timeout 0 97     64     6600   .66 0      timeout 0 5.6  130    260 .0041 0      false(unreach-call) 1 .67   .67   30    .049  0      - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 3.8 3.8 130 47 .52 0      - - - - true 2 3.4  1.9  250 0   0      true 2 7.2   4.1   310   .62 0     
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 3.7 3.7 130 55 .52 .11   - - - - true 2 3.7  2.1  250 0   .0041 true 2 6.7   4.3   310   .62 0     
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 8.1 8.1 190 110 .52 .24   - - - - error (recursion) 0 3.6  1.9  250 0   0      true 2 38     24     2200   .62 0     
recursive-simple/fibo_15_true-unreach-call.c true 1 8.1 8.1 190 110 .52 .11   - - - - error (recursion) 0 3.4  1.9  250 0   0      timeout 0 960     890     6000   1.0  0     
recursive-simple/fibo_20_true-unreach-call.c true 1 13   13   200 180 .52 1.7    - - - - error (recursion) 0 3.4  1.9  250 0   0      out of memory 0 700     650     7000   .63 0     
recursive-simple/fibo_25_true-unreach-call.c true 1 15   15   210 190 .52 1.1    - - - - error (recursion) 0 3.7  2.0  250 0   0      timeout 0 900     850     7000   .63 0     
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 8.2 8.2 190 120 .53 0      - - - - error (recursion) 0 4.0  2.2  250 0   0      true 2 85     55     3800   .62 0     
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 8.3 8.3 200 110 .53 .25   - - - - error (recursion) 0 3.8  2.1  250 0   0      timeout 0 960     900     5400   1.0  0     
recursive-simple/fibo_2calls_20_true-unreach-call.c true 1 10   10   200 130 .53 0      - - - - error (recursion) 0 3.5  2.0  250 0   0      timeout 0 960     900     5300   1.0  0     
recursive-simple/fibo_2calls_25_true-unreach-call.c true 1 6.9 7.0 200 81 .53 1.9    - - - - error (recursion) 0 3.4  1.9  250 0   0      out of memory 0 580     530     7000   .63 0     
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 7.0 7.0 170 84 .53 .25   - - - - true 2 3.4  1.9  250 0   0      true 2 11     6.8   390   .62 0     
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 8.2 8.2 190 120 .53 .11   - - - - error (recursion) 0 3.9  2.1  250 0   0      true 2 15     9.7   540   .62 0     
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 8.1 8.1 190 120 .53 0      - - - - error (recursion) 0 3.5  1.9  250 0   0      true 2 21     13     510   .62 0     
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 8.3 8.3 190 100 .53 0      - - - - error (recursion) 0 3.5  1.9  250 0   0      true 2 26     16     700   .62 0     
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 8.2 8.2 190 99 .53 0      - - - - error (recursion) 0 4.0  2.2  260 0   0      true 2 50     32     1300   .62 0     
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 8.1 8.1 190 92 .52 0      - - - - error (recursion) 0 3.4  1.9  250 0   0      true 2 16     9.6   580   .62 .0041
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 8.0 8.0 190 110 .52 .0041 - - - - error (recursion) 0 3.5  2.0  250 0   0      true 2 21     13     550   .62 0     
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 9.0 9.0 200 110 .84 0      - - - - error (recursion) 0 3.9  2.2  250 0   0      true 2 12     7.5   460   .10 0     
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 8.8 8.9 200 110 .84 2.6    - - - - error (recursion) 0 3.6  2.0  250 0   0      true 2 13     8.2   460   .62 0     
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 9.0 9.0 200 110 .84 1.9    - - - - error (recursion) 0 4.2  2.4  250 0   .0041 true 2 13     8.3   520   .62 0     
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 6.9 6.9 160 87 .52 0      - - - - error (recursion) 0 3.4  1.9  250 0   0      true 2 14     8.6   500   .62 0     
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 9.0 9.0 200 120 .79 3.0    - - - - error (recursion) 0 3.6  2.0  250 0   0      true 2 11     6.9   380   .62 0     
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 7.0 7.0 150 90 .79 .049  - - - - error (recursion) 0 3.7  2.1  250 0   0      true 2 8.5   4.8   320   .62 0     
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 6.9 6.9 150 100 .79 .21   - - - - error (recursion) 0 3.5  2.0  250 0   0      true 2 7.8   4.9   310   .62 0     
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 8.2 8.2 200 100 .52 2.2    - - - - error (recursion) 0 3.5  1.9  250 0   0      true 2 16     9.9   480   .62 0     
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 8.9 8.9 200 130 .52 .11   - - - - error (recursion) 0 3.4  1.9  260 0   0      true 2 21     13     630   .62 0     
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 9.7 9.7 200 140 .52 0      - - - - error (recursion) 0 3.4  1.9  250 0   0      true 2 28     17     700   .62 0     
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 11   11   200 160 .52 .11   - - - - error (recursion) 0 3.9  2.2  250 0   0      true 2 35     23     730   .62 0     
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 6.8 6.8 160 98 .52 .18   - - - - error (recursion) 0 4.2  2.4  250 0   .0041 true 2 11     6.9   440   .62 0     
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 6.7 6.7 210 78 .52 .19   - - - - error (recursion) 0 3.5  1.9  250 0   0      true 2 19     12     490   .62 0     
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 7.0 7.1 210 84 .52 0      - - - - error (recursion) 0 3.5  2.0  250 0   0      true 2 26     16     650   .62 .0041
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 55   55   300 600 .52 0      - - - - error (recursion) 0 3.3  1.9  250 0   0      true 2 35     22     580   .62 0     
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 55   55   300 690 .52 .32   - - - - error (recursion) 0 3.9  2.1  250 0   .0041 true 2 49     32     690   .62 0     
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 5.2 5.2 130 59 .52 .18   - - - - error (recursion) 0 3.5  2.0  250 0   0      true 2 11     6.4   380   .62 0     
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 81   81   220 950 .53 1.9    - - - - error (recursion) 0 3.8  2.1  250 0   0      true 2 10     6.1   340   .62 0     
sv-benchmarks/c/ status score cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 535 680 32000 32000 370000 400000 340 260   147 -532 2500 2000 75000 0   .20   147 -1792 2900 1800 190000 78 .082  147 -21 810   780   36000 .86 .020  147 -846 96 96 4600 5.4 .045 388 78 180000 180000 1000000 0   .13  388 200 200000 190000 390000 230 .53 
    correct results 372 646 13000 13000 130000 160000 240 180   44 44 350 210 16000 0   .17   32 32 410 230 17000 21 .0082 43 43 190   110   11000 0    .0082 82 82 76 76 3800 3.9 .025 39 78 1400 1200 17000 0   .012 100 200 2700 2000 53000 62 .020
        correct true 274 548 12000 13000 78000 150000 140 160   0 0 0 0 39 78 1400 1200 17000 0   .012 100 200 2700 2000 53000 62 .020
        correct false 98 98 750 750 47000 9900 99 22   44 44 350 210 16000 0   .17   32 32 410 230 17000 21 .0082 43 43 190   110   11000 0    .0082 82 82 76 76 3800 3.9 .025 0 0
    correct-unconfimed results 47 34 1300 1300 9400 16000 38 31   0 0 0 0 0 0
        correct-unconfirmed true 34 34 1200 1200 6900 14000 18 28   0 0 0 0 0 0
        correct-unconfirmed false 13 0 100 100 2500 1400 20 3.3 0 0 0 0 0 0
    incorrect results 0 18 -576 120 65 6600 0   .0041 57 -1824 590 340 27000 37 .020  2 -64 7.4 4.3 490 0    0      29 -928 19 19 800 1.4 .020 0 0
        incorrect true 0 18 -576 120 65 6600 0   .0041 57 -1824 590 340 27000 37 .020  2 -64 7.4 4.3 490 0    0      29 -928 19 19 800 1.4 .020 0 0
        incorrect false 0 0 0 0 0 0 0
Run set viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive] cpa-seq-validate-violation-witnesses-viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive] uautomizer-validate-violation-witnesses-viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive] cpa-witness2test-validate-violation-witnesses-viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive] fshell-witness2test-validate-violation-witnesses-viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive] cpa-seq-validate-correctness-witnesses-viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive] uautomizer-validate-correctness-witnesses-viap.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-Recursive]