Unexpected output from Z3: WARNING: (287323,14): pattern does not contain any variable.

Z3EncodingExample.fst

module Z3EncodingExample

module HS = FStar.HyperStack
module B = LowStar.Buffer

let hloc_t (inv:HS.mem -> Type0) = fp:(h0:HS.mem { inv h0 } -> GTot B.loc) {
  forall (h0 h1:HS.mem). {:pattern fp h0; fp h1} // hloc_buffer_nonworking works if we remove this pattern
  inv h0 /\
  (exists l'. B.modifies l' h0 h1 /\ B.loc_disjoint (fp h0) l') ==> inv h1
}

// Succeeds:
let hloc_buffer' (#a:Type) (b:B.buffer a) (h:HS.mem { B.live h b }): GTot (l:B.loc { B.loc_in l h })
= B.loc_buffer b

let hloc_buffer  (#a:Type) (b:B.buffer a): hloc_t (fun h0 -> B.live h0 b) = hloc_buffer' b

// Fails: (Error 276) Unexpected output from Z3: WARNING: (287323,14): pattern does not contain any variable.
//        (Warning 271) SMT pattern misses at least one bound variable: h0#1453
let hloc_buffer_nonworking  (#a:Type) (b:B.buffer a): hloc_t (fun h0 -> B.live h0 b)
= fun h0 -> B.loc_buffer b