mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
279f1986a6
commit
0b4e54be38
|
@ -367,6 +367,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
SASSERT(num_args == 2);
|
||||
return mk_re_concat(args[0], args[1], result);
|
||||
case OP_RE_UNION:
|
||||
if (num_args == 1) {
|
||||
result = args[0]; return BR_DONE;
|
||||
}
|
||||
SASSERT(num_args == 2);
|
||||
return mk_re_union(args[0], args[1], result);
|
||||
case OP_RE_RANGE:
|
||||
|
|
Loading…
Reference in a new issue