diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index df97e0d52..ebe537d21 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -540,12 +540,10 @@ class rewrite_fn {
             return none_expr();
         cs_seq.linearize(cs);
         unifier_config cfg;
+        cfg.m_discard = true;
         unify_result_seq rseq = unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), m_subst, cfg);
         if (auto p = rseq.pull()) {
             substitution new_subst     = p->first.first;
-            constraints  new_postponed = p->first.second;
-            if (new_postponed)
-                return none_expr(); // all constraints must be solved
             new_e   = new_subst.instantiate_all(new_e);
             if (has_expr_metavar_strict(new_e))
                 return none_expr(); // new expressions was not completely instantiated
@@ -738,13 +736,11 @@ class rewrite_fn {
                 return unify_result();
             cs_seq.linearize(cs);
             unifier_config cfg;
-            cfg.m_conservative    = false;
+            cfg.m_conservative = false;
+            cfg.m_discard      = true;
             unify_result_seq rseq = unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), m_subst, cfg);
             if (auto p = rseq.pull()) {
                 substitution new_subst     = p->first.first;
-                constraints  new_postponed = p->first.second;
-                if (new_postponed)
-                    return unify_result(); // all constraints must be solved
                 rule      = new_subst.instantiate_all(rule);
                 rule_type = new_subst.instantiate_all(rule_type);
                 if (has_expr_metavar_strict(rule) || has_expr_metavar_strict(rule_type))
diff --git a/tests/lean/run/rewriter11.lean b/tests/lean/run/rewriter11.lean
new file mode 100644
index 000000000..674bc80b3
--- /dev/null
+++ b/tests/lean/run/rewriter11.lean
@@ -0,0 +1,18 @@
+import algebra.ring
+open algebra eq.ops
+
+variable {A : Type}
+
+theorem zero_mul1 [s : ring A] (a : A) : 0 * a = 0 :=
+have H : 0 * a + 0 = 0 * a + 0 * a,
+  begin
+    rewrite add_zero,
+    rewrite -(add_zero 0) at {1},
+    rewrite right_distrib
+  end,
+show 0 * a = 0, from (add.left_cancel H)⁻¹
+
+theorem zero_mul2 [s : ring A] (a : A) : 0 * a = 0 :=
+have H : 0 * a + 0 = 0 * a + 0 * a,
+  by rewrite [add_zero, -(add_zero 0) at {1}, right_distrib],
+show 0 * a = 0, from (add.left_cancel H)⁻¹