diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index 406031cf1..0a8fff495 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -305,6 +305,9 @@ namespace Microsoft.Z3
}
}
+ ///
+ /// Fixedpoint statistics.
+ ///
public Statistics Statistics
{
get
diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index 29fbfbf75..93d1e0478 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -155,6 +155,9 @@ namespace Microsoft.Z3
return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
}
+ ///
+ /// Optimize statistics.
+ ///
public Statistics Statistics
{
get
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index 4710368aa..ee570da41 100644
--- a/src/api/java/Fixedpoint.java
+++ b/src/api/java/Fixedpoint.java
@@ -308,6 +308,18 @@ public class Fixedpoint extends Z3Object
return res;
}
+ /**
+ * Fixedpoint statistics.
+ *
+ * @throws Z3Exception
+ **/
+ public Statistics getStatistics() throws Z3Exception
+ {
+ return new Statistics(getContext(), Native.fixedpointGetStatistics(
+ getContext().nCtx(), getNativeObject()));
+ }
+
+
Fixedpoint(Context ctx, long obj) throws Z3Exception
{
super(ctx, obj);