From 6ced6995d00690f4f513622b3e2772895ed347f5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 22 Jun 2020 11:48:46 -0700 Subject: [PATCH] check for m.get_sort(lhs->get_owner()) == m.get_sort(rhs->get_owner()) in equality propagation Signed-off-by: Lev Nachmanson --- src/math/lp/lp_bound_propagator.h | 4 +++- src/smt/theory_lra.cpp | 3 ++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 32bf1c86060..b3d58e5aee2 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -417,7 +417,9 @@ class lp_bound_propagator { TRACE("cheap_eq", tout << "reporting eq " << j << ", " << k << "\n"; for (auto p : exp) { lp().constraints().display(tout, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci()); - }); + } + tout << "theory_vars v" << lp().local_to_external(je) << " == v" << lp().local_to_external(ke) << "\n"; + ); m_imp.add_eq(je, ke, exp); lp().settings().stats().m_cheap_eqs++; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b2c73d40e68..f58b3dfc193 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2423,7 +2423,8 @@ class theory_lra::imp { theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form enode* n1 = get_enode(uv); enode* n2 = get_enode(vv); - if (n1->get_root() == n2->get_root()) + if (n1->get_root() == n2->get_root() || + m.get_sort(n1->get_owner()) != m.get_sort(n2->get_owner())) return; reset_evidence(); for (auto const& ev : e)