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); }