From 51811443eeb7c594b8db9bbffd387dc0fbfeffd3 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 7 Nov 2019 16:16:14 +0000
Subject: Backport fixes to SMT generation from poly_mapping branch

---
 src/util.ml | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

(limited to 'src/util.ml')

diff --git a/src/util.ml b/src/util.ml
index 02a5468a..99f1111f 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -143,6 +143,22 @@ let remove_dups compare eq l =
   in
   aux [] l'
 
+let lex_ord_list comparison xs ys =
+  let rec lex_lists xs ys =
+    match xs, ys with
+    | x :: xs, y :: ys ->
+       let c = comparison x y in
+       if c = 0 then lex_lists xs ys else c
+    | [], [] -> 0
+    | _, _ -> assert false
+  in
+  if List.length xs = List.length ys then
+    lex_lists xs ys
+  else if List.length xs < List.length ys then
+    -1
+  else
+    1
+
 let rec power i tothe =
   if tothe <= 0
   then 1
@@ -228,7 +244,7 @@ let option_bind f = function
   | None -> None
   | Some(o) -> f o
 
-let rec option_binop f x y = match x, y with
+let option_binop f x y = match x, y with
   | Some x, Some y -> Some (f x y)
   | _ -> None
 
-- 
cgit v1.2.3