Post-condition failures are not localized to the failing branch

[hacklex]

The example below is ripped out of context, so don't be surprised at the absurd conditions. Append was something else originally.

Thing is, fstar fails to localize the problem and just highlights the entire body, just like it did before the update.

module Sandbox

open FStar.List
open FStar.List.Tot.Base

let rec test (#a:eqtype) (p q: list a) (x:a)
  : Lemma (ensures mem x q ==> not (mem x (append p q)))
          (decreases length p + length q) = 
  match p with 
  | [] -> ()
  | ph::pt -> match q with 
            | Nil -> ()
            | qh::qt -> let res = append p q in
                      assert (not (mem qh res));
                      admit();
                      ()

[nikswamy]

This program fails with

Bug2628.fst(9,2-16,24): (Error 19) could not prove post-condition; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel

meaning that it blames the whole match term for the failing postcondition, rather than blaming just the first two branches where the postcondition couldn't be proven.

Localizing postcondition failures to the control flow path(s) on which they were not true would be really nice to have. However, F* doesn't currently have the infrastructure to support tracking errors at that granularity. Would be great to have .... I'm keeping this open.

[hacklex]

Not even both, just highlighting the first failure would also be good news :)