mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 20:18:18 +00:00
edited error message string
This commit is contained in:
parent
0321312c8d
commit
ea8ef3edf8
|
@ -1547,7 +1547,7 @@ struct
|
||||||
|
|
||||||
let get_const_interp (x:model) (f:func_decl) =
|
let get_const_interp (x:model) (f:func_decl) =
|
||||||
if FuncDecl.get_arity f <> 0 then
|
if FuncDecl.get_arity f <> 0 then
|
||||||
raise (Error "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.")
|
raise (Error "Non-zero arity functions have FunctionInterpretations as a model. Use FuncInterp.")
|
||||||
else
|
else
|
||||||
let np = Z3native.model_get_const_interp (gc x) x f in
|
let np = Z3native.model_get_const_interp (gc x) x f in
|
||||||
if Z3native.is_null_ast np then
|
if Z3native.is_null_ast np then
|
||||||
|
|
Loading…
Reference in a new issue