From 82e481f6d9876a6e0c39704943c766b9c52dd363 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 5 Jun 2021 16:03:02 -0700 Subject: [PATCH] #5324 --- src/sat/smt/array_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index 850429579..4e6f75c4d 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -269,6 +269,6 @@ namespace array { bool solver::can_beta_reduce(euf::enode* n) const { expr* c = n->get_expr(); - return a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c); + return a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c) || a.is_map(c); } }