diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp
index c6cd1020e..5e8a687c7 100644
--- a/src/cmd_context/extra_cmds/dbg_cmds.cpp
+++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp
@@ -429,6 +429,8 @@ public:
         params_ref p;
         solver_ref sA = sf(m, p, false /* no proofs */, true, true, symbol::null);
         solver_ref sB = sf(m, p, false /* no proofs */, true, true, symbol::null);
+        sA->assert_expr(a);
+        sB->assert_expr(b);
         qe::prop_mbi_plugin pA(sA.get());
         qe::prop_mbi_plugin pB(sB.get());
         lbool res = mbi.binary(pA, pB, vars, itp);
diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index f149af764..8be15ed7f 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -104,6 +104,7 @@ namespace qe {
     /** --------------------------------------------------------------
      * ping-pong interpolation of Gurfinkel & Vizel
      * compute a binary interpolant.
+     * TBD: also implement the one-sided versions that create clausal interpolants.
      */
     lbool interpolator::binary(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp) {
         ast_manager& m = vars.get_manager();
@@ -126,14 +127,18 @@ namespace qe {
                     itp = nullptr;
                     return l_true;
                 }
+                TRACE("mbi", tout << "new lits " << lits << "\n";);
                 break; // continue
             case mbi_unsat: {
                 if (lits.empty()) {
-                    itp = mk_and(itps[turn]);
+                    // TBD, either a => itp and itp => !b 
+                    // or          b => itp and itp => !a
+                    itp = mk_and(itps[!turn]);
                     return l_false;
                 }
                 t2->block(lits);
                 expr_ref lemma(mk_not(mk_and(lits)));
+                TRACE("mbi", tout << lemma << "\n";);
                 blocks[turn].push_back(lemma);
                 itp = m.mk_implies(mk_and(blocks[!turn]), lemma);
                 // TBD: compute closure over variables not in vars
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 8dec3335e..b60a9db71 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3061,7 +3061,7 @@ namespace smt {
 
     bool context::reduce_assertions() {
         if (!m_asserted_formulas.inconsistent()) {
-            SASSERT(at_base_level());
+            // SASSERT(at_base_level());
             m_asserted_formulas.reduce();
         }
         return m_asserted_formulas.inconsistent();