From b246389267eba16a14415650f41c91b0eddef301 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Tue, 12 Jun 2018 13:41:45 -0700
Subject: [PATCH] Don't reset m_is_var in project

---
 src/qe/qe_term_graph.cpp | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp
index d4cde6b4f..82b6e9d2e 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/qe_term_graph.cpp
@@ -185,9 +185,9 @@ namespace qe {
     bool term_graph::is_variable_proc::operator()(const expr * e) const {
         if (!is_app(e)) return false;
         const app *a = ::to_app(e);
-        return 
+        return
             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());
     }
 
@@ -774,13 +774,14 @@ namespace qe {
     }
 
     expr_ref_vector term_graph::project() {
+        // reset solved vars so that they are not considered pure by projector
         m_is_var.reset_solved();
         projector p(*this);
-        m_is_var.reset();
         return p.project();
     }
 
     expr_ref_vector term_graph::solve() {
+        // reset solved vars so that they are not considered pure by projector
         m_is_var.reset_solved();
         projector p(*this);
         return p.solve();