From 5d429ea0752dee28975bbe4b45f0a9799ead4445 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 4 Mar 2020 06:21:12 -0800
Subject: [PATCH] [sledge] Improve Equality.extend

Reviewed By: jvillard

Differential Revision: D20192872

fbshipit-source-id: a853d8c4e
---
 sledge/src/symbheap/equality.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 21892fb8e..38de2f3cb 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -444,17 +444,19 @@ let rec canon r a =
   |>
   [%Trace.retn fun {pf} -> pf "%a" Term.pp]
 
-(** add a term to the carrier *)
-let rec extend a r =
+let rec extend_ a r =
   match classify a with
-  | Interpreted | Simplified -> Term.fold ~f:extend a ~init:r
+  | Interpreted | Simplified -> Term.fold ~f:extend_ a ~init:r
   | Uninterpreted -> (
-    match Subst.extend a r.rep with
-    | Some rep -> Term.fold ~f:extend a ~init:{r with rep}
+    match Subst.extend a r with
+    | Some r -> Term.fold ~f:extend_ a ~init:r
     | None -> r )
   | Atomic -> r
 
-let extend a r = extend a r |> check invariant
+(** add a term to the carrier *)
+let extend a r =
+  let rep = extend_ a r.rep in
+  if rep == r.rep then r else {r with rep} |> check invariant
 
 let merge us a b r =
   [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Term.pp a Term.pp b pp r]