diff --git a/z3/src/ast.rs b/z3/src/ast.rs
index ae8110b5..ad18cbb1 100644
--- a/z3/src/ast.rs
+++ b/z3/src/ast.rs
@@ -583,10 +583,17 @@ impl<'ctx> Real<'ctx> {
     }
 
     pub fn from_real_str(ctx: &'ctx Context, num: &str, den: &str) -> Option<Real<'ctx>> {
+        let fraction_string = format!("{num:} / {den:}");
+        Self::from_str(ctx, &fraction_string)
+    }
+
+    /// The string may be of the form \[num\]*\[.\[num\]*\]\[E\[+|-\]\[num\]...+\].
+    /// Or a rational, that is, a string of the form \[num\]* / \[num\]*
+    pub fn from_str(ctx: &'ctx Context, numeral: &str) -> Option<Real<'ctx>> {
         let sort = Sort::real(ctx);
         let ast = unsafe {
-            let fraction_cstring = CString::new(format!("{num:} / {den:}")).unwrap();
-            let numeral_ptr = Z3_mk_numeral(ctx.z3_ctx, fraction_cstring.as_ptr(), sort.z3_sort);
+            let c_numeral = CString::new(numeral).unwrap();
+            let numeral_ptr = Z3_mk_numeral(ctx.z3_ctx, c_numeral.as_ptr(), sort.z3_sort);
             if numeral_ptr.is_null() {
                 return None;
             }
@@ -930,6 +937,10 @@ impl<'ctx> Real<'ctx> {
         }
     }
 
+    pub fn as_f64(&self) -> f64 {
+        unsafe { Z3_get_numeral_double(self.ctx.z3_ctx, self.z3_ast) }
+    }
+
     pub fn from_int(ast: &Int<'ctx>) -> Real<'ctx> {
         unsafe { Self::wrap(ast.ctx, Z3_mk_int2real(ast.ctx.z3_ctx, ast.z3_ast)) }
     }