Steel with selectors: requires precondition not included in ensures postcondition block

[cmovcc]

Hello, I noticed the following bug while using Steel with selectors, that can be demonstrated with the following minimal example, which contains a simple workaround.

module Reqens

open Steel.Memory
open Steel.Effect.Atomic
open Steel.Effect
open Steel.Reference

[@@expect_failure]
let test (x: nat)
  : Steel nat
  emp (fun _ -> emp)
  (requires (fun _ -> x > 0))
  (ensures (fun _ r _ -> r = 1 / x))
  =
  return (1 / x)

let test (x: nat)
  : Steel nat
  emp (fun _ -> emp)
  (requires (fun _ -> x > 0))
  (ensures (fun _ r _ -> x > 0 /\ r = 1 / x))
  =
  return (1 / x)

Fixing this quite small bug would lead to even more concise specs. Thanks in advance!