mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

#5753

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-12 12:49:06 -08:00
parent 56d3718cde
commit 10dc8d7313
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/q_solver.cpp
View file

@ -65,6 +65,7 @@ namespace q {
} }
sat::check_result solver::check() { sat::check_result solver::check() {
std::cout << "check\n";
if (ctx.get_config().m_ematching && m_ematch()) if (ctx.get_config().m_ematching && m_ematch())
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
@ -230,10 +231,9 @@ namespace q {
bool solver::expand(quantifier* q) { bool solver::expand(quantifier* q) {
expr_ref r(q, m); expr_ref r(q, m);
proof_ref pr(m); proof_ref pr(m);
ctx.rewrite(r);
m_der(r, r, pr); m_der(r, r, pr);
m_expanded.reset(); m_expanded.reset();
if (r != q) { if (q != r) {
ctx.rewrite(r); ctx.rewrite(r);
m_expanded.push_back(r); m_expanded.push_back(r);
return true; return true;