mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

z3str3: don't compute intersection difficulty against a null automaton (#4846)

Browse source
This commit is contained in:
Murphy Berzish 2020-12-04 10:40:03 -06:00 • committed by GitHub
parent 6d427d9dae
commit b0fd25f041
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_str_regex.cpp
View file

@ -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) {