From 9e5b6e0c9c8abb8c3ecb4f0d93bcc51146659218 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Jan 2022 12:12:58 -0800
Subject: [PATCH] #5778

---
 src/sat/smt/array_axioms.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index 296c35b8c..c0f0e9a72 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -556,7 +556,7 @@ namespace array {
             bool has_default = false;
             for (euf::enode* p : euf::enode_parents(n))
                 has_default |= a.is_default(p->get_expr());
-            if (has_default)
+            if (!has_default)
                 propagate_parent_default(v);      
         }