mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix internalize regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
6f55971177
commit
bfa960c2ce
|
@ -120,8 +120,8 @@ namespace array {
|
|||
SASSERT(!n || !n->is_attached_to(get_id()));
|
||||
if (!n)
|
||||
n = mk_enode(e, false);
|
||||
SASSERT(!n->is_attached_to(get_id()));
|
||||
mk_var(n);
|
||||
if (!n->is_attached_to(get_id()))
|
||||
mk_var(n);
|
||||
for (auto* arg : euf::enode_args(n))
|
||||
ensure_var(arg);
|
||||
switch (a->get_decl_kind()) {
|
||||
|
|
Loading…
Reference in a new issue