mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix #2149

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-23 11:10:01 +01:00
parent c0d20f8ea8
commit 773c613694
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/rewriter/array_rewriter.cpp
View file

@ -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) {