diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp
index 812b79740..75ec17dd4 100644
--- a/src/smt/tactic/unit_subsumption_tactic.cpp
+++ b/src/smt/tactic/unit_subsumption_tactic.cpp
@@ -40,8 +40,9 @@ struct unit_subsumption_tactic : public tactic {
     void cleanup() override {}
 
     void operator()(/* in */  goal_ref const & in, 
-                    /* out */ goal_ref_buffer & result) override {     
-        fail_if_proof_generation("unit-subsumption", in);
+                    /* out */ goal_ref_buffer & result) override {  
+        tactic_report report("unit-subsume-simplify", *in);
+        fail_if_proof_generation("unit-subsume-simplify", in);
         reduce_core(in, result);
     }
 
@@ -76,7 +77,8 @@ struct unit_subsumption_tactic : public tactic {
 
     void assert_clauses(goal_ref const& g) {
         for (unsigned i = 0; i < g->size(); ++i) {
-            m_context.assert_expr(m.mk_iff(new_clause(), g->form(i)));
+            expr_ref fml(m.mk_iff(new_clause(), g->form(i)), m);
+            m_context.assert_expr(fml);
         }
     }