From 496ec5f2b44bf6c7460b16326311a8c2b43508bd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 11 Aug 2021 05:00:02 -0700
Subject: [PATCH] #5454
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/smt/array_model.cpp | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp
index b4e7d3cab..74594e5a0 100644
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@@ -73,7 +73,7 @@ namespace array {
obj_map<expr, unsigned> num_occ;
for (euf::enode* p : euf::enode_parents(n->get_root())) {
if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n->get_root()) {
- expr* v = values.get(p->get_root_id());
+ expr* v = values.get(p->get_root_id(), nullptr);
if (!v)
continue;
unsigned no = 0;
@@ -92,7 +92,7 @@ namespace array {
for (euf::enode* p : euf::enode_parents(n)) {
if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n) {
- expr* value = values.get(p->get_root_id());
+ expr* value = values.get(p->get_root_id(), nullptr);
if (!value || value == fi->get_else())
continue;
args.reset();