add macros to model #4679

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Sep 8, 2020 · f976b16 · f976b16
1 parent 629e981
commit f976b16
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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) {
-Original file line number
+Diff line change
@@ Expand Up @@
         else {
             VERIFY(decls.insert(m(), arity, domain, t));
         }
+        model_add(s, arity, domain, t);
     }
     void cmd_context::erase_macro(symbol const& s) {
@@ Expand Down @@