mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
ML API bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
47997e175f
commit
2a67301c50
|
@ -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.")
|
||||
|
||||
|
|
Loading…
Reference in a new issue