Bad error localization

[tdardinier]

The fold line 252 in the attached file makes verification fail (and commenting it out makes verification succeed). However, the warnings and errors reported are not really helpful. From the command line, I get

...
(Error 19) assertion failed; The SMT solver could not prove the query. Use --query_stats for more details.
../../../../share/steel/examples/pulse/parallel/NewDomains.fst(68,5-68,29): (Warning 249) Losing precision when encoding a function literal: fun a -> NewDomains.unit_emp_stt_pure_pure u#0 a
(Unnannotated abstraction in the compiler ?) (see also ../../../../share/steel/examples/pulse/parallel/NewDomains.fst(65,2-68,27))
../../../../share/steel/examples/pulse/parallel/NewDomains.fst(68,5-251,24): (Warning 249) Losing precision when encoding a function literal: fun v ->
  Pulse.Lib.Reference.pts_to (Mkdtuple4?._3 u#1 u#0 u#0 u#0 (Mkdtuple2?._1 u#1 u#0 t))
    NewDomains.half
    v **
  Pulse.Lib.Core.pure (Some? u#0 v)
...

• The first problem is the range of warning 249, from line 68 to line 251, while it should only be localized on line 113
• The second problem is that the actual error 19 (related to the fold on line 252), is reported in VSCode on line 1