From 80af949e89c9e63ed73c4d080b354e5814956b44 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 2 Feb 2021 04:34:14 -0800
Subject: [PATCH] [sledge] Fix the constant 1 from being considered a subterm

Reviewed By: jvillard

Differential Revision: D25883713

fbshipit-source-id: 3d7103ce4
---
 sledge/src/fol/arithmetic.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml
index 9b03436a3..9edf08f68 100644
--- a/sledge/src/fol/arithmetic.ml
+++ b/sledge/src/fol/arithmetic.ml
@@ -294,7 +294,9 @@ struct
     (* traverse *)
 
     let monos poly =
-      Iter.from_iter (fun f -> Sum.iter poly ~f:(fun mono _ -> f mono))
+      Iter.from_iter (fun f ->
+          Sum.iter poly ~f:(fun mono _ ->
+              if not (Mono.equal_one mono) then f mono ) )
 
     let trms poly = Iter.flat_map ~f:Mono.trms (monos poly)