mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

Don't reset m_is_var in project

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-12 13:41:45 -07:00
parent 5e198f4119
commit b246389267
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/qe/qe_term_graph.cpp
View file

@ -185,9 +185,9 @@ namespace qe {
bool term_graph::is_variable_proc::operator()(const expr * e) const { bool term_graph::is_variable_proc::operator()(const expr * e) const {
if (!is_app(e)) return false; if (!is_app(e)) return false;
const app *a = ::to_app(e); const app *a = ::to_app(e);
return return
a->get_family_id() == null_family_id && a->get_family_id() == null_family_id &&
!m_solved.contains(a->get_decl()) && !m_solved.contains(a->get_decl()) &&
m_exclude == m_decls.contains(a->get_decl()); m_exclude == m_decls.contains(a->get_decl());
} }
@ -774,13 +774,14 @@ namespace qe {
} }
expr_ref_vector term_graph::project() { expr_ref_vector term_graph::project() {
// reset solved vars so that they are not considered pure by projector
m_is_var.reset_solved(); m_is_var.reset_solved();
projector p(*this); projector p(*this);
m_is_var.reset();
return p.project(); return p.project();
} }
expr_ref_vector term_graph::solve() { expr_ref_vector term_graph::solve() {
// reset solved vars so that they are not considered pure by projector
m_is_var.reset_solved(); m_is_var.reset_solved();
projector p(*this); projector p(*this);
return p.solve(); return p.solve();