diff --git a/CMakeLists.txt b/CMakeLists.txt
index 2ace973a1..583e757aa 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -34,7 +34,7 @@ endif()
 ################################################################################
 set(Z3_VERSION_MAJOR 4)
 set(Z3_VERSION_MINOR 8)
-set(Z3_VERSION_PATCH 0)
+set(Z3_VERSION_PATCH 2)
 set(Z3_VERSION_TWEAK 0)
 set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
 set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified
diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 6faeb3edc..3089f5e2b 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -835,6 +835,17 @@ void tst_visit() {
     visit(f);
 }
 
+void tst_numeral() {
+    context c;
+    expr x = c.real_val("1/3");
+    double d = 0;
+    if (!x.is_numeral(d)) {
+        std::cout << x << " is not recognized as a numeral\n";
+        return;
+    }
+    std::cout << x << " is " << d << "\n";
+}
+
 void incremental_example1() {
     std::cout << "incremental example1\n";
     context c;
@@ -1212,6 +1223,7 @@ int main() {
         tactic_example9(); std::cout << "\n";
         tactic_qe(); std::cout << "\n";
         tst_visit(); std::cout << "\n";
+        tst_numeral(); std::cout << "\n";
         incremental_example1(); std::cout << "\n";
         incremental_example2(); std::cout << "\n";
         incremental_example3(); std::cout << "\n";
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 1ec5f05b5..3003578bf 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -9,7 +9,7 @@ from mk_util import *
 
 # Z3 Project definition
 def init_project_def():
-    set_version(4, 8, 0, 0)
+    set_version(4, 8, 2, 0)
     add_lib('util', [], includes2install = ['z3_version.h'])
     add_lib('polynomial', ['util'], 'math/polynomial')
     add_lib('sat', ['util'])
diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index 2891e8cc4..11afed82e 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -227,6 +227,11 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
+    double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a) {
+        Z3_string s = Z3_get_numeral_decimal_string(c, a, 12);
+        return std::stod(std::string(s));
+    }
+
     Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision) {
         Z3_TRY;
         LOG_Z3_get_numeral_decimal_string(c, a, precision);
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 1b1820909..9434323fb 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -709,6 +709,7 @@ namespace z3 {
         bool is_numeral_u(unsigned& i) const { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
         bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
         bool is_numeral(std::string& s, unsigned precision) const { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }
+        bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
         /**
            \brief Return true if this expression is an application.
         */
diff --git a/src/api/dotnet/RatNum.cs b/src/api/dotnet/RatNum.cs
index bad6b323d..ef5f1a867 100644
--- a/src/api/dotnet/RatNum.cs
+++ b/src/api/dotnet/RatNum.cs
@@ -92,6 +92,14 @@ namespace Microsoft.Z3
             return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
         }
 
+        /// <summary>
+        /// Returns a double representing the value.
+        /// </summary>
+        public double Double
+        {
+            get { return Native.Z3_get_numeral_double(Context.nCtx, NativeObject); }
+        }
+
         /// <summary>
         /// Returns a string representation of the numeral.
         /// </summary>        
diff --git a/src/api/dotnet/core/project.json b/src/api/dotnet/core/project.json
deleted file mode 100644
index d54b6877b..000000000
--- a/src/api/dotnet/core/project.json
+++ /dev/null
@@ -1,22 +0,0 @@
-{
-    "version": "1.0.0-*",
-    "buildOptions": {
-        "debugType": "portable",
-        "emitEntryPoint": false,
-        "outputName": "Microsoft.Z3",
-        "compile": [ "../*.cs", "*.cs" ],
-        "define": ["DOTNET_CORE"]
-    },
-    "dependencies": { },
-    "frameworks": {
-        "netcoreapp1.0": {
-            "dependencies": {
-                "Microsoft.NETCore.App": {
-                    "type": "platform",
-                    "version": "1.0.1"
-                }
-            },
-            "imports": "dnxcore50"
-        }
-    }
-}
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 03bce5d5e..bb88c1f98 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -4438,6 +4438,15 @@ extern "C" {
     */
     Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision);
 
+    /**
+       \brief Return numeral as a double.
+
+       \pre Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST || Z3_is_algebraic_number(c, a)
+
+       def_API('Z3_get_numeral_double', STRING, (_in(CONTEXT), _in(AST)))
+    */
+    double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a);
+
     /**
        \brief Return the numerator (as a numeral AST) of a numeral AST of sort Real.