From bfa960c2cee9ec4343d00f2e504508d757a36a1e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Oct 2021 14:48:17 -0700 Subject: [PATCH] fix internalize regression Signed-off-by: Nikolaj Bjorner --- src/sat/smt/array_internalize.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index 7e3f94b84..aa94f12a7 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -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()) {