diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 025ec76d1..1e4bc1b96 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -934,8 +934,8 @@ bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
         new_lower    = alloc(derived_bound, v, inf_numeral(k), B_LOWER);
         new_upper    = alloc(derived_bound, v, inf_numeral(k), B_UPPER);
     }
-    SASSERT(new_lower != 0);
-    SASSERT(new_upper != 0);
+    SASSERT(new_lower);
+    SASSERT(new_upper);
     m_bounds_to_delete.push_back(new_lower);
     m_asserted_bounds.push_back(new_lower);
     m_bounds_to_delete.push_back(new_upper);
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index 48414e629..076fefda1 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -677,7 +677,10 @@ namespace smt {
 
     template<typename Ext>
     bool theory_utvpi<Ext>::enable_edge(edge_id id) {
-        return (id == null_edge_id) || (m_graph.enable_edge(id) && m_graph.enable_edge(id+1));
+        return 
+            (id == null_edge_id) || 
+            (m_graph.enable_edge(id) && m_graph.enable_edge(id+1)) ||
+            m_non_utvpi_exprs;
     }
 
     template<typename Ext>