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 #4195

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-03 10:55:38 -07:00
parent 91a190a785
commit fcab7e4f9c
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_utvpi_def.h
View file

@ -853,6 +853,7 @@ namespace smt {
CTRACE("utvpi", !ok,
tout << "validation failed:\n";
tout << "Assignment: " << assign << "\n";
tout << mk_pp(e, get_manager()) << "\n";
a.display(*this, tout);
tout << "\n";
display(tout);
@ -915,7 +916,7 @@ namespace smt {
template<typename Ext>
rational theory_utvpi<Ext>::mk_value(th_var v, bool is_int) {
rational theory_utvpi<Ext>::mk_value(th_var v, bool is_int) {
SASSERT(v != null_theory_var);
numeral val1 = m_graph.get_assignment(to_var(v));
numeral val2 = m_graph.get_assignment(neg(to_var(v)));
@ -945,7 +946,7 @@ namespace smt {
template<typename Ext>
void theory_utvpi<Ext>::compute_delta() {
m_delta = rational(1);
m_delta = rational(1,4);
unsigned sz = m_graph.get_num_edges();
for (unsigned i = 0; i < sz; ++i) {
@ -969,7 +970,7 @@ namespace smt {
if (eps_r.is_pos()) {
rational num_r = -b.get_rational();
SASSERT(num_r.is_pos());
rational new_delta = num_r/2*eps_r;
rational new_delta = num_r/4*eps_r;
if (new_delta < m_delta) {
m_delta = new_delta;
}