fix regression, fix #5115

Z3Prover · Mar 31, 2021 · 1fc9a7b · 1fc9a7b
1 parent 1fcd537
commit 1fc9a7b
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git 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
@@ -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);       
                 }