From 4e9f34efea74f53195b69ec783eba9b3b6832709 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Thu, 19 Mar 2020 11:40:28 -0700
Subject: [PATCH] [sledge] fix for `Equality.and_term`

Summary: `r/\true` isn't `true`, it's `r`.

Reviewed By: jberdine

Differential Revision: D20539014

fbshipit-source-id: 7360c1e67
---
 sledge/lib/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml
index 07b03a1bc..c17fc2df5 100644
--- a/sledge/lib/equality.ml
+++ b/sledge/lib/equality.ml
@@ -617,7 +617,7 @@ let orN us rs =
 let rec and_term_ us e r =
   let eq_false b r = and_eq us b Term.false_ r in
   match (e : Term.t) with
-  | Integer {data} -> if Z.is_false data then false_ else true_
+  | Integer {data} -> if Z.is_false data then false_ else r
   | Ap2 (And, a, b) -> and_term_ us a (and_term_ us b r)
   | Ap2 (Eq, a, b) -> and_eq us a b r
   | Ap2 (Xor, Integer {data}, a) when Z.is_true data -> eq_false a r