mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 10:26:16 +00:00
Code Activity

Java API comments fix.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-11-04 13:34:50 +00:00
parent 2f216ee5c1
commit 715050da0b
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/java/Model.java
View file

@ -56,7 +56,7 @@ public class Model extends Z3Object
Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT
.toInt()) .toInt())
throw new Z3Exception( 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(), long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
f.getNativeObject()); f.getNativeObject());
@ -101,7 +101,7 @@ public class Model extends Z3Object
} else } else
{ {
throw new Z3Exception( throw new Z3Exception(
"Constant functions do not have a function interpretation; use ConstInterp"); "Constant functions do not have a function interpretation; use getConstInterp");
} }
} else } else
{ {