diff --git a/src/api/dotnet/Deprecated.cs b/src/api/dotnet/Deprecated.cs
index 7dc524834..aa6dffb45 100644
--- a/src/api/dotnet/Deprecated.cs
+++ b/src/api/dotnet/Deprecated.cs
@@ -65,22 +65,29 @@ namespace Microsoft.Z3
         /// <summary>
         /// Checks whether the assertions in the context are consistent or not.
         /// </summary>
-        public static Status Check(Context ctx, List<BoolExpr> core, params Expr[] assumptions)
+        public static Status Check(Context ctx, List<BoolExpr> core, ref Model model, ref Expr proof, params Expr[] assumptions)
         {
             Z3_lbool r;
-            core = null;
+            model = null;
+            proof = null;
             if (assumptions == null || assumptions.Length == 0)
                 r = (Z3_lbool)Native.Z3_check(ctx.nCtx);
             else {
-                IntPtr model = IntPtr.Zero, proof = IntPtr.Zero;
+                IntPtr mdl = IntPtr.Zero, prf = IntPtr.Zero;
                 uint core_size = 0;
                 IntPtr[] native_core = new IntPtr[assumptions.Length];
                 r = (Z3_lbool)Native.Z3_check_assumptions(ctx.nCtx, 
                                    (uint)assumptions.Length, AST.ArrayToNative(assumptions),
-                                   ref model, ref proof, ref core_size, native_core);
+                                   ref mdl, ref prf, ref core_size, native_core);
 
                 for (uint i = 0; i < core_size; i++)
                     core.Add((BoolExpr)Expr.Create(ctx, native_core[i]));
+                if (mdl != IntPtr.Zero) {
+                    model = new Model(ctx, mdl);
+                }
+                if (prf != IntPtr.Zero) {
+                    proof = Expr.Create(ctx, prf);
+                }
 
             }
             switch (r)
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 1ea185530..16aaaf9b1 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -1148,18 +1148,21 @@ namespace datalog {
             utbv& neg = d->neg();
             unsigned mid = dm1.num_tbits();
             unsigned hi  = dm.num_tbits();
-            tbm.set(pos,d1.pos(), mid-1, 0);
-            tbm.set(pos,d2.pos(), hi-1, mid);
+            tbm.set(pos, d1.pos(), mid-1, 0);
+            tbm.set(pos, d2.pos(), hi-1, mid);
             for (unsigned i = 0; i < d1.neg().size(); ++i) {
                 t = tbm.allocateX();
                 tbm.set(*t, d1.neg()[i], mid-1, 0);
+                VERIFY(tbm.set_and(*t, pos));
                 neg.push_back(t.detach());
             }
             for (unsigned i = 0; i < d2.neg().size(); ++i) {
                 t = tbm.allocateX();
                 tbm.set(*t, d2.neg()[i], hi-1, mid);
+                VERIFY(tbm.set_and(*t, pos));
                 neg.push_back(t.detach());
             }
+            SASSERT(dm.well_formed(*d));
             return d.detach();
         }