diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index d21f7400c..5c711019f 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -260,9 +260,8 @@ extern "C" {
         bool initialized = to_solver(s)->m_solver.get() != nullptr;
         if (!initialized)
             init_solver(c, s);
-        for (expr* e : ctx->tracked_assertions()) {
+        for (expr* e : ctx->tracked_assertions()) 
             to_solver(s)->assert_expr(e);
-        }
         to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
     }
 
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index f86cc6cb6..709886e4d 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -306,6 +306,7 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma
     else {
         VERIFY(decls.insert(m(), arity, domain, t));
     }
+    model_add(s, arity, domain, t);
 }
 
 void cmd_context::erase_macro(symbol const& s) {