diff --git a/scripts/update_api.py b/scripts/update_api.py
index 78fad45be..4452ae613 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -73,7 +73,7 @@ Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctype
 
 # Mapping to .NET types
 Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double',
-                FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'int', SYMBOL : 'IntPtr',
+                FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'bool', SYMBOL : 'IntPtr',
                 PRINT_MODE : 'uint', ERROR_CODE : 'uint' }
 
 # Mapping to Java types
diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp
index 9bb236fe2..a79f55855 100644
--- a/src/api/api_arith.cpp
+++ b/src/api/api_arith.cpp
@@ -120,12 +120,8 @@ extern "C" {
     }
 
     Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) {
-        Z3_TRY;
         LOG_Z3_is_algebraic_number(c, a);
-        RESET_ERROR_CODE();
-        expr * e = to_expr(a);
-        return mk_c(c)->autil().is_irrational_algebraic_numeral(e);
-        Z3_CATCH_RETURN(Z3_FALSE);
+        return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a));
     }
 
     Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision) {
diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs
index c7ca1851e..64ec88d09 100644
--- a/src/api/dotnet/AST.cs
+++ b/src/api/dotnet/AST.cs
@@ -43,7 +43,7 @@ namespace Microsoft.Z3
                    (!Object.ReferenceEquals(a, null) &&
                     !Object.ReferenceEquals(b, null) &&
                     a.Context.nCtx == b.Context.nCtx &&
-                    Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
+                    Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject));
         }
 
         /// <summary>
diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs
index 596b2943f..9dcb3ef82 100644
--- a/src/api/dotnet/ASTMap.cs
+++ b/src/api/dotnet/ASTMap.cs
@@ -37,7 +37,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(k != null);
 
-            return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject) != 0;
+            return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject);
         }
 
         /// <summary>
diff --git a/src/api/dotnet/BitVecNum.cs b/src/api/dotnet/BitVecNum.cs
index 66054761a..c6055db14 100644
--- a/src/api/dotnet/BitVecNum.cs
+++ b/src/api/dotnet/BitVecNum.cs
@@ -39,7 +39,7 @@ namespace Microsoft.Z3
             get
             {
                 UInt64 res = 0;
-                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not a 64 bit unsigned");
                 return res;
             }
@@ -53,7 +53,7 @@ namespace Microsoft.Z3
             get
             {
                 int res = 0;
-                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not an int");
                 return res;
             }
@@ -67,7 +67,7 @@ namespace Microsoft.Z3
             get
             {
                 Int64 res = 0;
-                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not an int64");
                 return res;
             }
@@ -81,7 +81,7 @@ namespace Microsoft.Z3
             get
             {
                 uint res = 0;
-                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not a uint");
                 return res;
             }
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 890d86619..ba76ae7eb 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -1963,7 +1963,7 @@ namespace Microsoft.Z3
             Contract.Ensures(Contract.Result<IntExpr>() != null);
 
             CheckContextMatch(t);
-            return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
+            return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed)));
         }
 
         /// <summary>
@@ -1980,7 +1980,7 @@ namespace Microsoft.Z3
 
             CheckContextMatch(t1);
             CheckContextMatch(t2);
-            return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
+            return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned)));
         }
 
         /// <summary>
@@ -2031,7 +2031,7 @@ namespace Microsoft.Z3
 
             CheckContextMatch(t1);
             CheckContextMatch(t2);
-            return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
+            return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned)));
         }
 
         /// <summary>
@@ -2080,7 +2080,7 @@ namespace Microsoft.Z3
 
             CheckContextMatch(t1);
             CheckContextMatch(t2);
-            return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
+            return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned)));
         }
 
         /// <summary>
@@ -3135,9 +3135,7 @@ namespace Microsoft.Z3
         public BitVecNum MkBV(bool[] bits)
         {
             Contract.Ensures(Contract.Result<BitVecNum>() != null);
-            int[] _bits = new int[bits.Length];
-            for (int i = 0; i < bits.Length; ++i) _bits[i] = bits[i] ? 1 : 0;	
-            return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits));
+            return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, bits));
         }
 
 
@@ -4186,7 +4184,7 @@ namespace Microsoft.Z3
         public FPNum MkFPInf(FPSort s, bool negative)
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0));
+            return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative));
         }
 
         /// <summary>
@@ -4197,7 +4195,7 @@ namespace Microsoft.Z3
         public FPNum MkFPZero(FPSort s, bool negative)
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0));
+            return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative));
         }
 
         /// <summary>
@@ -4243,7 +4241,7 @@ namespace Microsoft.Z3
         public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn, exp, sig, s.NativeObject));
         }
 
         /// <summary>
@@ -4256,7 +4254,7 @@ namespace Microsoft.Z3
         public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn, exp, sig, s.NativeObject));
         }
 
         /// <summary>
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index f09eecbdd..677ea7f7c 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -179,7 +179,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsNumeral
         {
-            get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) ; }
         }
 
         /// <summary>
@@ -188,7 +188,7 @@ namespace Microsoft.Z3
         /// <returns>True if the term is well-sorted, false otherwise.</returns>
         public bool IsWellSorted
         {
-            get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) ; }
         }
 
         /// <summary>
@@ -239,7 +239,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsAlgebraicNumber
         {
-            get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject); }
         }
         #endregion
 
@@ -256,7 +256,7 @@ namespace Microsoft.Z3
                 return (IsExpr &&
                         Native.Z3_is_eq_sort(Context.nCtx,
                                               Native.Z3_mk_bool_sort(Context.nCtx),
-                                              Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0);
+                                              Native.Z3_get_sort(Context.nCtx, NativeObject)) );
             }
         }
 
@@ -423,7 +423,7 @@ namespace Microsoft.Z3
         {
             get
             {
-                return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
+                return (Native.Z3_is_app(Context.nCtx, NativeObject)  &&
                         (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
                         == Z3_sort_kind.Z3_ARRAY_SORT);
             }
@@ -789,7 +789,7 @@ namespace Microsoft.Z3
         /// Check whether expression is a string constant.
         /// </summary>
         /// <returns>a Boolean</returns>
-        public bool IsString  { get { return IsApp && 0 != Native.Z3_is_string(Context.nCtx, NativeObject); } }
+        public bool IsString  { get { return IsApp && Native.Z3_is_string(Context.nCtx, NativeObject); } }
 
         /// <summary>
         /// Retrieve string corresponding to string constant.
@@ -1336,7 +1336,7 @@ namespace Microsoft.Z3
         {
             get
             {
-                return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
+                return (Native.Z3_is_app(Context.nCtx, NativeObject)  &&
                         Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
                         == (uint)Z3_sort_kind.Z3_RELATION_SORT);
             }
@@ -1458,7 +1458,7 @@ namespace Microsoft.Z3
         {
             get
             {
-                return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
+                return (Native.Z3_is_app(Context.nCtx, NativeObject)  &&
                         Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
             }
         }
@@ -1822,11 +1822,13 @@ namespace Microsoft.Z3
             IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj);
             Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s);
 
-            if (Native.Z3_is_algebraic_number(ctx.nCtx, obj) != 0) // is this a numeral ast?
+            if (Z3_sort_kind.Z3_REAL_SORT == sk && 
+                Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast?
                 return new AlgebraicNum(ctx, obj);
 
-            if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0)
+            if (Native.Z3_is_numeral_ast(ctx.nCtx, obj))
             {
+
                 switch (sk)
                 {
                     case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);
diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs
index 808752eaa..4a2575fe4 100644
--- a/src/api/dotnet/FPNum.cs
+++ b/src/api/dotnet/FPNum.cs
@@ -52,7 +52,7 @@ namespace Microsoft.Z3
             get
             {
                 int res = 0;
-                if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Sign is not a Boolean value");
                 return res != 0;
             }
@@ -86,7 +86,7 @@ namespace Microsoft.Z3
             get
             {
                 UInt64 result = 0;
-                if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0)
+                if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == false)
                     throw new Z3Exception("Significand is not a 64 bit unsigned integer");
                 return result;
             }
@@ -111,7 +111,7 @@ namespace Microsoft.Z3
         /// </summary>
         public string Exponent(bool biased = true)
         {
-            return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased ? 1 : 0);
+            return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased);
         }
 
         /// <summary>
@@ -120,7 +120,7 @@ namespace Microsoft.Z3
         public Int64 ExponentInt64(bool biased = true)
         {
             Int64 result = 0;
-            if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased ? 1 : 0) == 0)
+            if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased) == false)
                 throw new Z3Exception("Exponent is not a 64 bit integer");
             return result;
         }
@@ -133,43 +133,43 @@ namespace Microsoft.Z3
         /// </remarks>
         public BitVecExpr ExponentBV(bool biased = true)
         {
-            return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased ? 1 : 0));
+            return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased));
         }
 
         /// <summary>
         /// Indicates whether the numeral is a NaN.
         /// </summary>
-        public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } }
+        public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) ; } }
 
         /// <summary>
         /// Indicates whether the numeral is a +oo or -oo.
         /// </summary>
-        public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } }
+        public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) ; } }
 
         /// <summary>
         /// Indicates whether the numeral is +zero or -zero.
         /// </summary>
-        public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; } }
+        public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) ; } }
 
         /// <summary>
         /// Indicates whether the numeral is normal.
         /// </summary>
-        public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } }
+        public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) ; } }
 
         /// <summary>
         /// Indicates whether the numeral is subnormal.
         /// </summary>
-        public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) != 0; } }
+        public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) ; } }
 
         /// <summary>
         /// Indicates whether the numeral is positive.
         /// </summary>
-        public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } }
+        public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) ; } }
 
         /// <summary>
         /// Indicates whether the numeral is negative.
         /// </summary>
-        public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } }
+        public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) ; } }
 
         #region Internal
         internal FPNum(Context ctx, IntPtr obj)
diff --git a/src/api/dotnet/FiniteDomainNum.cs b/src/api/dotnet/FiniteDomainNum.cs
index 52c0af8bd..fb51e1014 100644
--- a/src/api/dotnet/FiniteDomainNum.cs
+++ b/src/api/dotnet/FiniteDomainNum.cs
@@ -39,7 +39,7 @@ namespace Microsoft.Z3
             get
             {
                 UInt64 res = 0;
-                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not a 64 bit unsigned");
                 return res;
             }
@@ -53,7 +53,7 @@ namespace Microsoft.Z3
             get
             {
                 int res = 0;
-                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not an int");
                 return res;
             }
@@ -67,7 +67,7 @@ namespace Microsoft.Z3
             get
             {
                 Int64 res = 0;
-                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not an int64");
                 return res;
             }
@@ -81,7 +81,7 @@ namespace Microsoft.Z3
             get
             {
                 uint res = 0;
-                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not a uint");
                 return res;
             }
diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs
index 0587a2276..39ddfad83 100644
--- a/src/api/dotnet/FuncDecl.cs
+++ b/src/api/dotnet/FuncDecl.cs
@@ -38,7 +38,7 @@ namespace Microsoft.Z3
                    (!Object.ReferenceEquals(a, null) &&
                     !Object.ReferenceEquals(b, null) &&
                     a.Context.nCtx == b.Context.nCtx &&
-                    Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
+                    Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject));
         }
 
         /// <summary>
diff --git a/src/api/dotnet/Global.cs b/src/api/dotnet/Global.cs
index acf3fab32..f242003a8 100644
--- a/src/api/dotnet/Global.cs
+++ b/src/api/dotnet/Global.cs
@@ -65,7 +65,7 @@ namespace Microsoft.Z3
         public static string GetParameter(string id)
         {
             IntPtr t;
-            if (Native.Z3_global_param_get(id, out t) == 0)
+            if (Native.Z3_global_param_get(id, out t) == false)
                 return null;
             else
                 return Marshal.PtrToStringAnsi(t);
@@ -91,7 +91,7 @@ namespace Microsoft.Z3
         /// all contexts globally.</remarks>
         public static void ToggleWarningMessages(bool enabled)
         {
-            Native.Z3_toggle_warning_messages((enabled) ? 1 : 0);
+            Native.Z3_toggle_warning_messages(enabled);
         }
 
         /// <summary>
diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs
index 03e573538..a5e35fcd5 100644
--- a/src/api/dotnet/Goal.cs
+++ b/src/api/dotnet/Goal.cs
@@ -103,7 +103,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool Inconsistent
         {
-            get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) ; }
         }
 
         /// <summary>
@@ -163,7 +163,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsDecidedSat
         {
-            get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) ; }
         }
 
         /// <summary>
@@ -171,7 +171,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsDecidedUnsat
         {
-            get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) ; }
         }
 
 	/// <summary>
@@ -251,7 +251,7 @@ namespace Microsoft.Z3
         internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
         internal Goal(Context ctx, bool models, bool unsatCores, bool proofs)
-            : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0))
+            : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models), (unsatCores), (proofs)))
         {
             Contract.Requires(ctx != null);
         }
diff --git a/src/api/dotnet/IntNum.cs b/src/api/dotnet/IntNum.cs
index 64fd78ad2..78fee44f4 100644
--- a/src/api/dotnet/IntNum.cs
+++ b/src/api/dotnet/IntNum.cs
@@ -49,7 +49,7 @@ namespace Microsoft.Z3
             get
             {
                 UInt64 res = 0;
-                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not a 64 bit unsigned");
                 return res;
             }
@@ -63,7 +63,7 @@ namespace Microsoft.Z3
             get
             {
                 int res = 0;
-                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not an int");
                 return res;
             }
@@ -77,7 +77,7 @@ namespace Microsoft.Z3
             get
             {
                 Int64 res = 0;
-                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not an int64");
                 return res;
             }
@@ -91,7 +91,7 @@ namespace Microsoft.Z3
             get
             {
                 uint res = 0;
-                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not a uint");
                 return res;
             }
diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs
index d11a57052..2c6d12dc0 100644
--- a/src/api/dotnet/Model.cs
+++ b/src/api/dotnet/Model.cs
@@ -86,7 +86,7 @@ namespace Microsoft.Z3
                         return null;
                     else
                     {
-                        if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
+                        if (Native.Z3_is_as_array(Context.nCtx, n) == false)
                             throw new Z3Exception("Argument was not an array constant");
                         IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
                         return FuncInterp(new FuncDecl(Context, fd));
@@ -227,7 +227,7 @@ namespace Microsoft.Z3
             Contract.Ensures(Contract.Result<Expr>() != null);
 
             IntPtr v = IntPtr.Zero;
-            if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, ref v) == 0)
+            if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion), ref v) == false)
                 throw new ModelEvaluationFailedException();
             else
                 return Expr.Create(Context, v);
diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs
index 5b143d525..eeda55755 100644
--- a/src/api/dotnet/Params.cs
+++ b/src/api/dotnet/Params.cs
@@ -35,7 +35,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(name != null);
 
-            Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0);
+            Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value));
             return this;
         }
 
@@ -90,7 +90,7 @@ namespace Microsoft.Z3
         /// </summary>
         public Params Add(string name, bool value)
         {
-            Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0);
+            Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value));
 	    return this;
         }
 
diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs
index e34b4ef97..d729f7424 100644
--- a/src/api/dotnet/Quantifier.cs
+++ b/src/api/dotnet/Quantifier.cs
@@ -33,7 +33,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsUniversal
         {
-            get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject); }
         }
 
         /// <summary>
@@ -41,7 +41,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsExistential
         {
-            get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject); }
         }
 
         /// <summary>
@@ -193,7 +193,7 @@ namespace Microsoft.Z3
 
             if (noPatterns == null && quantifierID == null && skolemID == null)
             {
-                NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight,
+                NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) , weight,
                                            AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
                                            AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
                                            Symbol.ArrayToNative(names),
@@ -201,7 +201,7 @@ namespace Microsoft.Z3
             }
             else
             {
-                NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall) ? 1 : 0, weight,
+                NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall), weight,
                                   AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
                                   AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
                                   AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
@@ -229,14 +229,14 @@ namespace Microsoft.Z3
 
             if (noPatterns == null && quantifierID == null && skolemID == null)
             {
-                NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) ? 1 : 0, weight,
+                NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) , weight,
                                                  AST.ArrayLength(bound), AST.ArrayToNative(bound),
                                                  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
                                                  body.NativeObject);
             }
             else
             {
-                NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall) ? 1 : 0, weight,
+                NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall), weight,
                                         AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
                                         AST.ArrayLength(bound), AST.ArrayToNative(bound),
                                         AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
diff --git a/src/api/dotnet/Sort.cs b/src/api/dotnet/Sort.cs
index e6f195434..66acc5c0f 100644
--- a/src/api/dotnet/Sort.cs
+++ b/src/api/dotnet/Sort.cs
@@ -41,7 +41,7 @@ namespace Microsoft.Z3
                    (!Object.ReferenceEquals(a, null) &&
                     !Object.ReferenceEquals(b, null) &&
                     a.Context == b.Context &&
-                    Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
+                    Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject));
         }
 
         /// <summary>
diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs
index c94af625c..6708035bc 100644
--- a/src/api/dotnet/Statistics.cs
+++ b/src/api/dotnet/Statistics.cs
@@ -134,9 +134,9 @@ namespace Microsoft.Z3
                 {
                     Entry e;
                     string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i);
-                    if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) != 0)
+                    if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) )
                         e = new Entry(k, Native.Z3_stats_get_uint_value(Context.nCtx, NativeObject, i));
-                    else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) != 0)
+                    else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) )
                         e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i));
                     else
                         throw new Z3Exception("Unknown data entry value");
diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index fe5bc3af5..be3a02019 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -638,6 +638,11 @@ bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int
     return true;
 }
 
+bool arith_recognizers::is_irrational_algebraic_numeral(expr const * n) const { 
+    return is_app(n) && to_app(n)->is_app_of(m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); 
+}
+
+
 #define IS_INT_EXPR_DEPTH_LIMIT 100
 bool arith_recognizers::is_int_expr(expr const *e) const {
     if (is_int(e)) return true;
@@ -678,7 +683,7 @@ void arith_util::init_plugin() {
     m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(m_afid));
 }
 
-bool arith_util::is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val) {
+bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) {
     if (!is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM))
         return false;
     am().set(val, to_irrational_algebraic_numeral(n));
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index d7340297b..17b8fa1d0 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -229,7 +229,7 @@ public:
     family_id get_family_id() const { return m_afid; }
 
     bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == m_afid; }
-    bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
+    bool is_irrational_algebraic_numeral(expr const * n) const;
     bool is_numeral(expr const * n, rational & val, bool & is_int) const;
     bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); }
     bool is_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_NUM); }
@@ -338,8 +338,7 @@ public:
         return plugin().am();
     }
 
-    bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
-    bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val);
+    bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val);
     algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
 
     sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); }