From e7345f5ea809049d56705635208ffac8b93ab87a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Apr 2014 15:06:32 +0100 Subject: [PATCH] ML API bugfix Signed-off-by: Christoph M. Wintersteiger --- src/api/ml/z3.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index dda8807c9..e2fa01478 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1482,7 +1482,7 @@ struct let get_big_int ( x : expr ) = if (is_int_numeral x) then - let s = to_string(x) in + let s = (Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)) in (Big_int.big_int_of_string s) else raise (Z3native.Exception "Conversion failed.") @@ -1526,7 +1526,7 @@ struct let get_ratio ( x : expr ) = if (is_rat_numeral x) then - let s = to_string(x) in + let s = (Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)) in (Ratio.ratio_of_string s) else raise (Z3native.Exception "Conversion failed.")