Do not recheck postconditions for lemmas

[mtzguido]

In this module, we have a lemma hardpost whose spec is "hard" to verify (in this case, it's actually incorrect, so this example is not brittle). After verifying it, in this case just admitting it, we should be able to call without any further checking of the spec, but that is not the case, as test0 below fails.

module PostRecheck

#lang-pulse
open Pulse

#push-options "--admit_smt_queries true"
assume
val hardpost (x:int) : Lemma (1/x > 0)
#pop-options

fn test1 ()
  requires emp
  ensures emp
{
  hardpost 1;
  ();
}

fn test0 ()
  requires emp
  ensures emp
{
  hardpost 0;
  ();
}

This does not seem to happen for stt and stt_ghost functions, so maybe that's a workaround.

[gebner]

This does not seem to happen for stt and stt_ghost functions, so maybe that's a workaround.

Because Aseem fixed it in #23 (bug #11).