From 383d06b2259e5e32b368fd3f658504486b4755e7 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 10 Dec 2015 15:13:55 +0000
Subject: [PATCH] Bugfix for Expr.isInt in .NET, Java, ML.

Fixes #370
---
 src/api/dotnet/Expr.cs | 6 +-----
 src/api/java/Expr.java | 9 ++-------
 src/api/ml/z3.ml       | 1 -
 3 files changed, 3 insertions(+), 13 deletions(-)

diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index 3b918d76d..599cbf756 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -337,11 +337,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsInt
         {
-            get
-            {
-                return (Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0 &&
-                        Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_INT_SORT);
-            }
+            get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_INT_SORT; }
         }
 
         /// <summary>
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 9c75888e2..b0b95d4b7 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -415,10 +415,7 @@ public class Expr extends AST
      **/
     public boolean isInt()
     {
-        return (Native.isNumeralAst(getContext().nCtx(), getNativeObject()) && Native
-                .getSortKind(getContext().nCtx(),
-                        Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT
-                .toInt());
+        return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT.toInt();
     }
 
     /**
@@ -428,9 +425,7 @@ public class Expr extends AST
      **/
     public boolean isReal()
     {
-        return Native.getSortKind(getContext().nCtx(),
-                Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT
-                .toInt();
+        return Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT.toInt();
     }
 
     /**
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 5f6fd8dbd..84c70001e 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -1545,7 +1545,6 @@ end
 module Arithmetic =
 struct
   let is_int ( x : expr ) =
-    (Z3native.is_numeral_ast (Expr.gnc x) (Expr.gno x)) &&
       ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x)))) == INT_SORT)
       
   let is_arithmetic_numeral ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ANUM)