From a3a6a5a6fec34639f9c5bd39d5c5d6d0af29d300 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 16 Apr 2020 03:39:57 -0700
Subject: [PATCH] [sledge] Do not solve for Integer constants

Reviewed By: jvillard

Differential Revision: D21042524

fbshipit-source-id: b00115d71
---
 sledge/lib/term.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index 08fff4ee1..d2a50219a 100644
--- 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