Using a `={...}` in a call statement in phoare lemma produces anomoly instead of an error message.

[JoaoDiogoDuarte]

Hi all,

As I was trying to prove a phoare statement, after hours of staring at the computer, I incorrectly wrote a call statement containing ={...}, which should have returned an unknown memory error. However, I got the error anomaly: File "src/ecUtils.ml", line 239, characters 24-30: Assertion failed.

I am on r2026.02.

Here is a minimal working example:

module Minimalexample = {
  proc foo() = {
    return true;
  }
  proc main() = {
    var b : bool;
    b <@ foo();
    return b;
  }
}.

lemma minimalexamplelemma &m:
  Pr[Minimalexample.main() @ &m : res] = 1%r.
proof.
  byphoare. proc.
  call(: ={glob Minimalexample}).
  (* Bad: anomaly: File "src/ecUtils.ml", line 239, characters 24-30: Assertion failed *)

  call(: (glob Minimalexample){1} = (glob Minimalexample){2}).
  (* Good: unknown memory: &1 *)
qed.

[Gustavo2622]

Fixed in PR: #906

[strub]

@Gustavo2622 Don't close the issue manually. It will be automatically closed by merging the linked PR.