mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

Changed to get_const_interp to match Java and C# bindings

Browse source
This commit is contained in:
philzook58 2019-10-03 12:04:56 -04:00 • committed by Nikolaj Bjorner
parent bba9d11fba
commit 0321312c8d
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/api/ml/z3.ml
View file

@ -1546,8 +1546,7 @@ struct
end
let get_const_interp (x:model) (f:func_decl) =
if FuncDecl.get_arity f <> 0 ||
(sort_kind_of_int (Z3native.get_sort_kind (FuncDecl.gc f) (Z3native.get_range (FuncDecl.gc f) f))) = ARRAY_SORT then
if FuncDecl.get_arity f <> 0 then
raise (Error "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.")
else
let np = Z3native.model_get_const_interp (gc x) x f in