diff --git a/src/api/java/Model.java b/src/api/java/Model.java index e9922ac58..28934a1f3 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -56,7 +56,7 @@ public class Model extends Z3Object Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT .toInt()) throw new Z3Exception( - "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp."); + "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use getFuncInterp."); long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(), f.getNativeObject()); @@ -101,7 +101,7 @@ public class Model extends Z3Object } else { throw new Z3Exception( - "Constant functions do not have a function interpretation; use ConstInterp"); + "Constant functions do not have a function interpretation; use getConstInterp"); } } else {