diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 2ded7c1b3a..ba0f9ff350 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2210,6 +2210,9 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) { r = mk_true(); } + // riskier fix: +// else if (num_args == 1 && decl->is_left_associative() && is_app(args[0])) +// r = to_app(args[0]); else if (num_args > 2 && !decl->is_flat_associative()) { if (decl->is_right_associative()) { unsigned j = num_args - 1; diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 75949316a0..6f71dec7e7 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1695,14 +1695,20 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { //TBD: check if the character predicate contains uninterpreted symbols or is nonground or is unsat return info(true, l_false, 1, false); case OP_RE_CONCAT: + if (e->get_num_args() != 2) + return unknown_info; i1 = get_info_rec(e->get_arg(0)); i2 = get_info_rec(e->get_arg(1)); return i1.concat(i2, u.re.is_concat(e->get_arg(0))); case OP_RE_UNION: + if (e->get_num_args() != 2) + return unknown_info; i1 = get_info_rec(e->get_arg(0)); i2 = get_info_rec(e->get_arg(1)); return i1.disj(i2); case OP_RE_INTERSECT: + if (e->get_num_args() != 2) + return unknown_info; i1 = get_info_rec(e->get_arg(0)); i2 = get_info_rec(e->get_arg(1)); return i1.conj(i2); @@ -1727,10 +1733,14 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { upper_bound = e->get_decl()->get_parameter(1).get_int(); return i1.loop(lower_bound, upper_bound); case OP_RE_DIFF: + if (e->get_num_args() != 2) + return unknown_info; i1 = get_info_rec(e->get_arg(0)); i2 = get_info_rec(e->get_arg(1)); return i1.diff(i2); case OP_RE_XOR: + if (e->get_num_args() != 2) + return unknown_info; i1 = get_info_rec(e->get_arg(0)); i2 = get_info_rec(e->get_arg(1)); return i1.xor_(i2);