From 37f6364547a473ab84008848ef25d0d07cc27e50 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 May 2020 16:03:05 -0700 Subject: [PATCH] fix #4103 --- src/smt/theory_diff_logic_def.h | 7 ++++--- src/smt/theory_utvpi_def.h | 2 +- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 31ec2bce1..6fba631de 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -889,6 +889,7 @@ void theory_diff_logic::reset_eh() { template void theory_diff_logic::compute_delta() { m_delta = rational(1); + m_graph.set_to_zero(get_zero(true), get_zero(false)); unsigned num_edges = m_graph.get_num_edges(); for (unsigned i = 0; i < num_edges; ++i) { if (!m_graph.is_enabled(i)) { @@ -903,12 +904,12 @@ void theory_diff_logic::compute_delta() { rational k_y = m_graph.get_assignment(src).get_infinitesimal().to_rational(); rational n_c = w.get_rational().to_rational(); rational k_c = w.get_infinitesimal().to_rational(); - TRACE("epsilon", tout << "(n_x,k_x): " << n_x << ", " << k_x << ", (n_y,k_y): " + TRACE("arith", tout << "(n_x,k_x): " << n_x << ", " << k_x << ", (n_y,k_y): " << n_y << ", " << k_y << ", (n_c,k_c): " << n_c << ", " << k_c << "\n";); if (n_x < n_y + n_c && k_x > k_y + k_c) { - rational new_delta = (n_y + n_c - n_x) / (k_x - k_y - k_c); + rational new_delta = (n_y + n_c - n_x) / (2*(k_x - k_y - k_c)); if (new_delta < m_delta) { - TRACE("epsilon", tout << "new delta: " << new_delta << "\n";); + TRACE("arith", tout << "new delta: " << new_delta << "\n";); m_delta = new_delta; } } diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index d85b5fbf2..28d3ef194 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -969,7 +969,7 @@ namespace smt { if (eps_r.is_pos()) { rational num_r = -b.get_rational(); SASSERT(num_r.is_pos()); - rational new_delta = num_r/eps_r; + rational new_delta = num_r/2*eps_r; if (new_delta < m_delta) { m_delta = new_delta; }