diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index b06f9ed16..f716301e4 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -657,7 +657,8 @@ namespace Microsoft.Z3 /// A string containing the DIMACS CNF representation. public string ToDimacs(bool includeNames = true) { - return Native.Z3_solver_to_dimacs_string(Context.nCtx, NativeObject, includeNames ? (byte)1 : (byte)0); + byte includeNamesByte = includeNames ? (byte)1 : (byte)0; + return Native.Z3_solver_to_dimacs_string(Context.nCtx, NativeObject, includeNamesByte); } #region Internal diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 23f3a68d0..6a9939cb2 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -1999,7 +1999,8 @@ public class Context implements AutoCloseable { Native.mkArrayDefault(nCtx(), array.getNativeObject())); } - /** * Create an as-array expression from a function declaration. + /** + * Create an as-array expression from a function declaration. * @param f the function declaration to lift into an array. * Must have exactly one domain sort. * @see #mkTermArray(Expr) @@ -2011,7 +2012,6 @@ public class Context implements AutoCloseable { return (ArrayExpr) Expr.create(this, Native.mkAsArray(nCtx(), f.getNativeObject())); } - /** * Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt. **/