diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index e1c4f2359..79f8d4eac 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -8594,7 +8594,10 @@ namespace smt {
             }
         }
 
-        solve_regex_automata();
+        if (!solve_regex_automata()) {
+            TRACE("str", tout << "regex engine requested to give up!" << std::endl;);
+            return FC_GIVEUP;
+        }
 
         bool needToAssignFreeVars = false;
         expr_ref_vector free_variables(m);
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index bef665fed..6c1244976 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -623,7 +623,7 @@ protected:
     void instantiate_axiom_RegexIn(enode * e);
 
     // regex automata and length-aware regex
-    void solve_regex_automata();
+    bool solve_regex_automata();
     unsigned estimate_regex_complexity(expr * re);
     unsigned estimate_regex_complexity_under_complement(expr * re);
     unsigned estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2);
diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp
index b26ce197c..e27d79786 100644
--- a/src/smt/theory_str_regex.cpp
+++ b/src/smt/theory_str_regex.cpp
@@ -46,8 +46,8 @@ namespace smt {
         return result;
     }
 
-
-    void theory_str::solve_regex_automata() {
+    // Returns false if we need to give up solving, e.g. because we found symbolic expressions in an automaton.
+    bool theory_str::solve_regex_automata() {
         ast_manager & m = get_manager();
 
         // TODO since heuristics might fail, the "no progress" flag might need to be handled specially here
@@ -216,6 +216,10 @@ namespace smt {
                         CTRACE("str", regex_get_counter(regex_fail_count, str_in_re) >= m_params.m_RegexAutomata_FailedAutomatonThreshold,
                                 tout << "failed automaton threshold reached for " << mk_pp(str_in_re, m) << " -- automatically constructing full automaton" << std::endl;);
                         eautomaton * aut = m_mk_aut(re);
+                        if (aut == nullptr) {
+                            TRACE("str", tout << "ERROR: symbolic automaton construction failed, likely due to non-constant term in regex" << std::endl;);
+                            return false;
+                        }
                         aut->compress();
                         regex_automata.push_back(aut);
                         regex_automaton_under_assumptions new_aut(re, aut, true);
@@ -354,6 +358,10 @@ namespace smt {
                     bool failureThresholdExceeded = (regex_get_counter(regex_fail_count, str_in_re) >= m_params.m_RegexAutomata_FailedAutomatonThreshold);
                     if (expected_complexity <= m_params.m_RegexAutomata_DifficultyThreshold || failureThresholdExceeded) {
                         eautomaton * aut = m_mk_aut(re);
+                        if (aut == nullptr) {
+                            TRACE("str", tout << "ERROR: symbolic automaton construction failed, likely due to non-constant term in regex" << std::endl;);
+                            return false;
+                        }
                         aut->compress();
                         regex_automata.push_back(aut);
                         regex_automaton_under_assumptions new_aut(re, aut, true);
@@ -475,6 +483,10 @@ namespace smt {
                         bool failureThresholdExceeded = (regex_get_counter(regex_fail_count, str_in_re) >= m_params.m_RegexAutomata_FailedAutomatonThreshold);
                         if (expected_complexity <= m_params.m_RegexAutomata_DifficultyThreshold || failureThresholdExceeded) {
                             eautomaton * aut = m_mk_aut(re);
+                            if (aut == nullptr) {
+                                TRACE("str", tout << "ERROR: symbolic automaton construction failed, likely due to non-constant term in regex" << std::endl;);
+                                return false;
+                            }
                             aut->compress();
                             regex_automata.push_back(aut);
                             regex_automaton_under_assumptions new_aut(re, aut, true);
@@ -508,6 +520,10 @@ namespace smt {
                         if (expected_complexity <= m_params.m_RegexAutomata_DifficultyThreshold
                                 || failureThresholdExceeded) {
                             eautomaton * aut = m_mk_aut(re);
+                            if (aut == nullptr) {
+                                TRACE("str", tout << "ERROR: symbolic automaton construction failed, likely due to non-constant term in regex" << std::endl;);
+                                return false;
+                            }
                             aut->compress();
                             regex_automata.push_back(aut);
                             regex_automaton_under_assumptions new_aut(re, aut, true);
@@ -640,6 +656,10 @@ namespace smt {
                             // need to complement first
                             expr_ref rc(u.re.mk_complement(aut.get_regex_term()), m);
                             eautomaton * aut_c = m_mk_aut(rc);
+                            if (aut_c == nullptr) {
+                                TRACE("str", tout << "ERROR: symbolic automaton construction failed, likely due to non-constant term in regex" << std::endl;);
+                                return false;
+                            }
                             regex_automata.push_back(aut_c);
                             // TODO is there any way to build a complement automaton from an existing one?
                             // this discards length information
@@ -713,9 +733,7 @@ namespace smt {
                 regex_axiom_add = true;
             }
         } // foreach (entry in regex_terms_by_string)
-        if (regex_axiom_add) {
-            //return FC_CONTINUE;
-        }
+        return true;
     }
 
     unsigned theory_str::estimate_regex_complexity(expr * re) {