```fstar fn test (x : ref int) preserves live x { let v = !x; assert pure (v > 0); assert pure False; () } ``` This reports an error on the 2nd assert, but the first one already fails.
This reports an error on the 2nd assert, but the first one already fails.