[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

@@ -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)