diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp
index 75ec17dd4..4cbe425c4 100644
--- a/src/smt/tactic/unit_subsumption_tactic.cpp
+++ b/src/smt/tactic/unit_subsumption_tactic.cpp
@@ -15,6 +15,7 @@ Author:
 
 --*/
 
+#include "ast/ast_util.h"
 #include "smt/tactic/unit_subsumption_tactic.h"
 #include "smt/smt_context.h"
 
@@ -92,7 +93,8 @@ struct unit_subsumption_tactic : public tactic {
         m_context.push();
         for (unsigned j = 0; j < m_clause_count; ++j) {
             if (i == j) {
-                m_context.assert_expr(m.mk_not(m_clauses.get(j)));
+                expr_ref fml(mk_not(m, m_clauses.get(j)), m);
+                m_context.assert_expr(fml);
             }
             else if (!m_is_deleted.get(j)) {
                 m_context.assert_expr(m_clauses.get(j));
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index f1ebd2e7c..5179ecbbc 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -737,6 +737,7 @@ namespace smt {
      */
     template<typename Ext>
     void theory_utvpi<Ext>::enforce_parity() {
+        SASSERT(m_graph.is_feasible());
         unsigned_vector todo;        
         unsigned sz = get_num_vars();
         for (unsigned i = 0; i < sz; ++i) {
@@ -774,6 +775,7 @@ namespace smt {
                   }
                   display(tout);
                   );
+            SASSERT(m_graph.is_feasible());
 
             for (auto v : zero_v) {                
                 m_graph.inc_assignment(v, numeral(-1));
@@ -782,8 +784,8 @@ namespace smt {
                     todo.push_back(k);
                 }
             }         
+            TRACE("utvpi", display(tout););
         }
-        SASSERT(m_graph.is_feasible());
         DEBUG_CODE(
             for (unsigned i = 0; i < sz; ++i) {
                 enode* e = get_enode(i);
@@ -792,6 +794,7 @@ namespace smt {
                     UNREACHABLE();
                 }            
             });
+        SASSERT(m_graph.is_feasible());
     }