mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 19:21:22 +00:00
Code Activity

fix #3531

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-29 11:15:01 -07:00
parent 1155db383e
commit 7086a7c26a
1 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/nlsat/nlsat_solver.cpp
View file

@ -1750,11 +1750,13 @@ namespace nlsat {
} }
void process_antecedent(literal antecedent) { void process_antecedent(literal antecedent) {
checkpoint();
bool_var b = antecedent.var(); bool_var b = antecedent.var();
TRACE("nlsat_resolve", display(tout << "resolving antecedent: ", antecedent) << "\n";); TRACE("nlsat_resolve", display(tout << "resolving antecedent: ", antecedent) << "\n";);
if (assigned_value(antecedent) == l_undef) { if (assigned_value(antecedent) == l_undef) {
checkpoint();
// antecedent must be false in the current arith interpretation // antecedent must be false in the current arith interpretation
SASSERT(value(antecedent) == l_false); SASSERT(value(antecedent) == l_false || m_rlimit.get_cancel_flag());
if (!is_marked(b)) { if (!is_marked(b)) {
SASSERT(is_arith_atom(b) && max_var(b) < m_xk); // must be in a previous stage SASSERT(is_arith_atom(b) && max_var(b) < m_xk); // must be in a previous stage
TRACE("nlsat_resolve", tout << "literal is unassigned, but it is false in arithmetic interpretation, adding it to lemma\n";); TRACE("nlsat_resolve", tout << "literal is unassigned, but it is false in arithmetic interpretation, adding it to lemma\n";);
@ -1832,15 +1834,16 @@ namespace nlsat {
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
literal l = m_lazy_clause[i]; literal l = m_lazy_clause[i];
if (l.var() != b) { if (l.var() != b) {
SASSERT(value(l) == l_false); SASSERT(value(l) == l_false || m_rlimit.get_cancel_flag());
} }
else { else {
SASSERT(value(l) == l_true); SASSERT(value(l) == l_true || m_rlimit.get_cancel_flag());
SASSERT(!l.sign() || m_bvalues[b] == l_false); SASSERT(!l.sign() || m_bvalues[b] == l_false);
SASSERT(l.sign() || m_bvalues[b] == l_true); SASSERT(l.sign() || m_bvalues[b] == l_true);
} }
} }
}); });
checkpoint();
resolve_clause(b, m_lazy_clause.size(), m_lazy_clause.c_ptr()); resolve_clause(b, m_lazy_clause.size(), m_lazy_clause.c_ptr());
for (unsigned i = 0; i < jst.num_clauses(); ++i) { for (unsigned i = 0; i < jst.num_clauses(); ++i) {
@ -1982,6 +1985,7 @@ namespace nlsat {
while (true) { while (true) {
found_decision = false; found_decision = false;
while (m_num_marks > 0) { while (m_num_marks > 0) {
checkpoint();
SASSERT(top > 0); SASSERT(top > 0);
trail & t = m_trail[top-1]; trail & t = m_trail[top-1];
SASSERT(t.m_kind != trail::NEW_STAGE); // we only mark literals that are in the same stage SASSERT(t.m_kind != trail::NEW_STAGE); // we only mark literals that are in the same stage