From a7b547ccdf3a34149be334d703bb296e946f291d Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 12 Jan 2021 04:24:46 -0800
Subject: [PATCH] [sledge] Fix Context.apply_subst to preserve rest of
 representation

Summary:
Context.apply_subst erroneously resets everything in the
representation of a context except the solution substitution when
applying a substitution.

Reviewed By: jvillard

Differential Revision: D25756548

fbshipit-source-id: 949a34ced
---
 sledge/src/fol/context.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index e558e077b..008dc9e88 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -683,7 +683,8 @@ let apply_subst wrt s r =
   ;
   ( if Subst.is_empty s then r
   else
-    Trm.Map.fold (classes r) empty ~f:(fun ~key:rep ~data:cls r ->
+    Trm.Map.fold (classes r) {r with rep= Subst.empty}
+      ~f:(fun ~key:rep ~data:cls r ->
         let rep' = Subst.subst_ s rep in
         List.fold cls r ~f:(fun trm r ->
             let trm' = Subst.subst_ s trm in