mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
parent
91dbcbc36f
commit
382bce4bb7
|
@ -1816,7 +1816,7 @@ struct
|
||||||
|
|
||||||
let get_model x =
|
let get_model x =
|
||||||
let q = Z3native.solver_get_model (gc x) x in
|
let q = Z3native.solver_get_model (gc x) x in
|
||||||
if Z3native.is_null_model q then None else Some q
|
try if Z3native.is_null_model q then None else Some q with | _ -> None
|
||||||
|
|
||||||
let get_proof x =
|
let get_proof x =
|
||||||
let q = Z3native.solver_get_proof (gc x) x in
|
let q = Z3native.solver_get_proof (gc x) x in
|
||||||
|
|
Loading…
Reference in a new issue