[sledge] Strengthen Arithmetic.solve_zero_eq

Reviewed By: jvillard

Differential Revision: D25196725

fbshipit-source-id: 2be190927
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent 2726079a63
commit 86d129847c

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

Loading…
Cancel
Save