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

out

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-02-23 18:14:20 -08:00
parent 377d060036
commit 04edfc9fdb
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1155,8 +1155,6 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
if (str().is_extract(a, a1, b1, c1) && if (str().is_extract(a, a1, b1, c1) &&
is_prefix(a, b, c) && is_suffix(a1, b1, c1)) { is_prefix(a, b, c) && is_suffix(a1, b1, c1)) {
expr_ref q(m_autil.mk_sub(c, str().mk_length(a)), m()); expr_ref q(m_autil.mk_sub(c, str().mk_length(a)), m());
std::cout << "prefix-suffix " << mk_pp(a, m()) << " " << mk_pp(b, m()) << " " << mk_pp(c, m()) << "\n";
std::cout << q << "\n";
result = str().mk_substr(a1, b1, m_autil.mk_add(c1, q)); result = str().mk_substr(a1, b1, m_autil.mk_add(c1, q));
return BR_REWRITE3; return BR_REWRITE3;
} }