3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-29 14:49:53 -07:00
parent f381d51c83
commit e68c72755a

View file

@ -2263,8 +2263,8 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
unsigned lo = 0, hi = 0;
if (re().is_concat(r, r1, r2)) {
expr_ref is_n = is_nullable(r1);
expr* dr1 = re().mk_derivative(ele, r1);
expr* dr2 = re().mk_derivative(ele, r2);
expr_ref dr1(re().mk_derivative(ele, r1), m());
expr_ref dr2(re().mk_derivative(ele, r2), m());
result = re().mk_concat(dr1, r2);
if (m().is_false(is_n)) {
return BR_REWRITE2;