From e7217ac5fe2dff4c57fdf079ba6d25ba41a505b9 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 16 Apr 2020 03:37:19 -0700
Subject: [PATCH] [sledge] Check equality of logical variables by id only

Summary: Term.compare already ignores Var names, make Term.equal do so as well.

Reviewed By: jvillard

Differential Revision: D20663961

fbshipit-source-id: 59e7aa880
---
 sledge/lib/term.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index 5f881e70a..5c5758b7b 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -97,6 +97,12 @@ end = struct
     | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
         Int.compare i j
     | _ -> compare x y
+
+  let equal x y =
+    match (x, y) with
+    | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
+        Int.equal i j
+    | _ -> equal x y
 end
 
 include T