From cebbc7133077bcbcc3e10e94851c1b6ced43c2a5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 6 Apr 2022 07:58:19 +0200
Subject: [PATCH] #5778 ensure else value so that defaults align across
 equivalence class

---
 src/sat/smt/array_model.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp
index 50b6ffd9e..5b1042db0 100644
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@@ -116,6 +116,12 @@ namespace array {
         if (!get_else(v) && fi->get_else())
             set_else(v, fi->get_else());
 
+        if (!get_else(v)) {
+            expr* else_value = mdl.get_some_value(get_array_range(srt));
+            fi->set_else(else_value);
+            set_else(v, else_value);
+        }
+
         for (euf::enode* p : *get_select_set(n)) {
             expr* value = values.get(p->get_root_id(), nullptr);
             if (!value || value == fi->get_else())