From 47ec61793c96efdd79ffde7bcae9cddc8e0f0e1f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Aug 2026 10:54:40 -0700 Subject: [PATCH] allow single argument versions of concat, union, intersect, xor for get_info --- src/ast/seq_decl_plugin.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 6f71dec7e7..d0f45485dd 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1695,18 +1695,24 @@ 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() == 1) + return get_info_rec(e->get_arg(0)); 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() == 1) + return get_info_rec(e->get_arg(0)); 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() == 1) + return get_info_rec(e->get_arg(0)); if (e->get_num_args() != 2) return unknown_info; i1 = get_info_rec(e->get_arg(0)); @@ -1739,6 +1745,8 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { i2 = get_info_rec(e->get_arg(1)); return i1.diff(i2); case OP_RE_XOR: + if (e->get_num_args() == 1) + return get_info_rec(e->get_arg(0)); if (e->get_num_args() != 2) return unknown_info; i1 = get_info_rec(e->get_arg(0));