From 3faca52c400f090062b69f8d6218a2cc5129d3ef Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 8 Nov 2022 14:17:17 -0800
Subject: [PATCH] re-enable new solve_eqs with bug fixes

---
 src/ast/simplifiers/extract_eqs.cpp      | 2 ++
 src/tactic/core/solve_eqs2_tactic.h      | 4 ++--
 src/tactic/core/solve_eqs_tactic.h       | 4 ++--
 src/tactic/dependent_expr_state_tactic.h | 6 +++---
 4 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp
index 775eb4d22..d65f9b167 100644
--- a/src/ast/simplifiers/extract_eqs.cpp
+++ b/src/ast/simplifiers/extract_eqs.cpp
@@ -192,6 +192,8 @@ namespace euf {
                 ++i;
                 if (!is_uninterp_const(arg))
                     continue;
+                if (!a.is_real(arg))
+                    continue;
                 unsigned j = 0;
                 bool nonzero = true;
                 for (expr* arg2 : *to_app(x)) {
diff --git a/src/tactic/core/solve_eqs2_tactic.h b/src/tactic/core/solve_eqs2_tactic.h
index 34c0befa4..7d13b571e 100644
--- a/src/tactic/core/solve_eqs2_tactic.h
+++ b/src/tactic/core/solve_eqs2_tactic.h
@@ -33,7 +33,7 @@ inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p = param
     return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs");
 }
 
-#if 0
+#if 1
 inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) {
     return mk_solve_eqs2_tactic(m, p);
 }
@@ -41,7 +41,7 @@ inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = para
 
 
 /*
-  ADD_TACTIC("solve-eqs", "solve for variables.", "mk_solve_eqs2_tactic(m, p)")
+  ADD_TACTIC("solve-eqs2", "solve for variables.", "mk_solve_eqs2_tactic(m, p)")
 */
 
 
diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h
index 29c11a9c3..7b97172a3 100644
--- a/src/tactic/core/solve_eqs_tactic.h
+++ b/src/tactic/core/solve_eqs_tactic.h
@@ -24,14 +24,14 @@ class tactic;
 
 tactic * mk_solve_eqs1_tactic(ast_manager & m, params_ref const & p = params_ref());
 
-#if 1
+#if 0
 inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) {
     return mk_solve_eqs1_tactic(m, p);
 }
 #endif
 
 /*
-  ADD_TACTIC("solve-eqs1", "eliminate variables by solving equations.", "mk_solve_eqs1_tactic(m, p)")
+  ADD_TACTIC("solve-eqs", "eliminate variables by solving equations.", "mk_solve_eqs1_tactic(m, p)")
 */
 
 
diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
index 24f12aeae..4b89028f3 100644
--- a/src/tactic/dependent_expr_state_tactic.h
+++ b/src/tactic/dependent_expr_state_tactic.h
@@ -86,13 +86,13 @@ public:
 
     void operator()(goal_ref const & in, 
                     goal_ref_buffer & result) override {
-        if (in->proofs_enabled())
-            throw tactic_exception("tactic does not support low level proofs");
         init();
         statistics_report sreport(*this);
         tactic_report report(name(), *in);
         m_goal = in.get();
-        m_simp->reduce();
+        if (!in->proofs_enabled())
+            m_simp->reduce();
+        m_goal->elim_true();
         m_goal->inc_depth();
         if (in->models_enabled())
             in->add(m_model_trail->get_model_converter().get());