mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

(partial) fix #3788

Browse source 
Fixes a bug in computation of implicants inside spacer.
The instance now returns `unknown`. The root cause is the difference in what
proofs are in spacer and SMT. Spacer returns a proof of query, but horn_tactic
expects a proof of FALSE.
This commit is contained in:
Arie Gurfinkel 2020-04-10 12:26:31 -04:00
parent 44302f3f2a
commit b1b77e57e1
2 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz/spacer/spacer_sat_answer.cpp
View file

@ -127,8 +127,14 @@ void ground_sat_answer_op::mk_children(frame &fr, vector<frame> &todo) {
m_solver->assert_expr(fr.pt().transition()); m_solver->assert_expr(fr.pt().transition());
m_solver->assert_expr(fr.pt().rule2tag(&r)); m_solver->assert_expr(fr.pt().rule2tag(&r));
TRACE("spacer_sat",
tout << "Solver in mk_children\n";
m_solver->display(tout) << "\n";);
lbool res = m_solver->check_sat(0, nullptr); lbool res = m_solver->check_sat(0, nullptr);
(void)res; (void)res;
CTRACE("spacer_sat", res != l_true,
tout << "Result: " << res << "\n";);
VERIFY(res == l_true); VERIFY(res == l_true);
model_ref mdl; model_ref mdl;

7
src/muz/spacer/spacer_util.cpp
View file

@ -496,15 +496,16 @@ namespace {
SASSERT(m_todo.empty()); SASSERT(m_todo.empty());
if (m_visited.is_marked(e) || !is_app(e)) return; if (m_visited.is_marked(e) || !is_app(e)) return;
m_todo.reset();
m_todo.push_back(e); m_todo.push_back(e);
for (unsigned i = 0; i < m_todo.size(); ++i) { while(!m_todo.empty()) {
e = m_todo.back(); e = m_todo.back();
m_todo.pop_back();
if (!is_app(e)) continue; if (!is_app(e)) continue;
app* a = to_app(e); app* a = to_app(e);
m_todo.pop_back();
process_app(a, out); process_app(a, out);
m_visited.mark(a, true); m_visited.mark(a, true);
} }
m_todo.reset(); m_todo.reset();
} }