fix internalize regression

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Oct 8, 2021 · bfa960c · bfa960c
1 parent 6f55971
commit bfa960c
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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()) {