mirror of
https://github.com/Z3Prover/z3
synced 2025-04-16 22:05:36 +00:00
This commit is contained in:
parent
df95ed64e0
commit
82e481f6d9
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue