Post-condition inference fails without rewrites_to

[gebner]

module Bug455
open Pulse
#lang-pulse

fn bar ()
  returns r: bool
{
  true
}

fn foo () {
  while (not (bar ()))
(*       ^^^^^^^^^^^^
- Could not resolve all free variables in the proposition:
    _posth == op_Negation ?__anf122
*)
    invariant (emp)
  { () };
}

[gebner]

The error comes from the prover, when trying to discharge the following goal:

(exists* (__anf113:Prims.bool).
  emp **
  pure (_posth == Prims.op_Negation __anf113) **
  emp)

[gebner]

This is not limited to while invariants:

fn baz () {
  if (true) { not (bar ()); () };
(*                          ^^
- Could not resolve all free variables in the proposition:
    op_Negation ?__anf175 == op_Negation ?__anf175
*)
  ()
}