diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index d03b6c445..05c128cd6 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -86,7 +86,6 @@ namespace api {
 
         m_error_code = Z3_OK;
         m_print_mode = Z3_PRINT_SMTLIB_FULL;
-        m_searching  = false;
         
 
         m_interruptable = nullptr;
@@ -156,12 +155,6 @@ namespace api {
         }
     }
 
-    void context::check_searching() {
-        if (m_searching) { 
-            set_error_code(Z3_INVALID_USAGE, "cannot use function while searching"); // TBD: error code could be fixed.
-        } 
-    }
-
     char * context::mk_external_string(char const * str) {
         m_string_buffer = str?str:"";
         return const_cast<char *>(m_string_buffer.c_str());
diff --git a/src/api/api_context.h b/src/api/api_context.h
index d0f31c589..6a0ac588e 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -114,7 +114,6 @@ namespace api {
         Z3_error_code              m_error_code;
         Z3_error_handler *         m_error_handler;
         std::string                m_exception_msg; // catch the message associated with a Z3 exception
-        bool                       m_searching;
         Z3_ast_print_mode          m_print_mode;
 
         event_handler *            m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt
@@ -170,8 +169,6 @@ namespace api {
         void set_error_code(Z3_error_code err, char const* opt_msg);
         void set_error_code(Z3_error_code err, std::string &&opt_msg);
         void set_error_handler(Z3_error_handler h) { m_error_handler = h; }
-        // Sign an error if solver is searching
-        void check_searching();
 
         unsigned add_object(api::object* o);
         void del_object(api::object* o);
@@ -259,7 +256,6 @@ inline api::context * mk_c(Z3_context c) { return reinterpret_cast<api::context*
 #define SET_ERROR_CODE(ERR, MSG) { mk_c(c)->set_error_code(ERR, MSG); }
 #define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == 0) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is null"); return _ret_; } }
 #define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "not a valid ast"); return _ret_; } }
-#define CHECK_SEARCHING(c) mk_c(c)->check_searching();
 inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); }
 #define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == 0 || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not an expression"); return _ret_; } }
 inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); }
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 6d6f01ddb..2b590c070 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -736,7 +736,6 @@ extern "C" {
         LOG_Z3_get_implied_equalities(c, s, num_terms, terms, class_ids);
         ast_manager& m = mk_c(c)->m();
         RESET_ERROR_CODE();
-        CHECK_SEARCHING(c);
         init_solver(c, s);
         lbool result = smt::implied_equalities(m, *to_solver_ref(s), num_terms, to_exprs(num_terms, terms), class_ids);
         return static_cast<Z3_lbool>(result); 
@@ -752,7 +751,6 @@ extern "C" {
         LOG_Z3_solver_get_consequences(c, s, assumptions, variables, consequences);
         ast_manager& m = mk_c(c)->m();
         RESET_ERROR_CODE();
-        CHECK_SEARCHING(c);
         init_solver(c, s);
         expr_ref_vector _assumptions(m), _consequences(m), _variables(m);
         ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions);