bench/check-ce/703_reduce_term.mlw

   1 module Use_flags__base
   2   use int.Int
   3   use bv.BV32 as BV32
   4
   5   val function base :
   6     BV32.t
   7 end
   8
   9 module Flags__Oor
  10   use int.Int
  11   use bv.BV32 as BV32
  12
  13   val function oor (param__l: BV32.t) (param__r: BV32.t) :
  14     BV32.t
  15
  16   val function oor__function_guard (temp___result_168: BV32.t) (param__l:
  17     BV32.t) (param__r: BV32.t) : BV32.t
  18 end
  19
  20 module Flags__Oand
  21   use int.Int
  22   use bv.BV32 as BV32
  23
  24   val function oand (param__l: BV32.t) (param__r: BV32.t) :
  25     BV32.t
  26
  27   val function oand__function_guard (temp___result_169: BV32.t) (param__l:
  28     BV32.t) (param__r: BV32.t) : BV32.t
  29 end
  30
  31 module Use_flags__local___axiom
  32   use int.Int
  33   use bv.BV32 as BV32
  34   use Flags__Oor as Flags__Oor
  35   use Flags__Oand as Flags__Oand
  36
  37   val local (param__f: BV32.t) : unit
  38     requires { ((let temp___260 =
  39                    let temp___258 =
  40                      16777216 : BV32.t in
  41                    let temp___257 =
  42                      let temp___255 =
  43                        8388608 : BV32.t in
  44                      let temp___254 =
  45                        let temp___252 =
  46                          4194304 : BV32.t in
  47                        let temp___251 =
  48                          let temp___249 =
  49                            2097152 : BV32.t in
  50                          let temp___248 =
  51                            let temp___246 =
  52                              1048576 : BV32.t in
  53                            let temp___245 =
  54                              let temp___243 =
  55                                524288 : BV32.t in
  56                              let temp___242 =
  57                                let temp___240 =
  58                                  262144 : BV32.t in
  59                                let temp___239 =
  60                                  let temp___237 =
  61                                    131072 : BV32.t in
  62                                  let temp___236 =
  63                                    let temp___234 =
  64                                      65536 : BV32.t in
  65                                    let temp___233 =
  66                                      let temp___231 =
  67                                        32768 : BV32.t in
  68                                      let temp___230 =
  69                                        let temp___228 =
  70                                          16384 : BV32.t in
  71                                        let temp___227 =
  72                                          let temp___225 =
  73                                            8192 : BV32.t in
  74                                          let temp___224 =
  75                                            let temp___222 =
  76                                              4096 : BV32.t in
  77                                            let temp___221 =
  78                                              let temp___219 =
  79                                                2048 : BV32.t in
  80                                              let temp___218 =
  81                                                let temp___216 =
  82                                                  1024 : BV32.t in
  83                                                let temp___215 =
  84                                                  let temp___213 =
  85                                                    512 : BV32.t in
  86                                                  let temp___212 =
  87                                                    let temp___210 =
  88                                                      256 : BV32.t in
  89                                                    let temp___209 =
  90                                                      let temp___207 =
  91                                                        128 : BV32.t in
  92                                                      let temp___206 =
  93                                                        let temp___204 =
  94                                                          64 : BV32.t in
  95                                                        let temp___203 =
  96                                                          let temp___201 =
  97                                                            32 : BV32.t in
  98                                                          let temp___200 =
  99                                                            let temp___198 =
 100                                                              16 : BV32.t in
 101                                                            let temp___197 =
 102                                                              let temp___195 =
 103                                                                8 : BV32.t in
 104                                                              let temp___194 =
 105                                                                let temp___192 =
 106                                                                  4 : BV32.t in
 107                                                                let temp___191 =
 108                                                                  let temp___189 =
 109                                                                    2 : BV32.t in
 110                                                                  let temp___188 =
 111                                                                    let temp___186 =
 112                                                                     1 :
 113                                                                     BV32.t in
 114                                                                    let temp___185 =
 115                                                                     0 :
 116                                                                     BV32.t in
 117                                                                    let temp___result_184:
 118                                                                     BV32.t
 119                                                                     = (
 120                                                                     (Flags__Oor.oor
 121                                                                     temp___185
 122                                                                     temp___186)) in
 123                                                                     (
 124                                                                     (Flags__Oor.oor__function_guard
 125                                                                     temp___result_184
 126                                                                     temp___185
 127                                                                     temp___186)) in
 128                                                                  let temp___result_187:
 129                                                                    BV32.t
 130                                                                     = (
 131                                                                     (Flags__Oor.oor
 132                                                                     temp___188
 133                                                                     temp___189)) in
 134                                                                     (
 135                                                                     (Flags__Oor.oor__function_guard
 136                                                                     temp___result_187
 137                                                                     temp___188
 138                                                                     temp___189)) in
 139                                                                let temp___result_190:
 140                                                                  BV32.t
 141                                                                     =
 142                                                                     (
 143                                                                     (Flags__Oor.oor
 144                                                                     temp___191
 145                                                                     temp___192)) in
 146                                                                     (
 147                                                                     (Flags__Oor.oor__function_guard
 148                                                                     temp___result_190
 149                                                                     temp___191
 150                                                                     temp___192)) in
 151                                                              let temp___result_193:
 152                                                                BV32.t
 153                                                                    =
 154                                                                    (
 155                                                                     (Flags__Oor.oor
 156                                                                     temp___194
 157                                                                     temp___195)) in
 158                                                                   (
 159                                                                    (Flags__Oor.oor__function_guard
 160                                                                     temp___result_193
 161                                                                     temp___194
 162                                                                     temp___195)) in
 163                                                            let temp___result_196:
 164                                                              BV32.t
 165                                                                  = (
 166                                                                     (Flags__Oor.oor
 167                                                                     temp___197
 168                                                                     temp___198)) in
 169                                                                 (
 170                                                                  (Flags__Oor.oor__function_guard
 171                                                                     temp___result_196
 172                                                                     temp___197
 173                                                                     temp___198)) in
 174                                                          let temp___result_199:
 175                                                            BV32.t
 176                                                                = (
 177                                                                   (Flags__Oor.oor
 178                                                                     temp___200
 179                                                                     temp___201)) in
 180                                                               (
 181                                                                (Flags__Oor.oor__function_guard
 182                                                                   temp___result_199
 183                                                                   temp___200
 184                                                                   temp___201)) in
 185                                                        let temp___result_202:
 186                                                          BV32.t
 187                                                              = (
 188                                                                 (Flags__Oor.oor
 189                                                                    temp___203
 190                                                                    temp___204)) in
 191                                                             (
 192                                                              (Flags__Oor.oor__function_guard
 193                                                                 temp___result_202
 194                                                                 temp___203
 195                                                                 temp___204)) in
 196                                                      let temp___result_205:
 197                                                        BV32.t
 198                                                            = (
 199                                                               (Flags__Oor.oor
 200                                                                  temp___206
 201                                                                  temp___207)) in
 202                                                           (
 203                                                            (Flags__Oor.oor__function_guard
 204                                                               temp___result_205
 205                                                               temp___206
 206                                                               temp___207)) in
 207                                                    let temp___result_208:
 208                                                      BV32.t
 209                                                          = (
 210                                                             (Flags__Oor.oor
 211                                                                temp___209
 212                                                                temp___210)) in
 213                                                         (
 214                                                          (Flags__Oor.oor__function_guard
 215                                                             temp___result_208
 216                                                             temp___209
 217                                                             temp___210)) in
 218                                                  let temp___result_211:
 219                                                    BV32.t
 220                                                        = (
 221                                                           (Flags__Oor.oor
 222                                                              temp___212
 223                                                              temp___213)) in
 224                                                       (
 225                                                        (Flags__Oor.oor__function_guard
 226                                                           temp___result_211
 227                                                           temp___212
 228                                                           temp___213)) in
 229                                                let temp___result_214:
 230                                                  BV32.t
 231                                                      = (
 232                                                         (Flags__Oor.oor
 233                                                            temp___215
 234                                                            temp___216)) in
 235                                                     (
 236                                                      (Flags__Oor.oor__function_guard
 237                                                         temp___result_214
 238                                                         temp___215
 239                                                         temp___216)) in
 240                                              let temp___result_217:
 241                                                BV32.t
 242                                                    = (
 243                                                       (Flags__Oor.oor
 244                                                          temp___218
 245                                                          temp___219)) in
 246                                                   (
 247                                                    (Flags__Oor.oor__function_guard
 248                                                       temp___result_217
 249                                                       temp___218
 250                                                       temp___219)) in
 251                                            let temp___result_220:
 252                                              BV32.t
 253                                                  = (
 254                                                     (Flags__Oor.oor
 255                                                        temp___221
 256                                                        temp___222)) in
 257                                                 (
 258                                                  (Flags__Oor.oor__function_guard
 259                                                     temp___result_220
 260                                                     temp___221
 261                                                     temp___222)) in
 262                                          let temp___result_223: BV32.t
 263                                                = (
 264                                                   (Flags__Oor.oor
 265                                                      temp___224
 266                                                      temp___225)) in
 267                                               (
 268                                                (Flags__Oor.oor__function_guard
 269                                                   temp___result_223
 270                                                   temp___224
 271                                                   temp___225)) in
 272                                        let temp___result_226: BV32.t
 273                                              = (
 274                                                 (Flags__Oor.oor
 275                                                    temp___227
 276                                                    temp___228)) in
 277                                             (
 278                                              (Flags__Oor.oor__function_guard
 279                                                 temp___result_226
 280                                                 temp___227
 281                                                 temp___228)) in
 282                                      let temp___result_229: BV32.t
 283                                            = (
 284                                               (Flags__Oor.oor
 285                                                  temp___230
 286                                                  temp___231)) in
 287                                           (
 288                                            (Flags__Oor.oor__function_guard
 289                                               temp___result_229
 290                                               temp___230
 291                                               temp___231)) in
 292                                    let temp___result_232: BV32.t
 293                                          = (
 294                                             (Flags__Oor.oor
 295                                                temp___233
 296                                                temp___234)) in
 297                                         (
 298                                          (Flags__Oor.oor__function_guard
 299                                             temp___result_232
 300                                             temp___233
 301                                             temp___234)) in
 302                                  let temp___result_235: BV32.t
 303                                        = (
 304                                           (Flags__Oor.oor
 305                                              temp___236
 306                                              temp___237)) in
 307                                       (
 308                                        (Flags__Oor.oor__function_guard
 309                                           temp___result_235
 310                                           temp___236
 311                                           temp___237)) in
 312                                let temp___result_238: BV32.t
 313                                      = (
 314                                         (Flags__Oor.oor temp___239 temp___240)) in
 315                                     (
 316                                      (Flags__Oor.oor__function_guard
 317                                         temp___result_238
 318                                         temp___239
 319                                         temp___240)) in
 320                              let temp___result_241: BV32.t
 321                                    = (
 322                                       (Flags__Oor.oor temp___242 temp___243)) in
 323                                   (
 324                                    (Flags__Oor.oor__function_guard
 325                                       temp___result_241
 326                                       temp___242
 327                                       temp___243)) in
 328                            let temp___result_244: BV32.t
 329                                  = (
 330                                     (Flags__Oor.oor temp___245 temp___246)) in
 331                                 (
 332                                  (Flags__Oor.oor__function_guard
 333                                     temp___result_244
 334                                     temp___245
 335                                     temp___246)) in
 336                          let temp___result_247: BV32.t
 337                                = (
 338                                   (Flags__Oor.oor temp___248 temp___249)) in
 339                               (
 340                                (Flags__Oor.oor__function_guard
 341                                   temp___result_247
 342                                   temp___248
 343                                   temp___249)) in
 344                        let temp___result_250: BV32.t
 345                              = (
 346                                 (Flags__Oor.oor temp___251 temp___252)) in
 347                             (
 348                              (Flags__Oor.oor__function_guard
 349                                 temp___result_250
 350                                 temp___251
 351                                 temp___252)) in
 352                      let temp___result_253: BV32.t
 353                            = (
 354                               (Flags__Oor.oor temp___254 temp___255)) in
 355                           (
 356                            (Flags__Oor.oor__function_guard
 357                               temp___result_253
 358                               temp___254
 359                               temp___255)) in
 360                    let temp___result_256: BV32.t
 361                          = (
 362                             (Flags__Oor.oor temp___257 temp___258)) in
 363                         (
 364                          (Flags__Oor.oor__function_guard
 365                             temp___result_256
 366                             temp___257
 367                             temp___258)) in
 368                  let temp___result_259: BV32.t
 369                        = (
 370                           (Flags__Oand.oand param__f temp___260)) in
 371                       (
 372                        (Flags__Oand.oand__function_guard
 373                           temp___result_259
 374                           param__f
 375                           temp___260)))
 376                   = param__f)
 377     }
 378     ensures { true }
 379 end
 380
 381 module Use_flags__subprogram_def
 382   use int.Int
 383   use bv.BV32 as BV32
 384   use Use_flags__base as Use_flags__base
 385   use Flags__Oor as Flags__Oor
 386   use Flags__Oand as Flags__Oand
 387   use Use_flags__local___axiom as Use_flags__local___axiom
 388
 389   (*meta "compute_max_steps" 10*)
 390   let def (__void_param : unit) =
 391     Use_flags__local___axiom.local Use_flags__base.base
 392 end