From f1f974638ddd1fbf3bbaa39ccd564051b350af99 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Mar 2020 15:29:37 -0700 Subject: [PATCH] track variables used by nla_solver Signed-off-by: Nikolaj Bjorner --- src/math/dd/pdd_interval.h | 1 + src/smt/theory_lra.cpp | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h index 2972e0086..d797bb8b6 100644 --- a/src/math/dd/pdd_interval.h +++ b/src/math/dd/pdd_interval.h @@ -59,6 +59,7 @@ public: m_dep_intervals.mul(hi, a, t); m_dep_intervals.add(t, lo, ret); } + m().del(a); } // f meant to be called when the separation happens template diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 3c56127eb..c5cb34e8b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -687,7 +687,7 @@ class theory_lra::imp { } } - TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n";); + TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n" << vars << "\n";); if (!_has_var) { m_solver->register_existing_terms(); m_switcher.add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());