diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 58b166ac6..38f67374e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -345,11 +345,6 @@ final_check_status theory_seq::final_check_eh(unsigned level) { TRACEFIN("regex propagate"); return FC_CONTINUE; } - if (check_contains()) { - ++m_stats.m_propagate_contains; - TRACEFIN("propagate_contains"); - return FC_CONTINUE; - } if (check_fixed_length(true, false)) { ++m_stats.m_fixed_length; TRACEFIN("zero_length"); @@ -365,6 +360,16 @@ final_check_status theory_seq::final_check_eh(unsigned level) { TRACEFIN("fixed_length"); return FC_CONTINUE; } + if (check_fixed_length(false, true)) { + ++m_stats.m_fixed_length; + TRACEFIN("fixed_length"); + return FC_CONTINUE; + } + if (check_contains()) { + ++m_stats.m_propagate_contains; + TRACEFIN("propagate_contains"); + return FC_CONTINUE; + } if (check_int_string()) { ++m_stats.m_int_string; TRACEFIN("int_string");