From 2a0bbad524031af6235a9444cd6a5f7d212145e2 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 7 Dec 2015 14:42:40 +0000
Subject: [PATCH] Bugfix for ML API

---
 src/api/ml/z3.ml | 28 +++++++++++++++++++---------
 1 file changed, 19 insertions(+), 9 deletions(-)

diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index ca48a72bf..5f6fd8dbd 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -813,16 +813,26 @@ end = struct
       let s = Z3native.get_sort (context_gno ctx) no in
       let sk = (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) s)) in
       if (Z3native.is_algebraic_number (context_gno ctx) no) then
-	Expr(z3_native_object_of_ast_ptr ctx no)
+		Expr(z3_native_object_of_ast_ptr ctx no)
       else
-	if (Z3native.is_numeral_ast (context_gno ctx) no) then
-	  if (sk == INT_SORT || sk == REAL_SORT || sk == BV_SORT || 
-			sk == FLOATING_POINT_SORT || sk == ROUNDING_MODE_SORT) then
-	    Expr(z3_native_object_of_ast_ptr ctx no)
-	  else
-	    raise (Z3native.Exception "Unsupported numeral object")
-	else	  
-	  Expr(z3_native_object_of_ast_ptr ctx no)
+		if (Z3native.is_numeral_ast (context_gno ctx) no) then
+		  match sk with
+		  | REAL_SORT 
+		  | BOOL_SORT 
+		  | ARRAY_SORT 
+		  | BV_SORT 
+		  | ROUNDING_MODE_SORT 
+		  | RELATION_SORT 
+		  | UNINTERPRETED_SORT 
+		  | FLOATING_POINT_SORT 
+		  | INT_SORT 
+		  | DATATYPE_SORT 
+		  | FINITE_DOMAIN_SORT ->
+			 Expr(z3_native_object_of_ast_ptr ctx no)
+		  | _ -> 
+			 raise (Z3native.Exception "Unsupported numeral object")
+		else	  
+		  Expr(z3_native_object_of_ast_ptr ctx no)
 
   let expr_of_ast a = 
     let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc a) (z3obj_gno a))) in