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 {