diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index d249649c7..ae002f979 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -35,7 +35,6 @@ theory_str::theory_str(ast_manager & m):
 		opt_LCMUnrollStep(2),
 		opt_NoQuickReturn_IntegerTheory(false),
 		opt_DisableIntegerTheoryIntegration(false),
-		opt_NoCheckRegexIn(false),
         /* Internal setup */
         search_started(false),
         m_autil(m),
@@ -1645,12 +1644,8 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) {
     }
 
     if (!regex_in_bool_map.empty()) {
-        if (opt_NoCheckRegexIn) {
-            TRACE("t_str", tout << "WARNING: skipping check_regex_in()" << std::endl;);
-        } else {
-            TRACE("t_str", tout << "checking regex consistency" << std::endl;);
-            check_regex_in(lhs, rhs);
-        }
+        TRACE("t_str", tout << "checking regex consistency" << std::endl;);
+        check_regex_in(lhs, rhs);
     }
 
     // okay, all checks here passed
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 8acdb4f02..527753b73 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -138,14 +138,6 @@ namespace smt {
          */
         bool opt_DisableIntegerTheoryIntegration;
 
-        /*
-         * If NoCheckRegexIn is set to true,
-         * an expensive regular expression membership test is skipped.
-         * This option is for experiment purposes only and should be set to 'false'
-         * as skipping this check impacts the correctness of the solver.
-         */
-        bool opt_NoCheckRegexIn;
-
         bool search_started;
         arith_util m_autil;
         str_util m_strutil;