mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

simplify last_index function

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-09-18 12:52:50 -07:00
parent 31c91e1674
commit 643512613a
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/seq_rewriter.cpp
View file

@ -1716,6 +1716,10 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) {
result = m_autil.mk_numeral(rational(idx), true); result = m_autil.mk_numeral(rational(idx), true);
return BR_DONE; return BR_DONE;
} }
if (a == b) {
result = m_autil.mk_int(0);
return BR_DONE;
}
return BR_FAILED; return BR_FAILED;
} }