check for m.get_sort(lhs->get_owner()) == m.get_sort(rhs->get_owner()…

…) in equality propagation Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Z3Prover · Jun 22, 2020 · 6ced699 · 6ced699
1 parent 4b6ca6a
commit 6ced699
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git 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
@@ -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)