Backport fixes to SMT generation from poly_mapping branch

1 files changed, 17 insertions, 1 deletions

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