mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

fix #4103

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-02 16:03:05 -07:00
parent 09d881cce5
commit 37f6364547
2 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_diff_logic_def.h
View file

@ -889,6 +889,7 @@ void theory_diff_logic<Ext>::reset_eh() {
template<typename Ext>
void theory_diff_logic<Ext>::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<Ext>::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;
}
}

2
src/smt/theory_utvpi_def.h
View file

@ -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;
}