From 427b5ef0025ba99f0ab27a3d03be531913e3733f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 30 Nov 2017 11:20:19 -0800
Subject: [PATCH] set eliminated to false on literals used in clauses

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_elim_eqs.cpp    | 2 +-
 src/sat/sat_solver.h        | 1 +
 src/sat/tactic/goal2sat.cpp | 1 +
 src/solver/solver.cpp       | 4 ++--
 4 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index cb659247f..ea44c870d 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -96,7 +96,7 @@ namespace sat {
             // apply substitution
             for (i = 0; i < sz; i++) {                
                 c[i] = norm(roots, c[i]);
-				VERIFY(c[i] == norm(roots, c[i]));
+                VERIFY(c[i] == norm(roots, c[i]));
                 VERIFY(!m_solver.was_eliminated(c[i].var()));
             }
             std::sort(c.begin(), c.end());
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 0d65de1e1..7cadffd27 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -266,6 +266,7 @@ namespace sat {
         void set_external(bool_var v);
         void set_non_external(bool_var v);
         bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
+        void set_eliminated(bool_var v, bool f) { m_eliminated[v] = f; }
         unsigned scope_lvl() const { return m_scope_lvl; }
         unsigned search_lvl() const { return m_search_lvl; }
         bool  at_search_lvl() const { return m_scope_lvl == m_search_lvl; }
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 648bd3cf1..3e2abf8e8 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -151,6 +151,7 @@ struct goal2sat::imp {
         else {
             SASSERT(v != sat::null_bool_var);
             l = sat::literal(v, sign);
+            m_solver.set_eliminated(v, false);
         }
         SASSERT(l != sat::null_literal);
         if (root)
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 606c32bed..43ca9870a 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -204,12 +204,12 @@ void solver::assert_expr(expr* f, expr* t) {
 }
 
 void solver::collect_param_descrs(param_descrs & r) {
-    r.insert("solver.enforce_model_conversion", CPK_BOOL, "(default: true) enforce model conversion when asserting formulas");
+    r.insert("solver.enforce_model_conversion", CPK_BOOL, "(default: false) enforce model conversion when asserting formulas");
 }
 
 void solver::updt_params(params_ref const & p) { 
     m_params.copy(p); 
-    m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", true);
+    m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", false);
 }
 
 void solver::hoist_converter(model_converter_ref& mc) {