From fa23e85bb45777803d3eb36fef6b18610161d415 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 2 Mar 2020 08:44:10 -0800
Subject: [PATCH] [sledge] Dedup equality classes when printing

Reviewed By: ngorogiannis

Differential Revision: D20120266

fbshipit-source-id: 28eaf47db
---
 sledge/src/symbheap/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index a4b6c2ef9..a483e513b 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -660,7 +660,7 @@ let ppx_classes_diff x fs (r, s) =
     (fun fs (rep, cls) ->
       Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) rep
         (List.pp "@ = " (Term.ppx x))
-        (List.sort ~compare:Term.compare cls) )
+        (List.dedup_and_sort ~compare:Term.compare cls) )
     fs (Map.to_alist clss)
 
 (** Existential Witnessing and Elimination *)