From 0af249d651656048d569239edfe0e1d2f8d46723 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Aug 2019 13:44:07 -0700 Subject: [PATCH] 'na Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 5 ----- src/tactic/core/elim_uncnstr_tactic.cpp | 1 + 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 00b6260fc..1ceff2391 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2005,11 +2005,6 @@ public: } bool can_propagate() { -#if 0 - if (ctx().at_base_level() && has_delayed_constraints()) { - // we could add the delayed constraints here directly to the tableau instead of using bounds variables. - } -#endif return m_asserted_atoms.size() > m_asserted_qhead; } diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index bca13366f..c26e7b9eb 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -93,6 +93,7 @@ class elim_uncnstr_tactic : public tactic { } v = m().mk_fresh_const(nullptr, m().get_sort(t)); + std::cout << mk_pp(t, m()) << " -> " << mk_pp(v, m()) << "\n"; TRACE("elim_uncnstr_bug", tout << "eliminating:\n" << mk_ismt2_pp(t, m()) << "\n";); TRACE("elim_uncnstr_bug_ll", tout << "eliminating:\n" << mk_bounded_pp(t, m()) << "\n";); m_fresh_vars.push_back(v);