#6289

Z3Prover · Aug 21, 2022 · be0cd74 · be0cd74
1 parent 2181a0f
commit be0cd74
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -1241,6 +1241,7 @@ class theory_lra::imp {
         context& c = ctx();
         if (!k.is_zero()) {
             mk_axiom(eq);
+            m_arith_eq_adapter.mk_axioms(th.ensure_enode(mod_r), th.ensure_enode(p));
             mk_axiom(mk_literal(a.mk_ge(mod, zero)));
             mk_axiom(mk_literal(a.mk_le(mod, upper)));