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)