diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 1951d16ea..896d0ec85 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -397,6 +397,14 @@ extern "C" {
         Z3_CATCH;
     }
 
+    void Z3_API Z3_enable_concurrent_dec_ref(Z3_context c) {
+        Z3_TRY;
+        LOG_Z3_enable_concurrent_dec_ref(c);
+        mk_c(c)->enableset_concurrent_dec_ref();
+        Z3_CATCH;
+    }
+    
+
     void Z3_API Z3_toggle_warning_messages(bool enabled) {
         LOG_Z3_toggle_warning_messages(enabled);
         enable_warning_messages(enabled != 0);
diff --git a/src/api/api_context.h b/src/api/api_context.h
index 23b5d6f70..cf8c6ac87 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -172,8 +172,8 @@ 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; }
-
-        void set_concurrent_dec_ref() { m_concurrent_dec_ref = true; }
+        
+        void enable_concurrent_dec_ref() { m_concurrent_dec_ref = true; }
         unsigned add_object(api::object* o);
         void del_object(api::object* o);
         void dec_ref(ast* a);
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 36753a4f9..2fa4acc65 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -59,6 +59,7 @@ let mk_context (settings:(string * string) list) =
   Z3native.del_config cfg;
   Z3native.set_ast_print_mode res (Z3enums.int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT);
   Z3native.set_internal_error_handler res;
+  Z3native.enable_concurrent_dec_ref res;
   res
 
 module Symbol =
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 831e03b0e..2820205b9 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1705,6 +1705,16 @@ extern "C" {
     void Z3_API Z3_interrupt(Z3_context c);
 
 
+    /**
+       \brief use concurrency control for dec-ref. 
+       Reference counting decrements are allowed in separate threads from the context. 
+       If this setting is not invoked, reference counting decrements are not going to be thread safe.
+
+       def_API('Z3_enable_concurrent_dec_ref', VOID, (_in(CONTEXT),))
+     */
+    void Z3_API Z3_enable_concurrent_dec_ref(Z3_context c);
+    
+
     /**@}*/
 
     /** @name Parameters */