From 9ef78fcfa7b6163b18827a208dd2b0a1cc3210b0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Nov 2022 13:57:58 -0800 Subject: [PATCH] revert new solve-eqs Signed-off-by: Nikolaj Bjorner --- src/tactic/core/solve_eqs2_tactic.h | 2 +- src/tactic/core/solve_eqs_tactic.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/core/solve_eqs2_tactic.h b/src/tactic/core/solve_eqs2_tactic.h index fa095aad0c3..34c0befa431 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 1 +#if 0 inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) { return 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 4b26254a0f2..29c11a9c341 100644 --- a/src/tactic/core/solve_eqs_tactic.h +++ b/src/tactic/core/solve_eqs_tactic.h @@ -24,7 +24,7 @@ class tactic; tactic * mk_solve_eqs1_tactic(ast_manager & m, params_ref const & p = params_ref()); -#if 0 +#if 1 inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) { return mk_solve_eqs1_tactic(m, p); }