From 86d129847cd9ea5abe766cd1946dc13e838ebc22 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 2 Dec 2020 13:49:03 -0800 Subject: [PATCH] [sledge] Strengthen Arithmetic.solve_zero_eq Reviewed By: jvillard Differential Revision: D25196725 fbshipit-source-id: 2be190927 --- sledge/src/fol/arithmetic.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml index f0fd2ae9c..b987dc077 100644 --- a/sledge/src/fol/arithmetic.ml +++ b/sledge/src/fol/arithmetic.ml @@ -353,11 +353,11 @@ struct | Some f, Some (c, _) -> assert (equal (trm f) c) | _ -> () ) @@ fun () -> - let* a = Embed.get_arith e in + let a = trm e in match for_ with | None -> solve_poly Sum.empty a | Some for_ -> ( - let* for_poly = Embed.get_arith for_ in + let for_poly = trm for_ in match get_mono for_poly with | Some m -> let* c, p = Sum.find_and_remove m a in