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

fix #4156

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-28 13:47:26 -07:00
parent fa88dabd10
commit 815feddd1a
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -457,8 +457,14 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
st = mk_re_range(args[0], args[1], result); st = mk_re_range(args[0], args[1], result);
break; break;
case OP_RE_INTERSECT: case OP_RE_INTERSECT:
SASSERT(num_args == 2); if (num_args == 1) {
st = mk_re_inter(args[0], args[1], result); result = args[0];
st = BR_DONE;
}
else {
SASSERT(num_args == 2);
st = mk_re_inter(args[0], args[1], result);
}
break; break;
case OP_RE_COMPLEMENT: case OP_RE_COMPLEMENT:
SASSERT(num_args == 1); SASSERT(num_args == 1);