mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-20 11:55:49 +00:00
Code Activity

perf: move check_fixed_length(false,true) before check_contains in final_check_eh

Browse source 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-18 01:05:56 +00:00 • committed by Lev Nachmanson
parent 09c13a75e3
commit 960ab8e67a
1 changed files with 10 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_seq.cpp
View file

@ -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");