From 9e7f58242953667dbdbea73ef3b31a0a0dda7bed Mon Sep 17 00:00:00 2001
From: Peter Lozov <not_kill@gmail.ru>
Date: Thu, 22 Jun 2023 04:21:17 +0300
Subject: [PATCH] Magic fix for disequality simplify exception.

---
 src/core/Subst.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/core/Subst.ml b/src/core/Subst.ml
index 8aa8b2530..c909e7088 100644
--- a/src/core/Subst.ml
+++ b/src/core/Subst.ml
@@ -157,8 +157,12 @@ let unify ?(subsume=false) ?(scope=Term.Var.non_local_scope) env subst x y =
       ~fvar:(fun ((_, subst) as acc) x y ->
         match walk env subst x, walk env subst y with
         | Var x, Var y      ->
-          if Var.equal x y then acc else extend x (Term.repr y) acc
-        | Var x, Value y    -> extend x y acc
+          (* if Var.equal x y then acc else extend x (Term.repr y) acc *)
+         let cmp = Term.Var.compare x y in
+          if cmp < 0 then extend x (Term.repr y) acc
+          else if cmp > 0 then extend y (Term.repr x) acc
+          else acc
+          | Var x, Value y    -> extend x y acc
         | Value x, Var y    -> extend y x acc
         | Value x, Value y  -> helper x y acc
       )