From 3c3f127b0cbce7f448155a7621aef596d56ba776 Mon Sep 17 00:00:00 2001
From: Oskar Goldhahn <oskar.goldhahn@ntnu.no>
Date: Thu, 7 May 2026 15:35:16 +0200
Subject: [PATCH] fall back to checking equality of expressions in `sim`

---
 src/ecPV.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/ecPV.ml b/src/ecPV.ml
index 04fb55032..19c763f24 100644
--- a/src/ecPV.ml
+++ b/src/ecPV.ml
@@ -1139,6 +1139,10 @@ module Mpv2 = struct
       when EcReduction.EqTest.for_type env ty1 ty2
         && EcReduction.EqTest.for_type env b1.e_ty b2.e_ty ->
       List.fold_left2 (add_eqs_loc env local) eqs (b1::es1) (b2::es2)
+    | _, _ when EcReduction.EqTest.for_expr env e1 e2 -> 
+      let fv1 = e_read env e1 in
+      let fv2 = e_read env e2 in
+      union eqs (eq_refl (PV.inter fv1 fv2))
     | _, _ -> raise EqObsInError
 
   let add_eqs env e1 e2 eqs =  add_eqs_loc env Mid.empty eqs e1 e2