diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 80577efee..f26ffeeba 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -201,7 +201,7 @@ extern "C" {
         LOG_Z3_get_as_array_func_decl(c, a);
         RESET_ERROR_CODE();
         if (is_expr(to_ast(a)) && is_app_of(to_expr(a), mk_c(c)->get_array_fid(), OP_AS_ARRAY)) {
-            return of_func_decl(to_func_decl(to_app(a)->get_decl()->get_parameter(0).get_ast()));
+            RETURN_Z3(of_func_decl(to_func_decl(to_app(a)->get_decl()->get_parameter(0).get_ast())));
         }
         else {
             SET_ERROR_CODE(Z3_INVALID_ARG);
diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index fc9b8939f..533d143c3 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -58,7 +58,7 @@ namespace smt {
            \remark if negate == true, then the hypothesis is actually (not (= lhs rhs))
         */
         proof * mk_hypothesis(ast_manager & m, app * eq, bool negate, expr * lhs, expr * rhs) {
-            SASSERT(m.is_eq(eq));
+            SASSERT(m.is_eq(eq) || m.is_iff(eq));
             SASSERT((eq->get_arg(0) == lhs && eq->get_arg(1) == rhs) ||
                     (eq->get_arg(0) == rhs && eq->get_arg(1) == lhs));
             app * h = negate ? m.mk_not(eq) : eq;