tests/while_break.scop

   1 start: 45
   2 end: 294
   3 context: '[N] -> {  : N <= 2147483647 and N >= -2147483648 }'
   4 arrays:
   5 - context: '{  :  }'
   6   extent: '[N] -> { __pet_test_0[t] : t >= 0 }'
   7   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
   8   element_type: int
   9   element_size: 4
  10   uniquely_defined: 1
  11 - context: '{  :  }'
  12   extent: '[N] -> { __pet_test_1[t] : N = 0 and t >= 1; __pet_test_1[0] }'
  13   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  14   element_type: int
  15   element_size: 4
  16   uniquely_defined: 1
  17 - context: '{  :  }'
  18   extent: '[N] -> { __pet_test_2[t] : t >= 0 }'
  19   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  20   element_type: int
  21   element_size: 4
  22   uniquely_defined: 1
  23 - context: '{  :  }'
  24   extent: '[N] -> { __pet_test_3[t] : t >= 0 }'
  25   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  26   element_type: int
  27   element_size: 4
  28   uniquely_defined: 1
  29 - context: '{  :  }'
  30   extent: '[N] -> { a[] }'
  31   element_type: int
  32   element_size: 4
  33 statements:
  34 - line: 10
  35   domain: '[N] -> { S_0[t] : N = 0 and t >= 1; S_0[0] }'
  36   schedule: '[N] -> { S_0[t] -> [0, t, 0] }'
  37   body:
  38     type: binary
  39     operation: =
  40     arguments:
  41     - type: access
  42       relation: '[N] -> { S_0[t] -> a[] }'
  43       index: '[N] -> { S_0[t] -> a[] }'
  44       reference: __pet_ref_0
  45       read: 0
  46       write: 1
  47     - type: access
  48       relation: '[N] -> { S_0[t] -> [5] }'
  49       index: '[N] -> { S_0[t] -> [(5)] }'
  50       reference: __pet_ref_1
  51       read: 1
  52       write: 0
  53 - line: 13
  54   domain: '[N] -> { S_1[t] : N = 0 and t >= 1; S_1[0] : N = 0 }'
  55   schedule: '[N] -> { S_1[t] -> [0, t, 2] }'
  56   body:
  57     type: binary
  58     operation: =
  59     arguments:
  60     - type: access
  61       relation: '[N] -> { S_1[t] -> a[] }'
  62       index: '[N] -> { S_1[t] -> a[] }'
  63       reference: __pet_ref_2
  64       read: 0
  65       write: 1
  66     - type: access
  67       relation: '[N] -> { S_1[t] -> [6] }'
  68       index: '[N] -> { S_1[t] -> [(6)] }'
  69       reference: __pet_ref_3
  70       read: 1
  71       write: 0
  72 - line: 16
  73   domain: '[N] -> { [S_2[t] -> [0]] : t >= 0 }'
  74   schedule: '{ S_2[t] -> [1, t, 0] }'
  75   body:
  76     type: binary
  77     operation: =
  78     arguments:
  79     - type: access
  80       relation: '[N] -> { S_2[t] -> a[] }'
  81       index: '[N] -> { S_2[t] -> a[] }'
  82       reference: __pet_ref_5
  83       read: 0
  84       write: 1
  85     - type: access
  86       relation: '[N] -> { S_2[t] -> [5] }'
  87       index: '[N] -> { S_2[t] -> [(5)] }'
  88       reference: __pet_ref_6
  89       read: 1
  90       write: 0
  91   arguments:
  92   - type: access
  93     relation: '[N] -> { S_2[t] -> __pet_test_0[-1 + t] : t >= 1 }'
  94     index: '[N] -> { S_2[t] -> __pet_test_0[((-1 + t) : t >= 1)] }'
  95     reference: __pet_ref_4
  96     read: 1
  97     write: 0
  98 - line: 17
  99   domain: '[N] -> { [S_3[t] -> [0]] : t >= 0 }'
 100   schedule: '{ S_3[t] -> [1, t, 1, 0] }'
 101   body:
 102     type: binary
 103     operation: =
 104     arguments:
 105     - type: access
 106       relation: '[N] -> { S_3[t] -> __pet_test_0[t] }'
 107       index: '[N] -> { S_3[t] -> __pet_test_0[(t)] }'
 108       reference: __pet_ref_8
 109       read: 0
 110       write: 1
 111     - type: call
 112       name: f
 113   arguments:
 114   - type: access
 115     relation: '[N] -> { S_3[t] -> __pet_test_0[-1 + t] : t >= 1 }'
 116     index: '[N] -> { S_3[t] -> __pet_test_0[((-1 + t) : t >= 1)] }'
 117     reference: __pet_ref_7
 118     read: 1
 119     write: 0
 120 - line: 19
 121   domain: '[N] -> { [S_4[t] -> [0]] : t >= 0 }'
 122   schedule: '{ S_4[t] -> [1, t, 2] }'
 123   body:
 124     type: binary
 125     operation: =
 126     arguments:
 127     - type: access
 128       relation: '[N] -> { S_4[t] -> a[] }'
 129       index: '[N] -> { S_4[t] -> a[] }'
 130       reference: __pet_ref_10
 131       read: 0
 132       write: 1
 133     - type: access
 134       relation: '[N] -> { S_4[t] -> [6] }'
 135       index: '[N] -> { S_4[t] -> [(6)] }'
 136       reference: __pet_ref_11
 137       read: 1
 138       write: 0
 139   arguments:
 140   - type: access
 141     relation: '[N] -> { S_4[t] -> __pet_test_0[t] }'
 142     index: '[N] -> { S_4[t] -> __pet_test_0[(t)] }'
 143     reference: __pet_ref_9
 144     read: 1
 145     write: 0
 146 - line: 21
 147   domain: '[N] -> { [S_5[t] -> [1]] : N = 0 and t >= 1; [S_5[0] -> [1]] }'
 148   schedule: '[N] -> { S_5[t] -> [2, t, 0] }'
 149   body:
 150     type: binary
 151     operation: =
 152     arguments:
 153     - type: access
 154       relation: '[N] -> { S_5[t] -> __pet_test_1[t] }'
 155       index: '[N] -> { S_5[t] -> __pet_test_1[(t)] }'
 156       reference: __pet_ref_13
 157       read: 0
 158       write: 1
 159     - type: call
 160       name: f
 161   arguments:
 162   - type: access
 163     relation: '[N] -> { S_5[t] -> __pet_test_1[-1 + t] : N = 0 and t >= 2; S_5[1]
 164       -> __pet_test_1[0] }'
 165     index: '[N] -> { S_5[t] -> __pet_test_1[((-1 + t) : t = 1 or (N = 0 and t >= 2))]
 166       }'
 167     reference: __pet_ref_12
 168     read: 1
 169     write: 0
 170 - line: 22
 171   domain: '[N] -> { [S_6[t] -> [1]] : N = 0 and t >= 1; [S_6[0] -> [1]] }'
 172   schedule: '[N] -> { S_6[t] -> [2, t, 1, 0] }'
 173   body:
 174     type: binary
 175     operation: =
 176     arguments:
 177     - type: access
 178       relation: '[N] -> { S_6[t] -> a[] }'
 179       index: '[N] -> { S_6[t] -> a[] }'
 180       reference: __pet_ref_15
 181       read: 0
 182       write: 1
 183     - type: access
 184       relation: '[N] -> { S_6[t] -> [5] }'
 185       index: '[N] -> { S_6[t] -> [(5)] }'
 186       reference: __pet_ref_16
 187       read: 1
 188       write: 0
 189   arguments:
 190   - type: access
 191     relation: '[N] -> { S_6[t] -> __pet_test_1[t] }'
 192     index: '[N] -> { S_6[t] -> __pet_test_1[(t)] }'
 193     reference: __pet_ref_14
 194     read: 1
 195     write: 0
 196 - line: 25
 197   domain: '[N] -> { [S_7[t] -> [1]] : N = 0 and t >= 1; [S_7[0] -> [1]] : N = 0 }'
 198   schedule: '[N] -> { S_7[t] -> [2, t, 1, 2] }'
 199   body:
 200     type: binary
 201     operation: =
 202     arguments:
 203     - type: access
 204       relation: '[N] -> { S_7[t] -> a[] }'
 205       index: '[N] -> { S_7[t] -> a[] }'
 206       reference: __pet_ref_18
 207       read: 0
 208       write: 1
 209     - type: access
 210       relation: '[N] -> { S_7[t] -> [6] }'
 211       index: '[N] -> { S_7[t] -> [(6)] }'
 212       reference: __pet_ref_19
 213       read: 1
 214       write: 0
 215   arguments:
 216   - type: access
 217     relation: '[N] -> { S_7[t] -> __pet_test_1[t] }'
 218     index: '[N] -> { S_7[t] -> __pet_test_1[(t)] }'
 219     reference: __pet_ref_17
 220     read: 1
 221     write: 0
 222 - line: 27
 223   domain: '[N] -> { [S_8[t] -> [1, 0]] : t >= 0 }'
 224   schedule: '{ S_8[t] -> [3, t, 0] }'
 225   body:
 226     type: binary
 227     operation: =
 228     arguments:
 229     - type: access
 230       relation: '[N] -> { S_8[t] -> __pet_test_2[t] }'
 231       index: '[N] -> { S_8[t] -> __pet_test_2[(t)] }'
 232       reference: __pet_ref_22
 233       read: 0
 234       write: 1
 235     - type: call
 236       name: f
 237   arguments:
 238   - type: access
 239     relation: '[N] -> { S_8[t] -> __pet_test_2[-1 + t] : t >= 1 }'
 240     index: '[N] -> { S_8[t] -> __pet_test_2[((-1 + t) : t >= 1)] }'
 241     reference: __pet_ref_20
 242     read: 1
 243     write: 0
 244   - type: access
 245     relation: '[N] -> { S_8[t] -> __pet_test_3[-1 + t] : t >= 1 }'
 246     index: '[N] -> { S_8[t] -> __pet_test_3[((-1 + t) : t >= 1)] }'
 247     reference: __pet_ref_21
 248     read: 1
 249     write: 0
 250 - line: 28
 251   domain: '[N] -> { [S_9[t] -> [1, 0]] : t >= 0 }'
 252   schedule: '{ S_9[t] -> [3, t, 1, 0] }'
 253   body:
 254     type: binary
 255     operation: =
 256     arguments:
 257     - type: access
 258       relation: '[N] -> { S_9[t] -> a[] }'
 259       index: '[N] -> { S_9[t] -> a[] }'
 260       reference: __pet_ref_25
 261       read: 0
 262       write: 1
 263     - type: access
 264       relation: '[N] -> { S_9[t] -> [5] }'
 265       index: '[N] -> { S_9[t] -> [(5)] }'
 266       reference: __pet_ref_26
 267       read: 1
 268       write: 0
 269   arguments:
 270   - type: access
 271     relation: '[N] -> { S_9[t] -> __pet_test_2[t] }'
 272     index: '[N] -> { S_9[t] -> __pet_test_2[(t)] }'
 273     reference: __pet_ref_23
 274     read: 1
 275     write: 0
 276   - type: access
 277     relation: '[N] -> { S_9[t] -> __pet_test_3[-1 + t] : t >= 1 }'
 278     index: '[N] -> { S_9[t] -> __pet_test_3[((-1 + t) : t >= 1)] }'
 279     reference: __pet_ref_24
 280     read: 1
 281     write: 0
 282 - line: 29
 283   domain: '[N] -> { [S_10[t] -> [1, 0]] : t >= 0 }'
 284   schedule: '{ S_10[t] -> [3, t, 1, 1, 0] }'
 285   body:
 286     type: binary
 287     operation: =
 288     arguments:
 289     - type: access
 290       relation: '[N] -> { S_10[t] -> __pet_test_3[t] }'
 291       index: '[N] -> { S_10[t] -> __pet_test_3[(t)] }'
 292       reference: __pet_ref_29
 293       read: 0
 294       write: 1
 295     - type: call
 296       name: f
 297   arguments:
 298   - type: access
 299     relation: '[N] -> { S_10[t] -> __pet_test_2[t] }'
 300     index: '[N] -> { S_10[t] -> __pet_test_2[(t)] }'
 301     reference: __pet_ref_27
 302     read: 1
 303     write: 0
 304   - type: access
 305     relation: '[N] -> { S_10[t] -> __pet_test_3[-1 + t] : t >= 1 }'
 306     index: '[N] -> { S_10[t] -> __pet_test_3[((-1 + t) : t >= 1)] }'
 307     reference: __pet_ref_28
 308     read: 1
 309     write: 0
 310 - line: 31
 311   domain: '[N] -> { [S_11[t] -> [1, 0]] : t >= 0 }'
 312   schedule: '{ S_11[t] -> [3, t, 1, 2] }'
 313   body:
 314     type: binary
 315     operation: =
 316     arguments:
 317     - type: access
 318       relation: '[N] -> { S_11[t] -> a[] }'
 319       index: '[N] -> { S_11[t] -> a[] }'
 320       reference: __pet_ref_32
 321       read: 0
 322       write: 1
 323     - type: access
 324       relation: '[N] -> { S_11[t] -> [6] }'
 325       index: '[N] -> { S_11[t] -> [(6)] }'
 326       reference: __pet_ref_33
 327       read: 1
 328       write: 0
 329   arguments:
 330   - type: access
 331     relation: '[N] -> { S_11[t] -> __pet_test_2[t] }'
 332     index: '[N] -> { S_11[t] -> __pet_test_2[(t)] }'
 333     reference: __pet_ref_30
 334     read: 1
 335     write: 0
 336   - type: access
 337     relation: '[N] -> { S_11[t] -> __pet_test_3[t] }'
 338     index: '[N] -> { S_11[t] -> __pet_test_3[(t)] }'
 339     reference: __pet_ref_31
 340     read: 1
 341     write: 0
 342 implications:
 343 - satisfied: 0
 344   extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }'
 345 - satisfied: 1
 346   extension: '[N] -> { __pet_test_1[t] -> __pet_test_1[t''] : N = 0 and t'' <= t and
 347     t'' >= 1; __pet_test_1[t] -> __pet_test_1[0] : t >= 0 }'
 348 - satisfied: 0
 349   extension: '{ __pet_test_3[t] -> __pet_test_3[t''] : t'' <= t and t'' >= 0 }'
 350 - satisfied: 1
 351   extension: '{ __pet_test_2[t] -> __pet_test_2[t''] : t'' <= t and t'' >= 0 }'