From fd0213fe82647187b57bd198841dcf6f14556a0e Mon Sep 17 00:00:00 2001
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Date: Wed, 14 Feb 2024 15:57:34 +0100
Subject: [PATCH] fix a ConstraintSimplifier bug

Reported-by: Mathis Bouverot-Dupuis
---
 src/support/ConstraintSimplifier.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/support/ConstraintSimplifier.ml b/src/support/ConstraintSimplifier.ml
index e0dca13..3b6942d 100644
--- a/src/support/ConstraintSimplifier.ml
+++ b/src/support/ConstraintSimplifier.ml
@@ -58,6 +58,7 @@ module Make(T : Utils.Functor) = struct
             VarSet.of_list [v1; v2], Eq (v1, v2)
         end
       | Exist (v, s, c) ->
+        let v = normalize v in
         let fvs, c = simpl (VarSet.add v bvs) c in
         if is_in_env v then (fvs, c)
         else if not (VarSet.mem v fvs) then (fvs, c)