diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index ac11022c1..a941f8e86 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -931,6 +931,26 @@ namespace Microsoft.Z3
             return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
         }
 
+        /// <summary>
+        /// Create an expression representing <c>t1 xor t2 xor t3 ... </c>.
+        /// </summary>
+        public BoolExpr MkXor(IEnumerable<BoolExpr> ts)
+        {
+            Debug.Assert(ts != null);
+            Debug.Assert(ts.All(a => a != null));
+            CheckContextMatch<BoolExpr>(ts);
+            BoolExpr r = null;
+            foreach (var t in ts) {
+                if (r == null) 
+                   r = t;
+                else
+                   r = MkXor(r, t);
+            }
+            if (r == null) 
+               r = MkTrue();
+            return r;
+        }
+
         /// <summary>
         /// Create an expression representing <c>t[0] and t[1] and ...</c>.
         /// </summary>
diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs
index c24516c22..c0cb091b0 100644
--- a/src/api/dotnet/Model.cs
+++ b/src/api/dotnet/Model.cs
@@ -238,6 +238,14 @@ namespace Microsoft.Z3
             return Eval(t, completion);
         }
 
+        /// <summary>
+        /// Evaluate expression to a double, assuming it is a numeral already.
+        /// </summary>
+        public double Double(Expr t) {
+            var r = Eval(t, true);
+            return Native.Z3_get_numeral_double(Context.nCtx, r.NativeObject);
+        }
+
         /// <summary>
         /// The number of uninterpreted sorts that the model has an interpretation for.
         /// </summary>    
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 7f8b8ba91..98e6531ea 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -405,7 +405,7 @@ public:
 
         TRACE("opt", 
               tout << "sat: " << is_sat << " num cores: " << cores.size() << "\n";
-              for (auto const& c : cores) display_vec(tout, c);
+              for (auto const& c : cores) display_vec(tout, c.m_core);
               tout << "num assumptions: " << m_asms.size() << "\n";);
         
         return is_sat;