From b0fd25f04190cb54fbfae69cec8b8369a96c5300 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 4 Dec 2020 10:40:03 -0600 Subject: [PATCH] z3str3: don't compute intersection difficulty against a null automaton (#4846) --- src/smt/theory_str_regex.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp index fdad98b46..ecdc0c14c 100644 --- a/src/smt/theory_str_regex.cpp +++ b/src/smt/theory_str_regex.cpp @@ -611,7 +611,10 @@ namespace smt { }); if (regex_get_counter(regex_length_attempt_count, aut.get_regex_term()) >= m_params.m_RegexAutomata_LengthAttemptThreshold) { - unsigned intersectionDifficulty = estimate_automata_intersection_difficulty(aut_inter, aut.get_automaton()); + unsigned intersectionDifficulty = 0; + if (aut_inter != nullptr) { + intersectionDifficulty = estimate_automata_intersection_difficulty(aut_inter, aut.get_automaton()); + } TRACE("str", tout << "intersection difficulty is " << intersectionDifficulty << std::endl;); if (intersectionDifficulty <= m_params.m_RegexAutomata_IntersectionDifficultyThreshold || regex_get_counter(regex_intersection_fail_count, aut.get_regex_term()) >= m_params.m_RegexAutomata_FailedIntersectionThreshold) {