From 815feddd1ad51a47f532740c1a8a68efb1ce1596 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Apr 2020 13:47:26 -0700
Subject: [PATCH] fix #4156
---
src/ast/rewriter/seq_rewriter.cpp | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 8a3a44093..538cd38c8 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -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);
break;
case OP_RE_INTERSECT:
- SASSERT(num_args == 2);
- st = mk_re_inter(args[0], args[1], result);
+ if (num_args == 1) {
+ result = args[0];
+ st = BR_DONE;
+ }
+ else {
+ SASSERT(num_args == 2);
+ st = mk_re_inter(args[0], args[1], result);
+ }
break;
case OP_RE_COMPLEMENT:
SASSERT(num_args == 1);