From a51f4e5fec63392db281fae42f934a6177d291d4 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sat, 15 Aug 2020 02:19:59 -0700
Subject: [PATCH] [sledge] Change: Normalize trivial equalities

Summary:
`Sh.norm` relies on `Eq (v, v)` formulas for `v` a variable to be
normalized to `Tt`, which is how eliminated variables are actually
removed from the representation.

Reviewed By: jvillard

Differential Revision: D22571132

fbshipit-source-id: 6d5f3efd7
---
 sledge/src/fol.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 3246c3d80..74afb01ea 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -197,7 +197,7 @@ end = struct
 
   let _Tt = Tt
   let _Ff = Ff
-  let _Eq x y = Eq (x, y)
+  let _Eq x y = if equal_trm x y then Tt else Eq (x, y)
   let _Dq x y = Dq (x, y)
   let _Eq0 x = Eq0 x