From 773c61369480b6f031eb8fa98a7eb24bd52c7070 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Feb 2019 11:10:01 +0100 Subject: [PATCH] fix #2149 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/array_rewriter.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 83749c82d..56e094dab 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -375,7 +375,13 @@ br_status array_rewriter::mk_set_intersect(unsigned num_args, expr * const * arg br_status array_rewriter::mk_set_complement(expr * arg, expr_ref & result) { - return mk_map_core(m().mk_not_decl(), 1, &arg, result); + func_decl* fnot = m().mk_not_decl(); + br_status st = mk_map_core(fnot, 1, &arg, result); + if (BR_FAILED == st) { + result = m_util.mk_map(fnot, 1, &arg); + st = BR_DONE; + } + return st; } br_status array_rewriter::mk_set_difference(expr * arg1, expr * arg2, expr_ref & result) {