euf-completion bug fix, streamline name to solve_eqs

Z3Prover · Nov 15, 2022 · 48c0f86 · 48c0f86
1 parent 3eeb59d
commit 48c0f86
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 12 deletions.
diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
@@ -90,7 +90,8 @@ namespace euf {
             return;
         }
 
-        for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+        unsigned sz = m_fmls.size();
+        for (unsigned i = m_qhead; i < sz; ++i) {
             auto [f, d] = m_fmls[i]();
 
             expr_dependency_ref dep(d, m);

diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h
@@ -22,26 +22,19 @@ Module Name:
 #include "ast/simplifiers/solve_eqs.h"
 
 
-class solve_eqs2_tactic_factory : public dependent_expr_simplifier_factory {
+class solve_eqs_tactic_factory : public dependent_expr_simplifier_factory {
 public:
     dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override {
         return alloc(euf::solve_eqs, m, s);
     }
 };
 
-inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p = params_ref()) {
-    return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs");
+inline tactic * mk_solve_eqs_tactic(ast_manager& m, params_ref const& p = params_ref()) {
+    return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs_tactic_factory), "solve-eqs");
 }
 
-#if 1
-inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) {
-    return mk_solve_eqs2_tactic(m, p);
-}
-#endif
-
-
 /*
-  ADD_TACTIC("solve-eqs", "solve for variables.", "mk_solve_eqs2_tactic(m, p)")
+  ADD_TACTIC("solve-eqs", "solve for variables.", "mk_solve_eqs_tactic(m, p)")
 */