From 03a44803b6da631cf7d3773319685e0c0f9fb0da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Mar 2023 13:38:02 +0100 Subject: [PATCH] fix #6635 --- src/smt/theory_lra.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 3eda1ddff..568143d36 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -436,6 +436,9 @@ 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); @@ -443,6 +446,9 @@ class theory_lra::imp { } 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 @@ public: } } 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());