Confusing result by `wp_op`

As reported in private by @birkedal:

From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".

Definition test `{heapG Σ} (n : nat) (v : val) :
  (WP if: #n = v then #true else #false {{ _, True }})%I.
Proof.
  wp_op.

This gives

bin_op_eval EqOp #n v = Some ?Goal0
______________________________________(2/2)
--------------------------------------∗
WP if: ?Goal0 then #true else #false {{ _, True }}

Pre !97 (merged) this used to work because bin_op_eval used to match first on the operations and then on the operand. Right now, it first matches on the operands, and only then on the operation.