#5778 ensure else value so that defaults align across equivalence class

Z3Prover · Apr 6, 2022 · cebbc71 · cebbc71
1 parent ac2523a
commit cebbc71
Showing 1 changed file with 6 additions and 0 deletions.
diff --git 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())