diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index 8c6e6c4c6..3f40b220b 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -269,6 +269,14 @@ namespace Microsoft.Z3
                              AST.ArrayLength(queries), AST.ArrayToNative(queries));
         }
 
+        BoolExpr[] ToBoolExprs(ASTVector v) {
+            uint n = v.Size;
+            BoolExpr[] res = new BoolExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = new BoolExpr(Context, v[i].NativeObject);
+            return res;
+        }
+
         /// <summary>
         /// Retrieve set of rules added to fixedpoint context.
         /// </summary>                
@@ -278,12 +286,7 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
-                uint n = v.Size;
-                BoolExpr[] res = new BoolExpr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new BoolExpr(Context, v[i].NativeObject);
-                return res;
+                return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)));
             }
         }
 
@@ -296,15 +299,27 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
-                uint n = v.Size;
-                BoolExpr[] res = new BoolExpr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new BoolExpr(Context, v[i].NativeObject);
-                return res;
+                return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)));
             }
         }
 
+        /// <summary>
+        /// Parse an SMT-LIB2 file with fixedpoint rules. 
+        /// Add the rules to the current fixedpoint context. 
+        /// Return the set of queries in the file.
+        /// </summary>                
+	public BoolExpr[] ParseFile(string file) {
+            return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file)));
+        }
+
+        /// <summary>
+        /// Similar to ParseFile. Instead it takes as argument a string.
+        /// </summary>                
+
+	public BoolExpr[] ParseString(string s) {
+            return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s)));
+        }
+
 
         #region Internal
         internal Fixedpoint(Context ctx, IntPtr obj)