From 0321312c8db1d3f0edbd23e6e48884fbb7d77d1d Mon Sep 17 00:00:00 2001
From: philzook58 <philzook58@gmail.com>
Date: Thu, 3 Oct 2019 12:04:56 -0400
Subject: [PATCH] Changed to get_const_interp to match Java and C# bindings

---
 src/api/ml/z3.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 825f3606cb0..89da9f85ff4 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -1546,8 +1546,7 @@ struct
   end
 
   let get_const_interp (x:model) (f:func_decl) =
-    if FuncDecl.get_arity f <> 0 ||
-       (sort_kind_of_int (Z3native.get_sort_kind (FuncDecl.gc f) (Z3native.get_range (FuncDecl.gc f) f))) = ARRAY_SORT then
+    if FuncDecl.get_arity f <> 0 then
       raise (Error "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.")
     else
       let np = Z3native.model_get_const_interp (gc x) x f  in