From 464d52babed90db7f0bf255057a33bbdae442e2f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 18 Oct 2022 12:34:45 -0700
Subject: [PATCH] fix #6410

regression after introducing beta-redex optimization
---
 src/smt/theory_array.cpp | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp
index 1f842c2ed..4df6ea7e1 100644
--- a/src/smt/theory_array.cpp
+++ b/src/smt/theory_array.cpp
@@ -380,9 +380,8 @@ namespace smt {
         }
         else {
             if (m_final_check_idx % 2 == 1) {
-                if (assert_delayed_axioms() == FC_CONTINUE)
-                    r = FC_CONTINUE;
-                else 
+                r = assert_delayed_axioms();
+                if (r == FC_DONE) 
                     r = mk_interface_eqs_at_final_check();
             }
             else {