examples/tests/rac.oracle

   1
   2 * Local
   3 ** Local.test1 ()
   4 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
   5 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 7, characters 13-19
   6 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 8, characters 13-37
   7 <rac:check_term_result>Assertion failed at "examples/tests/rac.mlw", line 9, characters 13-18
   8                        - Term: x = 0
   9                        - Variables: x -> 1
  10 Assertion failed at "examples/tests/rac.mlw", line 9, characters 13-18
  11 - Term: x = 0
  12 - Variables: x -> 1
  13 ** Local.test2 ()
  14 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
  15 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 14, characters 16-18
  16 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 14, characters 16-18
  17 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 14, characters 16-18
  18 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 15, characters 13-20
  19 result: () = ()
  20 globals: <none>
  21 ** Local.test3 ()
  22 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
  23 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 18, characters 16-17
  24 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 18, characters 16-17
  25 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 19, characters 13-19
  26 <rac:check_term_result>Assertion failed at "examples/tests/rac.mlw", line 20, characters 13-19
  27                        - Term: x.contents > 10
  28                        - Variables: x -> {contents= 1}
  29 Assertion failed at "examples/tests/rac.mlw", line 20, characters 13-19
  30 - Term: x.contents > 10
  31 - Variables: x -> {contents= 1}
  32 ** Local.test4 ()
  33 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
  34 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 23, characters 13-28
  35 result: () = ()
  36 globals: <none>
  37 ** Local.test5 ()
  38 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
  39 <rac:check_term_result>Postcondition of `True` is ok at "examples/tests/rac.mlw", line 26, characters 12-16
  40 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 27, characters 13-21
  41 result: () = ()
  42 globals: <none>
  43
  44 * Global
  45 ** Global.test1 ()
  46 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 34, characters 12-17
  47 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 34, characters 12-17
  48 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 41, characters 14-16
  49 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 41, characters 14-16
  50 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
  51 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 37, characters 13-18
  52 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 38, characters 9-10
  53 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 38, characters 9-14
  54 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 39, characters 13-18
  55 result: () = ()
  56 globals: x -> {contents= 1}, y -> {contents= 42}
  57 ** Global.test2 ()
  58 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 34, characters 12-17
  59 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 34, characters 12-17
  60 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 41, characters 14-16
  61 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 41, characters 14-16
  62 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
  63 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 44, characters 13-19
  64 result: () = ()
  65 globals: x -> {contents= 0}, y -> {contents= 42}
  66
  67 * Functions
  68 ** Functions.test1 ()
  69 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
  70 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
  71 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
  72 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 57, characters 13-27
  73 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 58, characters 13-30
  74 <rac:check_term_result>Assertion failed at "examples/tests/rac.mlw", line 59, characters 13-35
  75                        - Term: f1_aux 0 = ((f1_aux' @ 0) @ 1)
  76                        - Variables: <none>
  77 Assertion failed at "examples/tests/rac.mlw", line 59, characters 13-35
  78 - Term: f1_aux 0 = ((f1_aux' @ 0) @ 1)
  79 - Variables: <none>
  80 ** Functions.test2 ()
  81 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
  82 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
  83 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
  84 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 63, characters 13-29
  85 result: () = ()
  86 globals: x -> {contents= 0}
  87 ** Functions.test3a ()
  88 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
  89 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
  90 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 7-9
  91 <rac:check_term_result>Precondition of `test3_aux` failed at "examples/tests/rac.mlw", line 71, characters 4-15
  92                        - Defined at "examples/tests/rac.mlw", line 66, characters 15-20
  93                        - Term: y > 0
  94                        - Variables: y -> 0
  95 Precondition of `test3_aux` failed at "examples/tests/rac.mlw", line 71, characters 4-15
  96 - Defined at "examples/tests/rac.mlw", line 66, characters 15-20
  97 - Term: y > 0
  98 - Variables: y -> 0
  99 ** Functions.test3b ()
 100 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
 101 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
 102 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 7-9
 103 <rac:check_term_result>Precondition of `test3_aux` is ok at "examples/tests/rac.mlw", line 74, characters 12-23
 104                        - Defined at "examples/tests/rac.mlw", line 66, characters 15-20
 105 <rac:check_term_result>Postcondition of `test3_aux` is ok at "examples/tests/rac.mlw", line 74, characters 12-23
 106                        - Defined at "examples/tests/rac.mlw", line 67, characters 14-24
 107 <rac:check_term_result>Precondition of `test3_aux` is ok at "examples/tests/rac.mlw", line 75, characters 4-15
 108                        - Defined at "examples/tests/rac.mlw", line 66, characters 15-20
 109 <rac:check_term_result>Postcondition of `test3_aux` failed at "examples/tests/rac.mlw", line 75, characters 4-15
 110                        - Defined at "examples/tests/rac.mlw", line 67, characters 14-24
 111                        - Term: result = 1
 112                        - Variables: result -> 2
 113 Postcondition of `test3_aux` failed at "examples/tests/rac.mlw", line 75, characters 4-15
 114 - Defined at "examples/tests/rac.mlw", line 67, characters 14-24
 115 - Term: result = 1
 116 - Variables: result -> 2
 117 ** Functions.test4 ()
 118 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
 119 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
 120 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 121 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 85, characters 18-20
 122 <rac:check_term_result>Exceptional postcondition of `test4_aux` failed at "examples/tests/rac.mlw", line 85, characters 8-20
 123                        - Defined at "examples/tests/rac.mlw", line 80, characters 20-25
 124                        - Term: j = x.contents
 125                        - Variables: j -> 42, x -> {contents= 1}
 126 Exceptional postcondition of `test4_aux` failed at "examples/tests/rac.mlw", line 85, characters 8-20
 127 - Defined at "examples/tests/rac.mlw", line 80, characters 20-25
 128 - Term: j = x.contents
 129 - Variables: j -> 42, x -> {contents= 1}
 130 ** Functions.test5 ()
 131 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
 132 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
 133 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 134 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 90, characters 9-10
 135 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 90, characters 9-14
 136 <rac:check_term_result>Postcondition of `test5_aux` is ok at "examples/tests/rac.mlw", line 93, characters 4-15
 137                        - Defined at "examples/tests/rac.mlw", line 89, characters 14-27
 138 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 90, characters 9-10
 139 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 90, characters 9-14
 140 <rac:check_term_result>Postcondition of `test5_aux` failed at "examples/tests/rac.mlw", line 94, characters 4-15
 141                        - Defined at "examples/tests/rac.mlw", line 89, characters 14-27
 142                        - Term: x.contents = (x1.contents + 1)
 143                        - Variables: x -> {contents= 3}, x1 -> {contents= 1}
 144 Postcondition of `test5_aux` failed at "examples/tests/rac.mlw", line 94, characters 4-15
 145 - Defined at "examples/tests/rac.mlw", line 89, characters 14-27
 146 - Term: x.contents = (x1.contents + 1)
 147 - Variables: x -> {contents= 3}, x1 -> {contents= 1}
 148 ** Functions.test6 ()
 149 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
 150 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 53, characters 14-15
 151 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 152 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 103, characters 16-17
 153 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 103, characters 16-17
 154 <rac:check_term_result>Precondition of `test6_aux` is ok at "examples/tests/rac.mlw", line 104, characters 12-26
 155                        - Defined at "examples/tests/rac.mlw", line 97, characters 15-21
 156 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 100, characters 4-5
 157 <rac:check_term_result>Postcondition of `test6_aux` is ok at "examples/tests/rac.mlw", line 104, characters 12-26
 158                        - Defined at "examples/tests/rac.mlw", line 98, characters 14-24
 159 <rac:check_term_result>Precondition of `test6_aux` failed at "examples/tests/rac.mlw", line 105, characters 12-26
 160                        - Defined at "examples/tests/rac.mlw", line 97, characters 15-21
 161                        - Term: not x.contents = y
 162                        - Variables: x -> {contents= 42}, y -> 42
 163 Precondition of `test6_aux` failed at "examples/tests/rac.mlw", line 105, characters 12-26
 164 - Defined at "examples/tests/rac.mlw", line 97, characters 15-21
 165 - Term: not x.contents = y
 166 - Variables: x -> {contents= 42}, y -> 42
 167
 168 * Loops
 169 ** Loops.test1 ()
 170 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 112, characters 12-17
 171 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 112, characters 12-17
 172 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 173 <rac:check_term_result>Precondition of `test1` is ok at "command line expression to execute", line 1, characters 0-8
 174                        - Defined at "examples/tests/rac.mlw", line 114, characters 26-31
 175 <rac:check_term_result>Loop invariant init is ok at "examples/tests/rac.mlw", line 116, characters 18-29
 176 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 116, characters 31-31
 177 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 116, characters 18-29
 178 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 116, characters 31-31
 179 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 116, characters 18-29
 180 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 116, characters 31-31
 181 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 116, characters 18-29
 182 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 116, characters 31-31
 183 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 116, characters 18-29
 184 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 116, characters 31-31
 185 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 116, characters 18-29
 186 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 116, characters 31-31
 187 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 116, characters 18-29
 188 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 116, characters 31-31
 189 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 116, characters 18-29
 190 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 116, characters 31-31
 191 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 116, characters 18-29
 192 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 116, characters 31-31
 193 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 116, characters 18-29
 194 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 116, characters 31-31
 195 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 116, characters 18-29
 196 result: () = ()
 197 globals: x -> {contents= 0}
 198 ** Loops.test2 ()
 199 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 112, characters 12-17
 200 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 112, characters 12-17
 201 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 202 <rac:check_term_result>Precondition of `test2` is ok at "command line expression to execute", line 1, characters 0-8
 203                        - Defined at "examples/tests/rac.mlw", line 119, characters 26-31
 204 <rac:check_term_result>Loop invariant init is ok at "examples/tests/rac.mlw", line 121, characters 18-32
 205 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 122, characters 11-12
 206 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 122, characters 11-16
 207 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 121, characters 18-32
 208 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 122, characters 11-12
 209 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 122, characters 11-16
 210 <rac:check_term_result>Loop invariant preservation failed at "examples/tests/rac.mlw", line 121, characters 18-32
 211                        - Term: x.contents = 0 || x.contents = 1
 212                        - Variables: x -> {contents= 2}
 213 Loop invariant preservation failed at "examples/tests/rac.mlw", line 121, characters 18-32
 214 - Term: x.contents = 0 || x.contents = 1
 215 - Variables: x -> {contents= 2}
 216 ** Loops.test3 ()
 217 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 112, characters 12-17
 218 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 112, characters 12-17
 219 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 220 <rac:check_term_result>Loop invariant init is ok at "examples/tests/rac.mlw", line 128, characters 18-24
 221 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 126, characters 10-11
 222 <rac:check_term_result>Postcondition of `(<)` is ok at "examples/tests/rac.mlw", line 126, characters 10-16
 223 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 129, characters 11-12
 224 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 129, characters 11-16
 225 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 128, characters 18-24
 226 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 127, characters 16-22
 227 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 126, characters 10-11
 228 <rac:check_term_result>Postcondition of `(<)` is ok at "examples/tests/rac.mlw", line 126, characters 10-16
 229 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 129, characters 11-12
 230 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 129, characters 11-16
 231 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 128, characters 18-24
 232 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 127, characters 16-22
 233 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 126, characters 10-11
 234 <rac:check_term_result>Postcondition of `(<)` is ok at "examples/tests/rac.mlw", line 126, characters 10-16
 235 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 129, characters 11-12
 236 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 129, characters 11-16
 237 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 128, characters 18-24
 238 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 127, characters 16-22
 239 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 126, characters 10-11
 240 <rac:check_term_result>Postcondition of `(<)` is ok at "examples/tests/rac.mlw", line 126, characters 10-16
 241 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 129, characters 11-12
 242 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 129, characters 11-16
 243 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 128, characters 18-24
 244 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 127, characters 16-22
 245 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 126, characters 10-11
 246 <rac:check_term_result>Postcondition of `(<)` is ok at "examples/tests/rac.mlw", line 126, characters 10-16
 247 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 129, characters 11-12
 248 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 129, characters 11-16
 249 <rac:check_term_result>Loop invariant preservation is ok at "examples/tests/rac.mlw", line 128, characters 18-24
 250 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 127, characters 16-22
 251 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 126, characters 10-11
 252 <rac:check_term_result>Postcondition of `(<)` is ok at "examples/tests/rac.mlw", line 126, characters 10-16
 253 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 129, characters 11-12
 254 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 129, characters 11-16
 255 <rac:check_term_result>Loop invariant preservation failed at "examples/tests/rac.mlw", line 128, characters 18-24
 256                        - Term: 5 >= x.contents
 257                        - Variables: x -> {contents= 6}
 258 Loop invariant preservation failed at "examples/tests/rac.mlw", line 128, characters 18-24
 259 - Term: 5 >= x.contents
 260 - Variables: x -> {contents= 6}
 261
 262 * Aliasing
 263 ** Aliasing.test1 ()
 264 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 265 <rac:check_term_result>Postcondition of `r'mk` is ok at "examples/tests/rac.mlw", line 140, characters 12-22
 266 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 143, characters 13-44
 267 <rac:check_term_result>Postcondition of `value` is ok at "examples/tests/rac.mlw", line 144, characters 13-20
 268 <rac:check_term_result>Postcondition of `value` is ok at "examples/tests/rac.mlw", line 144, characters 4-11
 269 <rac:check_term_result>Postcondition of `Tuple2` is ok at "examples/tests/rac.mlw", line 144, characters 4-20
 270 result: (int, int) = (100, 100)
 271 globals: <none>
 272 ** Aliasing.test2 ()
 273 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 274 <rac:check_term_result>Postcondition of `True` is ok at "examples/tests/rac.mlw", line 157, characters 25-29
 275 <rac:check_term_result>Postcondition of `r'mk` is ok at "examples/tests/rac.mlw", line 147, characters 12-22
 276 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 153, characters 13-27
 277 <rac:check_term_result>Postcondition of `value` is ok at "examples/tests/rac.mlw", line 154, characters 13-20
 278 <rac:check_term_result>Postcondition of `value` is ok at "examples/tests/rac.mlw", line 154, characters 4-11
 279 <rac:check_term_result>Postcondition of `Tuple2` is ok at "examples/tests/rac.mlw", line 154, characters 4-20
 280 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 158, characters 13-32
 281 <rac:check_term_result>Postcondition of `False` is ok at "examples/tests/rac.mlw", line 159, characters 25-30
 282 <rac:check_term_result>Postcondition of `r'mk` is ok at "examples/tests/rac.mlw", line 147, characters 12-22
 283 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 153, characters 13-27
 284 <rac:check_term_result>Postcondition of `value` is ok at "examples/tests/rac.mlw", line 154, characters 13-20
 285 <rac:check_term_result>Postcondition of `value` is ok at "examples/tests/rac.mlw", line 154, characters 4-11
 286 <rac:check_term_result>Postcondition of `Tuple2` is ok at "examples/tests/rac.mlw", line 154, characters 4-20
 287 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 160, characters 13-32
 288 result: () = ()
 289 globals: <none>
 290
 291 * Labels
 292 ** Labels.test1 ()
 293 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 294 <rac:check_term_result>Postcondition of `r'mk` is ok at "examples/tests/rac.mlw", line 169, characters 12-22
 295 <rac:check_term_result>Postcondition of `value` is ok at "examples/tests/rac.mlw", line 171, characters 15-22
 296 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 171, characters 15-26
 297 <rac:check_term_result>Postcondition of `value` is ok at "examples/tests/rac.mlw", line 173, characters 15-22
 298 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 173, characters 15-26
 299 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 174, characters 13-58
 300 result: () = ()
 301 globals: <none>
 302
 303 * RecordMutGhost
 304 ** RecordMutGhost.test ()
 305 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 5-7
 306 <rac:check_term_result>Postcondition of `t'mk` is ok at "examples/tests/rac.mlw", line 212, characters 12-43
 307 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 213, characters 13-20
 308 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 214, characters 13-22
 309 <rac:check_term_result>Postcondition of `f` is ok at "examples/tests/rac.mlw", line 215, characters 20-23
 310 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 216, characters 13-23
 311 <rac:check_term_result>Postcondition of `f` is ok at "examples/tests/rac.mlw", line 217, characters 20-23
 312 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 215, characters 47-52
 313                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 314 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 217, characters 20-25
 315 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 217, characters 4-25
 316 result: int = 43
 317 globals: <none>
 318
 319 * PolyContext
 320 ** PolyContext.test1 ()
 321 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 322 <rac:check_term_result>Postcondition of `poly` is ok at "examples/tests/rac.mlw", line 227, characters 4-10
 323                        - Defined at "examples/tests/rac.mlw", line 222, characters 26-27
 324 <rac:check_term_result>Postcondition of `test1` is ok at "command line expression to execute", line 1, characters 0-8
 325                        - Defined at "examples/tests/rac.mlw", line 226, characters 12-14
 326 result: int = 42
 327 globals: <none>
 328 ** PolyContext.test2 ()
 329 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 330 <rac:check_term_result>Postcondition of `poly` is ok at "examples/tests/rac.mlw", line 231, characters 4-10
 331                        - Defined at "examples/tests/rac.mlw", line 222, characters 26-27
 332 <rac:check_term_result>Postcondition of `poly'` is ok at "examples/tests/rac.mlw", line 235, characters 4-11
 333                        - Defined at "examples/tests/rac.mlw", line 222, characters 26-27
 334 <rac:check_term_result>Postcondition of `test2` is ok at "command line expression to execute", line 1, characters 0-8
 335                        - Defined at "examples/tests/rac.mlw", line 234, characters 12-14
 336 result: int = 42
 337 globals: <none>
 338
 339 * PolyRefContracts
 340 ** PolyRefContracts.test1 ()
 341 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 253, characters 18-19
 342 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 253, characters 18-19
 343 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 344 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 243, characters 12-17
 345 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 243, characters 12-17
 346 <rac:check_term_result>Postcondition of `contents` is ok at "WHY3DATA/stdlib/ref.mlw", line 18, characters 33-43
 347 <rac:check_term_result>Postcondition of `(!)` is ok at "examples/tests/rac.mlw", line 244, characters 9-11
 348 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 244, characters 9-15
 349 <rac:check_term_result>Postcondition of `(:=)` is ok at "examples/tests/rac.mlw", line 244, characters 4-15
 350                        - Defined at "WHY3DATA/stdlib/ref.mlw", line 20, characters 39-44
 351 result: () = ()
 352 globals: myref -> {contents= 0}
 353 ** PolyRefContracts.test2a ()
 354 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 253, characters 18-19
 355 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 253, characters 18-19
 356 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 7-9
 357 <rac:check_term_result>Precondition of `test2_aux` is ok at "examples/tests/rac.mlw", line 256, characters 4-23
 358                        - Defined at "examples/tests/rac.mlw", line 247, characters 15-29
 359 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 251, characters 4-10
 360 <rac:check_term_result>Postcondition of `test2_aux` is ok at "examples/tests/rac.mlw", line 256, characters 4-23
 361                        - Defined at "examples/tests/rac.mlw", line 248, characters 14-27
 362 <rac:check_term_result>Postcondition of `test2_aux` is ok at "examples/tests/rac.mlw", line 256, characters 4-23
 363                        - Defined at "examples/tests/rac.mlw", line 249, characters 14-27
 364 result: int = 1
 365 globals: myref -> {contents= 1}
 366 ** PolyRefContracts.test2b ()
 367 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 253, characters 18-19
 368 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 253, characters 18-19
 369 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 7-9
 370 <rac:check_term_result>Precondition of `test2_aux` failed at "examples/tests/rac.mlw", line 259, characters 4-23
 371                        - Defined at "examples/tests/rac.mlw", line 247, characters 15-29
 372                        - Term: not argref.contents = argx
 373                        - Variables: argref -> {contents= 0}, argx -> 0
 374 Precondition of `test2_aux` failed at "examples/tests/rac.mlw", line 259, characters 4-23
 375 - Defined at "examples/tests/rac.mlw", line 247, characters 15-29
 376 - Term: not argref.contents = argx
 377 - Variables: argref -> {contents= 0}, argx -> 0
 378 ** PolyRefContracts.test2c ()
 379 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 253, characters 18-19
 380 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 253, characters 18-19
 381 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 7-9
 382 <rac:check_term_result>Precondition of `test2_aux` is ok at "examples/tests/rac.mlw", line 262, characters 4-23
 383                        - Defined at "examples/tests/rac.mlw", line 247, characters 15-29
 384 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 251, characters 4-10
 385 <rac:check_term_result>Postcondition of `test2_aux` is ok at "examples/tests/rac.mlw", line 262, characters 4-23
 386                        - Defined at "examples/tests/rac.mlw", line 248, characters 14-27
 387 <rac:check_term_result>Postcondition of `test2_aux` failed at "examples/tests/rac.mlw", line 262, characters 4-23
 388                        - Defined at "examples/tests/rac.mlw", line 249, characters 14-27
 389                        - Term: result = argy
 390                        - Variables: argy -> 2, result -> 1
 391 Postcondition of `test2_aux` failed at "examples/tests/rac.mlw", line 262, characters 4-23
 392 - Defined at "examples/tests/rac.mlw", line 249, characters 14-27
 393 - Term: result = argy
 394 - Variables: argy -> 2, result -> 1
 395
 396 * RecordPoly
 397 ** RecordPoly.test1 ()
 398 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 399 <rac:check_term_result>Postcondition of `t1'mk` is ok at "examples/tests/rac.mlw", line 270, characters 12-18
 400 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 271, characters 13-20
 401 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 273, characters 13-22
 402 result: () = ()
 403 globals: <none>
 404 ** RecordPoly.test2 ()
 405 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 406 <rac:check_term_result>Postcondition of `t2'mk` is ok at "examples/tests/rac.mlw", line 277, characters 12-39
 407 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 278, characters 13-25
 408 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 279, characters 13-25
 409 <rac:check_term_result>Postcondition of `f` is ok at "examples/tests/rac.mlw", line 280, characters 20-23
 410 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 281, characters 13-26
 411 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 282, characters 13-25
 412 result: () = ()
 413 globals: <none>
 414 ** RecordPoly.test3 ()
 415 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 416 <rac:check_term_result>Postcondition of `t3'mk` is ok at "examples/tests/rac.mlw", line 295, characters 12-52
 417 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 296, characters 13-28
 418 <rac:check_term_result>Postcondition of `False` is ok at "examples/tests/rac.mlw", line 297, characters 15-20
 419 <rac:check_term_result>Precondition of `update` is ok at "examples/tests/rac.mlw", line 297, characters 4-20
 420                        - Defined at "examples/tests/rac.mlw", line 287, characters 15-31
 421 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 290, characters 22-28
 422 <rac:check_term_result>Postcondition of `update` is ok at "examples/tests/rac.mlw", line 297, characters 4-20
 423                        - Defined at "examples/tests/rac.mlw", line 288, characters 14-77
 424 <rac:check_term_result>Postcondition of `update` is ok at "examples/tests/rac.mlw", line 297, characters 4-20
 425                        - Defined at "examples/tests/rac.mlw", line 289, characters 14-26
 426 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 298, characters 13-29
 427 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 299, characters 13-28
 428 <rac:check_term_result>Assertion failed at "examples/tests/rac.mlw", line 300, characters 13-29
 429                        - Term: (r.elts @ 1) = False
 430                        - Variables: r -> {elts=
 431                                           (fun j -> if j = i then x
 432                                              else f j) with i = 3, x = false, f = (fun _ -> true);
 433                                           length= 5}
 434 Assertion failed at "examples/tests/rac.mlw", line 300, characters 13-29
 435 - Term: (r.elts @ 1) = False
 436 - Variables: r -> {elts=
 437                    (fun j -> if j = i then x
 438                       else f j) with i = 3, x = false, f = (fun _ -> true);
 439                    length= 5}
 440
 441 * PolyFunc
 442 ** PolyFunc.test1 ()
 443 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 444 <rac:check_term_result>Postcondition of `mk` is ok at "examples/tests/rac.mlw", line 309, characters 6-10
 445 <rac:check_term_result>Postcondition of `test1` is ok at "command line expression to execute", line 1, characters 0-8
 446 result: int -> int = (fun _ -> v) with v = 0
 447 globals: <none>
 448 ** PolyFunc.test2 ()
 449 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 450 <rac:check_term_result>Postcondition of `t'mk` is ok at "examples/tests/rac.mlw", line 320, characters 12-27
 451 <rac:check_term_result>Postcondition of `f` is ok at "examples/tests/rac.mlw", line 317, characters 22-25
 452 <rac:check_term_result>Postcondition of `map_update` is ok at "examples/tests/rac.mlw", line 317, characters 11-29
 453 <rac:check_term_result>Postcondition of `f` is ok at "examples/tests/rac.mlw", line 323, characters 11-14
 454 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 314, characters 23-28
 455                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 456 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 314, characters 41-44
 457 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 323, characters 11-16
 458 <rac:check_term_result>Postcondition of `f` is ok at "examples/tests/rac.mlw", line 323, characters 4-7
 459 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 314, characters 23-28
 460                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 461 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 323, characters 4-9
 462 <rac:check_term_result>Postcondition of `Tuple2` is ok at "examples/tests/rac.mlw", line 323, characters 4-16
 463 result: (int, int) = (111, 0)
 464 globals: <none>
 465
 466 * ArrayExec
 467 ** ArrayExec.test1 ()
 468 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 469 <rac:check_term_result>Postcondition of `array'mk` is ok at "examples/tests/rac.mlw", line 349, characters 12-48
 470 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 350, characters 14-20
 471 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 350, characters 14-22
 472 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 350, characters 4-10
 473 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 350, characters 4-12
 474 <rac:check_term_result>Postcondition of `Tuple2` is ok at "examples/tests/rac.mlw", line 350, characters 4-22
 475 <rac:check_term_result>Postcondition of `test1` is ok at "command line expression to execute", line 1, characters 0-8
 476                        - Defined at "examples/tests/rac.mlw", line 349, character 4 to line 350, character 22
 477 result: (int, int) = (0, 0)
 478 globals: <none>
 479 ** ArrayExec.test2 ()
 480 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 481 <rac:check_term_result>Postcondition of `array'mk` is ok at "examples/tests/rac.mlw", line 353, characters 12-48
 482 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 354, characters 23-29
 483 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 355, characters 14-20
 484 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 354, characters 53-58
 485                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 486 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 354, characters 72-75
 487 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 355, characters 14-22
 488 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 355, characters 4-10
 489 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 354, characters 53-58
 490                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 491 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 355, characters 4-12
 492 <rac:check_term_result>Postcondition of `Tuple2` is ok at "examples/tests/rac.mlw", line 355, characters 4-22
 493 result: (int, int) = (11, 0)
 494 globals: <none>
 495 ** ArrayExec.test3 ()
 496 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 497 <rac:check_term_result>Postcondition of `array'mk` is ok at "examples/tests/rac.mlw", line 336, characters 4-33
 498 <rac:check_term_result>Postcondition of `make` is ok at "examples/tests/rac.mlw", line 358, characters 12-21
 499                        - Defined at "examples/tests/rac.mlw", line 334, characters 14-31
 500 <rac:check_term_result>Postcondition of `make` is ok at "examples/tests/rac.mlw", line 358, characters 12-21
 501                        - Defined at "examples/tests/rac.mlw", line 335, characters 14-55
 502 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 346, characters 27-33
 503 <rac:check_term_result>Postcondition of `map_update` is ok at "examples/tests/rac.mlw", line 346, characters 16-37
 504 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 341, characters 41-47
 505 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 339, characters 23-28
 506                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 507 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 339, characters 41-44
 508 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 341, characters 41-49
 509 <rac:check_term_result>Postcondition of `([])` is ok at "examples/tests/rac.mlw", line 360, characters 10-14
 510                        - Defined at "examples/tests/rac.mlw", line 341, characters 41-49
 511 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 341, characters 41-47
 512 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 339, characters 23-28
 513                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 514 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 341, characters 41-49
 515 <rac:check_term_result>Postcondition of `([])` is ok at "examples/tests/rac.mlw", line 360, characters 4-8
 516                        - Defined at "examples/tests/rac.mlw", line 341, characters 41-49
 517 <rac:check_term_result>Postcondition of `Tuple2` is ok at "examples/tests/rac.mlw", line 360, characters 4-14
 518 result: (int, int) = (10, 0)
 519 globals: <none>
 520 ** ArrayExec.test4 ()
 521 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 522 <rac:check_term_result>Postcondition of `array'mk` is ok at "examples/tests/rac.mlw", line 336, characters 4-33
 523 <rac:check_term_result>Postcondition of `make` is ok at "examples/tests/rac.mlw", line 363, characters 12-21
 524                        - Defined at "examples/tests/rac.mlw", line 334, characters 14-31
 525 <rac:check_term_result>Postcondition of `make` is ok at "examples/tests/rac.mlw", line 363, characters 12-21
 526                        - Defined at "examples/tests/rac.mlw", line 335, characters 14-55
 527 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 364, characters 13-26
 528 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 341, characters 41-47
 529 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 341, characters 41-49
 530 <rac:check_term_result>Postcondition of `([])` is ok at "examples/tests/rac.mlw", line 365, characters 12-16
 531                        - Defined at "examples/tests/rac.mlw", line 341, characters 41-49
 532 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 366, characters 13-18
 533 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 346, characters 27-33
 534 <rac:check_term_result>Postcondition of `map_update` is ok at "examples/tests/rac.mlw", line 346, characters 16-37
 535 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 341, characters 41-47
 536 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 339, characters 23-28
 537                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 538 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 339, characters 41-44
 539 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 341, characters 41-49
 540 <rac:check_term_result>Postcondition of `([])` is ok at "examples/tests/rac.mlw", line 368, characters 12-16
 541                        - Defined at "examples/tests/rac.mlw", line 341, characters 41-49
 542 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 369, characters 13-18
 543 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 341, characters 41-47
 544 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 339, characters 23-28
 545                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 546 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 341, characters 41-49
 547 <rac:check_term_result>Postcondition of `([])` is ok at "examples/tests/rac.mlw", line 370, characters 12-16
 548                        - Defined at "examples/tests/rac.mlw", line 341, characters 41-49
 549 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 371, characters 13-19
 550 <rac:check_term_result>Postcondition of `elts` is ok at "examples/tests/rac.mlw", line 341, characters 41-47
 551 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 339, characters 23-28
 552                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 553 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 339, characters 41-44
 554 <rac:check_term_result>Postcondition of `(@)` is ok at "examples/tests/rac.mlw", line 341, characters 41-49
 555 <rac:check_term_result>Postcondition of `([])` is ok at "examples/tests/rac.mlw", line 372, characters 12-16
 556                        - Defined at "examples/tests/rac.mlw", line 341, characters 41-49
 557 <rac:check_term_result>Assertion failed at "examples/tests/rac.mlw", line 373, characters 13-19
 558                        - Term: x = 11
 559                        - Variables: x -> 0
 560 Assertion failed at "examples/tests/rac.mlw", line 373, characters 13-19
 561 - Term: x = 11
 562 - Variables: x -> 0
 563
 564 * Ghost
 565 ** Ghost.test1 ()
 566 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 567 <rac:check_term_result>Postcondition of `t'mk` is ok at "examples/tests/rac.mlw", line 425, characters 12-30
 568 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 426, characters 13-37
 569 <rac:check_term_result>Postcondition of `i2` is ok at "examples/tests/rac.mlw", line 427, characters 11-15
 570 <rac:check_term_result>Postcondition of `i1` is ok at "examples/tests/rac.mlw", line 427, characters 5-9
 571 <rac:check_term_result>Postcondition of `Tuple2` is ok at "examples/tests/rac.mlw", line 427, characters 4-16
 572 <rac:check_term_result>Postcondition of `test1` is ok at "command line expression to execute", line 1, characters 0-8
 573                        - Defined at "examples/tests/rac.mlw", line 425, character 4 to line 427, character 16
 574 result: (int, int) = (123, 456)
 575 globals: <none>
 576 ** Ghost.test2 ()
 577 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 578 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 430, characters 7-12
 579                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 580 <rac:check_term_result>Postcondition of `f1` is ok at "examples/tests/rac.mlw", line 433, characters 18-24
 581                        - Defined at "examples/tests/rac.mlw", line 430, characters 4-30
 582 <rac:check_term_result>Postcondition of `(+)` is ok at "examples/tests/rac.mlw", line 434, characters 4-9
 583 <rac:check_term_result>Postcondition of `test2` is ok at "command line expression to execute", line 1, characters 0-8
 584                        - Defined at "examples/tests/rac.mlw", line 434, characters 4-9
 585 result: int = 457
 586 globals: <none>
 587
 588 * Predicates
 589 ** Predicates.test1 ()
 590 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 591 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 444, characters 13-19
 592 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 446, characters 13-15
 593 <rac:check_term_result>Postcondition of `True` is ok
 594 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 448, characters 13-15
 595 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 450, characters 13-19
 596 result: () = ()
 597 globals: <none>
 598 ** Predicates.test2 ()
 599 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 600 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 454, characters 13-15
 601 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 456, characters 13-18
 602 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 458, characters 13-15
 603 <rac:check_term_result>Postcondition of `Tuple3` is ok at "examples/tests/rac.mlw", line 459, characters 4-15
 604 <rac:check_term_result>Postcondition of `test2` is ok at "command line expression to execute", line 1, characters 0-8
 605                        - Defined at "examples/tests/rac.mlw", line 453, character 4 to line 459, character 15
 606 result: (bool, int, bool) = (True, 0, True)
 607 globals: <none>
 608
 609 * Arrays
 610 ** Arrays.test0 ()
 611 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 612 <rac:check_term_result>Precondition of `make` is ok at "examples/tests/rac.mlw", line 391, characters 12-21
 613                        - Defined at "WHY3DATA/stdlib/array.mlw", line 60, characters 43-49
 614 <rac:check_term_result>Postcondition of `make` is ok at "examples/tests/rac.mlw", line 391, characters 12-21
 615                        - Defined at "WHY3DATA/stdlib/array.mlw", line 61, characters 14-55
 616 <rac:check_term_result>Postcondition of `make` is ok at "examples/tests/rac.mlw", line 391, characters 12-21
 617                        - Defined at "WHY3DATA/stdlib/array.mlw", line 62, characters 14-31
 618 <rac:check_term_result>Precondition of `([]<-)` is ok at "examples/tests/rac.mlw", line 392, characters 4-14
 619                        - Defined at "WHY3DATA/stdlib/array.mlw", line 31, characters 45-62
 620 <rac:check_term_result>Postcondition of `([]<-)` cannot be evaluated at "examples/tests/rac.mlw", line 392, characters 4-14
 621                        - Defined at "WHY3DATA/stdlib/array.mlw", line 32, characters 15-48
 622 Warning: Postcondition of `([]<-)` cannot be evaluated.
 623
 624 <rac:check_term_result>Postcondition of `([]<-)` cannot be evaluated at "examples/tests/rac.mlw", line 392, characters 4-14
 625                        - Defined at "WHY3DATA/stdlib/array.mlw", line 33, characters 15-34
 626 Warning: Postcondition of `([]<-)` cannot be evaluated.
 627
 628 <rac:check_term_result>Precondition of `([])` is ok at "examples/tests/rac.mlw", line 393, characters 10-14
 629                        - Defined at "WHY3DATA/stdlib/array.mlw", line 23, characters 45-62
 630 <rac:check_term_result>Postcondition of `([])` is ok at "examples/tests/rac.mlw", line 393, characters 10-14
 631                        - Defined at "WHY3DATA/stdlib/array.mlw", line 24, characters 15-28
 632 <rac:check_term_result>Precondition of `([])` is ok at "examples/tests/rac.mlw", line 393, characters 4-8
 633                        - Defined at "WHY3DATA/stdlib/array.mlw", line 23, characters 45-62
 634 <rac:check_term_result>Postcondition of `([])` is ok at "examples/tests/rac.mlw", line 393, characters 4-8
 635                        - Defined at "WHY3DATA/stdlib/array.mlw", line 24, characters 15-28
 636 <rac:check_term_result>Postcondition of `Tuple2` is ok at "examples/tests/rac.mlw", line 393, characters 4-14
 637 result: (int, int) = (10, 0)
 638 globals: <none>
 639 ** Arrays.test1 ()
 640 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 641 <rac:check_term_result>Precondition of `make` is ok at "examples/tests/rac.mlw", line 396, characters 12-21
 642                        - Defined at "WHY3DATA/stdlib/array.mlw", line 60, characters 43-49
 643 <rac:check_term_result>Postcondition of `make` is ok at "examples/tests/rac.mlw", line 396, characters 12-21
 644                        - Defined at "WHY3DATA/stdlib/array.mlw", line 61, characters 14-55
 645 <rac:check_term_result>Postcondition of `make` is ok at "examples/tests/rac.mlw", line 396, characters 12-21
 646                        - Defined at "WHY3DATA/stdlib/array.mlw", line 62, characters 14-31
 647 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 397, characters 13-26
 648 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 398, characters 13-21
 649 <rac:check_term_result>Precondition of `([]<-)` is ok at "examples/tests/rac.mlw", line 399, characters 4-14
 650                        - Defined at "WHY3DATA/stdlib/array.mlw", line 31, characters 45-62
 651 <rac:check_term_result>Postcondition of `([]<-)` cannot be evaluated at "examples/tests/rac.mlw", line 399, characters 4-14
 652                        - Defined at "WHY3DATA/stdlib/array.mlw", line 32, characters 15-48
 653 Warning: Postcondition of `([]<-)` cannot be evaluated.
 654
 655 <rac:check_term_result>Postcondition of `([]<-)` cannot be evaluated at "examples/tests/rac.mlw", line 399, characters 4-14
 656                        - Defined at "WHY3DATA/stdlib/array.mlw", line 33, characters 15-34
 657 Warning: Postcondition of `([]<-)` cannot be evaluated.
 658
 659 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 400, characters 13-21
 660 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 401, characters 13-22
 661 <rac:check_term_result>Assertion failed at "examples/tests/rac.mlw", line 402, characters 13-22
 662                        - Term: a[2] = 11
 663                        - Variables: a -> [0; 11; 0; 0; 0; 0; 0; 0; 0; 0]
 664 Assertion failed at "examples/tests/rac.mlw", line 402, characters 13-22
 665 - Term: a[2] = 11
 666 - Variables: a -> [0; 11; 0; 0; 0; 0; 0; 0; 0; 0]
 667 ** Arrays.test2 ()
 668 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 669 <rac:check_term_result>Precondition of `make` is ok at "examples/tests/rac.mlw", line 408, characters 12-21
 670                        - Defined at "WHY3DATA/stdlib/array.mlw", line 60, characters 43-49
 671 <rac:check_term_result>Postcondition of `make` is ok at "examples/tests/rac.mlw", line 408, characters 12-21
 672                        - Defined at "WHY3DATA/stdlib/array.mlw", line 61, characters 14-55
 673 <rac:check_term_result>Postcondition of `make` is ok at "examples/tests/rac.mlw", line 408, characters 12-21
 674                        - Defined at "WHY3DATA/stdlib/array.mlw", line 62, characters 14-31
 675 <rac:check_term_result>Assertion failed at "examples/tests/rac.mlw", line 409, characters 13-26
 676                        - Term: a.length = 42
 677                        - Variables: a -> [11]
 678 Assertion failed at "examples/tests/rac.mlw", line 409, characters 13-26
 679 - Term: a.length = 42
 680 - Variables: a -> [11]
 681 ** Arrays.test3 ()
 682 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 683 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 412, characters 19-21
 684 <rac:check_term_result>Postcondition of `empty` is ok at "examples/tests/rac.mlw", line 412, characters 12-34
 685                        - Defined at "WHY3DATA/stdlib/array.mlw", line 65, characters 14-31
 686 <rac:check_term_result>Assertion failed at "examples/tests/rac.mlw", line 413, characters 13-26
 687                        - Term: a.length = 42
 688                        - Variables: a -> []
 689 Assertion failed at "examples/tests/rac.mlw", line 413, characters 13-26
 690 - Term: a.length = 42
 691 - Variables: a -> []
 692
 693 * Variants
 694 ** Variants.loop_var_ok1 ()
 695 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 13-15
 696 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 465, characters 16-17
 697 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 465, characters 16-17
 698 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 466, characters 10-11
 699 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 466, characters 10-16
 700 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 468, characters 11-12
 701 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 702 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 703 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 468, characters 11-16
 704 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 467, characters 16-17
 705 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 466, characters 10-11
 706 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 466, characters 10-16
 707 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 468, characters 11-12
 708 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 709 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 710 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 468, characters 11-16
 711 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 467, characters 16-17
 712 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 466, characters 10-11
 713 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 466, characters 10-16
 714 result: () = ()
 715 globals: <none>
 716 ** Variants.loop_var_ok2 ()
 717 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 13-15
 718 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 471, characters 16-17
 719 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 471, characters 16-17
 720 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 472, characters 16-17
 721 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 472, characters 16-17
 722 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 473, characters 10-11
 723 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 473, characters 10-16
 724 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 475, characters 9-10
 725 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 475, characters 9-14
 726 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 476, characters 13-14
 727 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 728 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 729 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 476, characters 13-18
 730 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 474, characters 16-17
 731 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 473, characters 10-11
 732 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 473, characters 10-16
 733 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 475, characters 9-10
 734 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 475, characters 9-14
 735 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 478, characters 13-14
 736 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 737 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 738 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 478, characters 13-18
 739 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 474, characters 16-17
 740 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 473, characters 10-11
 741 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 473, characters 10-16
 742 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 475, characters 9-10
 743 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 475, characters 9-14
 744 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 478, characters 13-14
 745 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 746 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 747 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 478, characters 13-18
 748 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 474, characters 16-17
 749 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 473, characters 10-11
 750 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 473, characters 10-16
 751 result: () = ()
 752 globals: <none>
 753 ** Variants.loop_var_fail1 ()
 754 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 15-17
 755 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 481, characters 16-17
 756 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 481, characters 16-17
 757 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 482, characters 10-11
 758 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 482, characters 10-16
 759 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 484, characters 9-10
 760 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 484, characters 9-14
 761 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 485, characters 13-14
 762 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 763 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 764 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 485, characters 13-18
 765 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 483, characters 16-17
 766 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 482, characters 10-11
 767 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 482, characters 10-16
 768 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 484, characters 9-10
 769 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 484, characters 9-14
 770 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 484, character 6 to line 485, character 18
 771 <rac:check_term_result>Loop variant decrease failed at "examples/tests/rac.mlw", line 483, characters 16-17
 772                        - Term: 0 <= i.contents /\ i1.contents < i.contents \/
 773                                i.contents = i1.contents /\ false
 774                        - Variables: i1 -> {contents= 1}, i -> {contents= 1}
 775 Loop variant decrease failed at "examples/tests/rac.mlw", line 483, characters 16-17
 776 - Term: 0 <= i.contents /\ i1.contents < i.contents \/
 777         i.contents = i1.contents /\ false
 778 - Variables: i1 -> {contents= 1}, i -> {contents= 1}
 779 ** Variants.loop_var_fail2 ()
 780 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 15-17
 781 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 488, characters 16-17
 782 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 488, characters 16-17
 783 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 489, characters 16-17
 784 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 489, characters 16-17
 785 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 490, characters 10-11
 786 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 490, characters 10-16
 787 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 492, characters 9-10
 788 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 492, characters 9-14
 789 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 493, characters 13-14
 790 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 791 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 792 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 493, characters 13-18
 793 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 491, characters 16-17
 794 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 490, characters 10-11
 795 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 490, characters 10-16
 796 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 492, characters 9-10
 797 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 492, characters 9-14
 798 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 494, characters 14-15
 799 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 494, characters 14-19
 800 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 495, characters 13-14
 801 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 802 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 803 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 495, characters 13-18
 804 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 491, characters 16-17
 805 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 490, characters 10-11
 806 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 490, characters 10-16
 807 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 492, characters 9-10
 808 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 492, characters 9-14
 809 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 494, characters 14-15
 810 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 494, characters 14-19
 811 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 494, character 11 to line 495, character 18
 812 <rac:check_term_result>Loop variant decrease failed at "examples/tests/rac.mlw", line 491, characters 16-17
 813                        - Term: 0 <= i.contents /\ i1.contents < i.contents \/
 814                                i.contents = i1.contents /\
 815                                (0 <= j.contents /\ j1.contents < j.contents \/
 816                                 j.contents = j1.contents /\ false)
 817                        - Variables: i1 -> {contents= 0},
 818                          i -> {contents= 0},
 819                          j1 -> {contents= 1},
 820                          j -> {contents= 1}
 821 Loop variant decrease failed at "examples/tests/rac.mlw", line 491, characters 16-17
 822 - Term: 0 <= i.contents /\ i1.contents < i.contents \/
 823         i.contents = i1.contents /\
 824         (0 <= j.contents /\ j1.contents < j.contents \/
 825          j.contents = j1.contents /\ false)
 826 - Variables: i1 -> {contents= 0},
 827   i -> {contents= 0},
 828   j1 -> {contents= 1},
 829   j -> {contents= 1}
 830 ** Variants.loop_custom_variant ()
 831 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 20-22
 832 <rac:check_term_result>Postcondition of `ref'mk` is ok at "examples/tests/rac.mlw", line 502, characters 16-17
 833 <rac:check_term_result>Postcondition of `ref` is ok at "examples/tests/rac.mlw", line 502, characters 16-17
 834 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 503, characters 10-11
 835 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 503, characters 10-16
 836 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 505, characters 11-12
 837 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 838 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 839 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 505, characters 11-16
 840 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 504, characters 16-21
 841 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 503, characters 10-11
 842 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 503, characters 10-16
 843 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 505, characters 11-12
 844 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 845 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 846 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 505, characters 11-16
 847 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 504, characters 16-21
 848 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 503, characters 10-11
 849 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 503, characters 10-16
 850 <rac:check_term_result>Assertion is ok at "examples/tests/rac.mlw", line 507, characters 13-19
 851 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 509, characters 10-11
 852 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 509, characters 10-17
 853 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 511, characters 11-12
 854 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 855 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 856 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 511, characters 11-16
 857 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 510, characters 16-21
 858 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 509, characters 10-11
 859 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 509, characters 10-17
 860 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 511, characters 11-12
 861 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 862 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 863 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 511, characters 11-16
 864 <rac:check_term_result>Loop variant decrease is ok at "examples/tests/rac.mlw", line 510, characters 16-21
 865 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 509, characters 10-11
 866 <rac:check_term_result>Postcondition of `(>=)` is ok at "examples/tests/rac.mlw", line 509, characters 10-17
 867 <rac:check_term_result>Postcondition of `contents` is ok at "examples/tests/rac.mlw", line 511, characters 11-12
 868 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 869 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 870 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 511, characters 11-16
 871 <rac:check_term_result>Loop variant decrease failed at "examples/tests/rac.mlw", line 510, characters 16-21
 872                        - Term: p (2 - i.contents) (2 - i1.contents) \/
 873                                (2 - i1.contents) = (2 - i.contents) /\ false
 874                        - Variables: i -> {contents= (-2)},
 875                          i1 -> {contents= (-1)}
 876 Loop variant decrease failed at "examples/tests/rac.mlw", line 510, characters 16-21
 877 - Term: p (2 - i.contents) (2 - i1.contents) \/
 878         (2 - i1.contents) = (2 - i.contents) /\ false
 879 - Variables: i -> {contents= (-2)}, i1 -> {contents= (-1)}
 880
 881 * TestUInt64
 882 ** TestUInt64.test ()
 883 <rac:check_term_result>Postcondition of `max_uint64` is ok
 884 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/mach/int.mlw", line 614, characters 29-43
 885 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 5-7
 886 <rac:check_term_result>Precondition of `(-)` failed at "examples/tests/rac.mlw", line 517, characters 16-21
 887                        - Defined at "WHY3DATA/stdlib/mach/int.mlw", line 67, characters 40-57
 888                        - Term: in_bounds (a -' b)
 889                        - Variables: a -> 0, b -> 1
 890 Precondition of `(-)` failed at "examples/tests/rac.mlw", line 517, characters 16-21
 891 - Defined at "WHY3DATA/stdlib/mach/int.mlw", line 67, characters 40-57
 892 - Term: in_bounds (a - b)
 893 - Variables: a -> 0, b -> 1
 894
 895 * Premises
 896 ** Premises.test1 ()
 897 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 6-8
 898 <rac:check_term_result>Precondition of `test1` cannot be evaluated at "command line expression to execute", line 1, characters 0-8
 899                        - Defined at "examples/tests/rac.mlw", line 527, characters 15-19
 900 Warning: Precondition of `test1` cannot be evaluated.
 901
 902 <rac:check_term_result>Postcondition of `Tuple0` is ok at "examples/tests/rac.mlw", line 529, characters 4-6
 903 <rac:check_term_result>Postcondition of `test1` is ok at "command line expression to execute", line 1, characters 0-8
 904                        - Defined at "examples/tests/rac.mlw", line 528, characters 14-18
 905 result: () = ()
 906 globals: <none>
 907
 908 * FunctionVariant
 909 ** FunctionVariant.test1 2
 910 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 536, characters 7-12
 911 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 912 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 913 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 536, characters 24-29
 914 <rac:check_term_result>Variant decrease is ok at "examples/tests/rac.mlw", line 535, characters 35-36
 915 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 536, characters 7-12
 916 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 917 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 918 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 536, characters 24-29
 919 <rac:check_term_result>Variant decrease is ok at "examples/tests/rac.mlw", line 535, characters 35-36
 920 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 536, characters 7-12
 921 result: int = 0
 922 globals: <none>
 923 ** FunctionVariant.test2 2
 924 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 539, characters 7-12
 925 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 926 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 927 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 539, characters 24-29
 928 <rac:check_term_result>Variant decrease is ok at "examples/tests/rac.mlw", line 538, characters 35-36
 929 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 539, characters 7-12
 930 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 931 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 932 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 539, characters 24-29
 933 <rac:check_term_result>Variant decrease is ok at "examples/tests/rac.mlw", line 538, characters 35-36
 934 <rac:check_term_result>Postcondition of `(>)` is ok at "examples/tests/rac.mlw", line 539, characters 7-12
 935 <rac:check_term_result>Variant decrease failed at "examples/tests/rac.mlw", line 538, characters 35-36
 936                        - Term: 0 <= i /\ i1 < i \/ i = i1 /\ false
 937                        - Variables: i1 -> 0, i -> 0
 938 Variant decrease failed at "examples/tests/rac.mlw", line 538, characters 35-36
 939 - Term: 0 <= i /\ i1 < i \/ i = i1 /\ false
 940 - Variables: i1 -> 0, i -> 0
 941 ** FunctionVariant.test3 2
 942 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 542, characters 7-12
 943                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 944 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 945 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 946 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 542, characters 38-43
 947 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 948 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 949 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 542, characters 32-37
 950 <rac:check_term_result>Variant decrease is ok at "examples/tests/rac.mlw", line 543, characters 35-36
 951 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 544, characters 7-12
 952                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 953 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 954 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 955 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 544, characters 40-47
 956 <rac:check_term_result>Variant decrease is ok at "examples/tests/rac.mlw", line 543, characters 35-36
 957 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 544, characters 7-12
 958                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 959 <rac:check_term_result>Variant decrease is ok at "examples/tests/rac.mlw", line 541, characters 35-36
 960 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 542, characters 7-12
 961                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 962 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 963 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 964 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 542, characters 38-43
 965 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 966 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 967 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 542, characters 32-37
 968 <rac:check_term_result>Variant decrease is ok at "examples/tests/rac.mlw", line 543, characters 35-36
 969 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 544, characters 7-12
 970                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 971 <rac:check_term_result>Variant decrease is ok at "examples/tests/rac.mlw", line 541, characters 35-36
 972 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 542, characters 7-12
 973                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 974 result: int = 0
 975 globals: <none>
 976 ** FunctionVariant.test4 2
 977 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 547, characters 7-12
 978                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
 979 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 980 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 981 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 547, characters 38-43
 982 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 983 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 984 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 547, characters 32-37
 985 <rac:check_term_result>Variant decrease is ok at "examples/tests/rac.mlw", line 548, characters 35-36
 986 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 987 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 988 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 549, characters 13-20
 989 <rac:check_term_result>Variant decrease is ok at "examples/tests/rac.mlw", line 548, characters 35-36
 990 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 991 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 992 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 549, characters 13-20
 993 <rac:check_term_result>Variant decrease is ok at "examples/tests/rac.mlw", line 548, characters 35-36
 994 <rac:check_term_result>Postcondition of `(-_)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 39-41
 995 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/int.mlw", line 23, characters 35-41
 996 <rac:check_term_result>Postcondition of `(-)` is ok at "examples/tests/rac.mlw", line 549, characters 13-20
 997 <rac:check_term_result>Variant decrease failed at "examples/tests/rac.mlw", line 548, characters 35-36
 998                        - Term: 0 <= i /\ i1 < i \/
 999                                i = i1 /\
1000                                (0 <= j /\ j1 < j \/ j = j1 /\ false)
1001                        - Variables: i1 -> 1, i -> 1, j1 -> (-2), j -> (-1)
1002 Variant decrease failed at "examples/tests/rac.mlw", line 548, characters 35-36
1003 - Term: 0 <= i /\ i1 < i \/ i = i1 /\ (0 <= j /\ j1 < j \/ j = j1 /\ false)
1004 - Variables: i1 -> 1, i -> 1, j1 -> (-2), j -> (-1)
1005 ** FunctionVariant.test5 2
1006 <rac:check_term_result>Postcondition of `(=)` is ok at "examples/tests/rac.mlw", line 552, characters 7-12
1007                        - Defined at "WHY3DATA/stdlib/int.mlw", line 16, characters 39-55
1008 <rac:check_term_result>Variant decrease failed at "examples/tests/rac.mlw", line 553, characters 35-36
1009                        - Term: 0 <= i /\ i1 < i \/ i = i1 /\ false
1010                        - Variables: i1 -> 2, i -> 2
1011 Variant decrease failed at "examples/tests/rac.mlw", line 553, characters 35-36
1012 - Term: 0 <= i /\ i1 < i \/ i = i1 /\ false
1013 - Variables: i1 -> 2, i -> 2
1014
1015 * ArrayList
1016 ** ArrayList.main ()
1017 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 5-7
1018 <rac:check_term_result>Precondition of `make` is ok at "examples/tests/rac.mlw", line 564, characters 12-20
1019                        - Defined at "WHY3DATA/stdlib/array.mlw", line 60, characters 43-49
1020 <rac:check_term_result>Postcondition of `make` is ok at "examples/tests/rac.mlw", line 564, characters 12-20
1021                        - Defined at "WHY3DATA/stdlib/array.mlw", line 61, characters 14-55
1022 <rac:check_term_result>Postcondition of `make` is ok at "examples/tests/rac.mlw", line 564, characters 12-20
1023                        - Defined at "WHY3DATA/stdlib/array.mlw", line 62, characters 14-31
1024 <rac:check_term_result>Precondition of `to_list` is ok at "examples/tests/rac.mlw", line 565, characters 4-17
1025                        - Defined at "WHY3DATA/stdlib/array.mlw", line 378, characters 15-38
1026 <rac:check_term_result>Postcondition of `(<=)` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 7-13
1027 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 49-54
1028 <rac:check_term_result>Variant decrease is ok at "WHY3DATA/stdlib/array.mlw", line 379, characters 15-20
1029 <rac:check_term_result>Precondition of `to_list1` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 38-57
1030                        - Defined at "WHY3DATA/stdlib/array.mlw", line 378, characters 15-38
1031 <rac:check_term_result>Postcondition of `(<=)` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 7-13
1032 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 49-54
1033 <rac:check_term_result>Variant decrease is ok at "WHY3DATA/stdlib/array.mlw", line 379, characters 15-20
1034 <rac:check_term_result>Precondition of `to_list1` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 38-57
1035                        - Defined at "WHY3DATA/stdlib/array.mlw", line 378, characters 15-38
1036 <rac:check_term_result>Postcondition of `(<=)` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 7-13
1037 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 49-54
1038 <rac:check_term_result>Variant decrease is ok at "WHY3DATA/stdlib/array.mlw", line 379, characters 15-20
1039 <rac:check_term_result>Precondition of `to_list1` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 38-57
1040                        - Defined at "WHY3DATA/stdlib/array.mlw", line 378, characters 15-38
1041 <rac:check_term_result>Postcondition of `(<=)` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 7-13
1042 <rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 49-54
1043 <rac:check_term_result>Variant decrease is ok at "WHY3DATA/stdlib/array.mlw", line 379, characters 15-20
1044 <rac:check_term_result>Precondition of `to_list1` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 38-57
1045                        - Defined at "WHY3DATA/stdlib/array.mlw", line 378, characters 15-38
1046 <rac:check_term_result>Postcondition of `(<=)` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 7-13
1047 <rac:check_term_result>Postcondition of `Nil` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 19-22
1048 <rac:check_term_result>Precondition of `([])` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 33-37
1049                        - Defined at "WHY3DATA/stdlib/array.mlw", line 23, characters 45-62
1050 <rac:check_term_result>Postcondition of `([])` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 33-37
1051                        - Defined at "WHY3DATA/stdlib/array.mlw", line 24, characters 15-28
1052 <rac:check_term_result>Postcondition of `Cons` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 28-57
1053 <rac:check_term_result>Precondition of `([])` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 33-37
1054                        - Defined at "WHY3DATA/stdlib/array.mlw", line 23, characters 45-62
1055 <rac:check_term_result>Postcondition of `([])` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 33-37
1056                        - Defined at "WHY3DATA/stdlib/array.mlw", line 24, characters 15-28
1057 <rac:check_term_result>Postcondition of `Cons` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 28-57
1058 <rac:check_term_result>Precondition of `([])` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 33-37
1059                        - Defined at "WHY3DATA/stdlib/array.mlw", line 23, characters 45-62
1060 <rac:check_term_result>Postcondition of `([])` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 33-37
1061                        - Defined at "WHY3DATA/stdlib/array.mlw", line 24, characters 15-28
1062 <rac:check_term_result>Postcondition of `Cons` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 28-57
1063 <rac:check_term_result>Precondition of `([])` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 33-37
1064                        - Defined at "WHY3DATA/stdlib/array.mlw", line 23, characters 45-62
1065 <rac:check_term_result>Postcondition of `([])` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 33-37
1066                        - Defined at "WHY3DATA/stdlib/array.mlw", line 24, characters 15-28
1067 <rac:check_term_result>Postcondition of `Cons` is ok at "WHY3DATA/stdlib/array.mlw", line 380, characters 28-57
1068 <rac:check_term_result>Postcondition of `to_list` is ok at "examples/tests/rac.mlw", line 565, characters 4-17
1069 result: list int = (Cons 0 (Cons 0 (Cons 0 (Cons 0 Nil))))
1070 globals: <none>