mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 21:20:52 +00:00
Code Activity

fix #2643 - fuzzers are here to get you @lorisdanton

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-12 18:19:13 -07:00
parent cc26d49060
commit a921b4ff4a
2 changed files with 10 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -251,7 +251,7 @@ eautomaton* re2automaton::operator()(expr* e) {
if (r) {
r->compress();
bool_rewriter br(m);
TRACE("seq", display_expr1 disp(m); r->display(tout, disp););
TRACE("seq", display_expr1 disp(m); r->display(tout << mk_pp(e, m) << " -->\n", disp););
}
return r;
}
@ -348,7 +348,9 @@ eautomaton* re2automaton::re2aut(expr* e) {
return a.detach();
}
else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) {
return m_sa->mk_product(*a, *b);
eautomaton* r = m_sa->mk_product(*a, *b);
TRACE("seq", display_expr1 disp(m); a->display(tout << "a:", disp); b->display(tout << "b:", disp); r->display(tout << "intersection:", disp););
return r;
}
else {
TRACE("seq", tout << "not handled " << mk_pp(e, m) << "\n";);