From e3734d3d2c23881007184ab4047fa2010d45ab30 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 15 Nov 2019 03:31:38 -0800
Subject: [PATCH] [sledge] Fix bug in Term.solve

Summary:
Term.solve makes the assumption that all distinct normalized constants
denote distinct values. This is fragile at best, and it is better to
enumerate the cases where solve discovers inconsistency.

Reviewed By: jvillard

Differential Revision: D18459619

fbshipit-source-id: 71f52557c
---
 sledge/src/llair/term.ml | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index a2d7cdb79..f0c0ec48e 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -1034,16 +1034,17 @@ let solve e f =
   ;
   let rec solve_ e f s =
     let solve_uninterp e f =
-      let ord = compare e f in
-      match (is_constant e, is_constant f) with
-      | true, true when ord <> 0 -> None
-      (* orient equation to discretionarily prefer term that is constant or
-         compares smaller as class representative *)
-      | true, false -> Some (Map.add_exn s ~key:f ~data:e)
-      | false, true -> Some (Map.add_exn s ~key:e ~data:f)
-      | _ ->
-          let key, data = if ord > 0 then (e, f) else (f, e) in
-          Some (Map.add_exn s ~key ~data)
+      match (e, f) with
+      | Integer {data= m}, Integer {data= n} when not (Z.equal m n) -> None
+      | _ -> (
+        match (is_constant e, is_constant f) with
+        (* orient equation to discretionarily prefer term that is constant
+           or compares smaller as class representative *)
+        | true, false -> Some (Map.add_exn s ~key:f ~data:e)
+        | false, true -> Some (Map.add_exn s ~key:e ~data:f)
+        | _ ->
+            let key, data = if compare e f > 0 then (e, f) else (f, e) in
+            Some (Map.add_exn s ~key ~data) )
     in
     let concat_size args =
       Vector.fold_until args ~init:zero