diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 40858e3f4..37306cb3d 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -602,6 +602,9 @@ namespace smt {
         m_app2enode.setx(q->get_id(), get_enode(lam_name), nullptr);
         m_l_internalized_stack.push_back(q);
         m_trail_stack.push_back(&m_mk_lambda_trail);
+        bool_var bv = get_bool_var(fa);
+        assign(literal(bv, false), nullptr);
+        mark_as_relevant(bv);
     }
 
     /**
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index b64e95ba7..85faee01f 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -450,7 +450,7 @@ class theory_lra::imp {
                     st.to_ensure_var().push_back(n1);
                     st.to_ensure_var().push_back(n2);
                 }
-                if (a.is_idiv0(n, n1, n2) || a.is_mod0(n, n1, n2) || a.is_rem0(n, n1, n2)) {
+                else if (a.is_idiv0(n, n1, n2) || a.is_mod0(n, n1, n2) || a.is_rem0(n, n1, n2)) {
                     st.to_ensure_var().push_back(n1);
                     st.to_ensure_var().push_back(n2);       
                 }