[sledge] Do not solve for Integer constants

Reviewed By: jvillard Differential Revision: D21042524 fbshipit-source-id: b00115d71
5 years ago · a3a6a5a6fe
parent 32c5fb2837
commit a3a6a5a6fe
1 changed files with 1 additions and 0 deletions
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@ -1382,6 +1382,7 @@ let solve_for_factor rejected_sum coeff prod sum =
 (* solve [0 = rejected_sum + (coeff × mono) + sum] *)
 let solve_for_mono rejected_sum coeff mono sum =
  match mono with
  | Integer _ -> None
  | Mul prod -> solve_for_factor rejected_sum coeff prod sum
  | _ ->
      if exists_fv_in (fv mono) sum then None