From 4ea9eced05fedfbaa861a10c400d52d5e50afafd Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 16 Apr 2020 03:38:47 -0700
Subject: [PATCH] [sledge] Improve Term.Sum.to_term

Reviewed By: jvillard

Differential Revision: D20863520

fbshipit-source-id: 21092161a
---
 sledge/lib/term.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index 003c31241..e8f091b92 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -478,12 +478,14 @@ module Sum = struct
     else Qset.map_counts ~f:(fun _ -> Q.mul const) sum
 
   let to_term sum =
-    match Qset.length sum with
-    | 0 -> zero
-    | 1 -> (
-      match Qset.min_elt sum with
-      | Some (Integer _, q) -> rational q
-      | Some (arg, q) when Q.equal Q.one q -> arg
+    match Qset.pop sum with
+    | None -> zero
+    | Some (arg, q, sum') when Qset.is_empty sum' -> (
+      match arg with
+      | Integer {data} ->
+          assert (Z.equal Z.one data) ;
+          rational q
+      | _ when Q.equal Q.one q -> arg
       | _ -> Add sum )
     | _ -> Add sum
 end