#6196

map can be simplified
Z3Prover · Aug 7, 2022 · 539d444 · 539d444
1 parent f34317d
commit 539d444
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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);
         }