fix #6635

Z3Prover · Mar 22, 2023 · 03a4480 · 03a4480
1 parent 2683a2d
commit 03a4480
Showing 1 changed file with 8 additions and 4 deletions.
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -436,13 +436,19 @@ class theory_lra::imp {
                     if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod);
                     if (m_nla && !a.is_numeral(n2)) {
                         // shortcut to create non-linear division axioms.
+                        internalize_term(to_app(n));
+                        internalize_term(to_app(n1));
+                        internalize_term(to_app(n2));
                         theory_var q = mk_var(n);
                         theory_var x = mk_var(n1);
                         theory_var y = mk_var(n2);
                         m_nla->add_idivision(register_theory_var_in_lar_solver(q), register_theory_var_in_lar_solver(x), register_theory_var_in_lar_solver(y));
                     }
                     if (a.is_numeral(n2) && a.is_bounded(n1)) {
                         ensure_nla();
+                        internalize_term(to_app(n));
+                        internalize_term(to_app(n1));
+                        internalize_term(to_app(n2));
                         theory_var q = mk_var(n);
                         theory_var x = mk_var(n1);
                         theory_var y = mk_var(n2);
@@ -1512,11 +1518,9 @@ class theory_lra::imp {
             } 
         }
         TRACE("arith", 
-              for (theory_var v = 0; v < sz; ++v) {
-                  if (th.is_relevant_and_shared(get_enode(v))) { 
+              for (theory_var v = 0; v < sz; ++v) 
+                  if (th.is_relevant_and_shared(get_enode(v)))  
                       tout << "v" << v << " ";
-                  }
-              }
               tout << "\n"; );
         if (!vars.empty()) {
             lp().random_update(vars.size(), vars.data());