From 539d44464f4bfac1c7390ec86f759d3cef228530 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 7 Aug 2022 10:17:24 +0300 Subject: [PATCH] #6196 map can be simplified --- src/sat/smt/array_axioms.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index df1fecc49..e824b01ad 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -265,7 +265,8 @@ namespace array { args1.push_back(e1); args2.push_back(e2); for (func_decl* f : funcs) { - expr* k = m.mk_app(f, e1, e2); + expr_ref k(m.mk_app(f, e1, e2), m); + rewrite(k); args1.push_back(k); args2.push_back(k); }