From 0b4e54be38c73c65bf51184828fae54f07f162cb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Apr 2018 07:15:04 +0200 Subject: [PATCH] fix #1583 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 186abda48..e5cac969f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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: