mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix #3167

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-07 14:49:18 +01:00
parent c765869d38
commit 983a552325
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/nlsat/nlsat_solver.cpp
View file

@ -2338,7 +2338,7 @@ namespace nlsat {
for (clause* c : m_clauses) {
if (has_root_atom(*c)) return false;
}
return true;
return m_patch_var.empty();
}
/**
@ -2660,7 +2660,7 @@ namespace nlsat {
m_pm.eval(q, m_assignment, qv);
val = qv / pv;
TRACE("nlsat",
m_display_var(tout << "patch ", v) << "\n";
m_display_var(tout << "patch v" << v << " ", v) << "\n";
if (m_assignment.is_assigned(v)) m_am.display(tout << "previous value: ", m_assignment.value(v)); tout << "\n";
m_am.display(tout << "updated value: ", val); tout << "\n";
);
@ -2677,6 +2677,7 @@ namespace nlsat {
unsigned num_atoms = m_atoms.size();
for (unsigned j = 0; j < num_atoms; ++j) {
atom* a = m_atoms[j];
if (a && a->is_ineq_atom()) {
ineq_atom const& a1 = *to_ineq_atom(a);
unsigned sz = a1.size();
@ -2697,7 +2698,7 @@ namespace nlsat {
}
}
if (!change) continue;
literal l = mk_ineq_literal(a1.get_kind(), ps.size(), ps.c_ptr(), even.c_ptr());
literal l = mk_ineq_literal(a1.get_kind(), ps.size(), ps.c_ptr(), even.c_ptr());
if (a1.m_bool_var != l.var()) {
b2l.insert(a1.m_bool_var, l);
inc_ref(l);