From 1fc9a7ba84c2824bbb9cba64d2ef279250ecb9df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Mar 2021 17:43:12 -0700 Subject: [PATCH] fix regression, fix #5115 --- src/smt/smt_internalizer.cpp | 3 +++ src/smt/theory_lra.cpp | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) 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); }