From 89373d5bf90d1f9393da7110a16e1990e0d1651a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Apr 2021 16:02:08 -0700 Subject: [PATCH] #5215 --- src/sat/smt/array_model.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp index b74270c23..964f6902d 100644 --- a/src/sat/smt/array_model.cpp +++ b/src/sat/smt/array_model.cpp @@ -39,8 +39,10 @@ namespace array { dep.add(n, p->get_arg(i)); } for (euf::enode* k : euf::enode_class(n)) - if (a.is_const(k->get_expr())) - dep.add(n, k->get_arg(0)); + if (a.is_const(k->get_expr())) + dep.add(n, k->get_arg(0)); + if (!dep.deps().contains(n)) + dep.insert(n, nullptr); return true; }