diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 6b86e718c..bc0e9342c 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -392,6 +392,8 @@ namespace smt { template final_check_status theory_dense_diff_logic::final_check_eh() { + //fix_zero(); + //compute_epsilon(); init_model(); if (assume_eqs(m_var_value_table)) return FC_CONTINUE; @@ -768,7 +770,7 @@ namespace smt { */ template void theory_dense_diff_logic::compute_epsilon() { - m_epsilon = rational(1); + m_epsilon = rational(1, 2); typename edges::const_iterator it = m_edges.begin(); typename edges::const_iterator end = m_edges.end(); // first edge is null