fix #3537

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_parsers.cpp

@@ -100,7 +100,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str());
             return of_ast_vector(v);
         }
-        for (expr * e : ctx->assertions()) {
+        for (expr* e : ctx->tracked_assertions()) {
             v->m_ast_vector.push_back(e);
         }
         return of_ast_vector(v);

src/api/api_solver.cpp

@@ -254,7 +254,7 @@ extern "C" {
         bool initialized = to_solver(s)->m_solver.get() != nullptr;
         if (!initialized)
             init_solver(c, s);
-        for (expr * e : ctx->assertions()) {
+        for (expr* e : ctx->tracked_assertions()) {
             to_solver(s)->assert_expr(e);
         }
         to_solver_ref(s)->set_model_converter(ctx->get_model_converter());

src/cmd_context/cmd_context.cpp

@@ -2055,6 +2055,29 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) {
 }
 
 
+expr_ref_vector cmd_context::tracked_assertions() {
+    expr_ref_vector result(m());
+    if (assertion_names().size() == assertions().size()) {
+        for (unsigned i = 0; i < assertions().size(); ++i) {
+            expr* an  = assertion_names()[i];
+            expr* asr = assertions()[i];
+            if (an) {
+                result.push_back(m().mk_implies(an, asr));
+            }
+            else {
+                result.push_back(asr);
+            }
+        }
+    }
+    else {
+        for (expr * e : assertions()) {
+            result.push_back(e);
+        }
+    }
+    return result;
+}
+
+
 void cmd_context::display_assertions() {
     if (!m_interactive_mode)
         throw cmd_exception("command is only available in interactive mode, use command (set-option :interactive-mode true)");

src/cmd_context/cmd_context.h

@@ -457,6 +457,7 @@ public:
 
     ptr_vector<expr> const& assertions() const { return m_assertions; }
     ptr_vector<expr> const& assertion_names() const { return m_assertion_names; }
+    expr_ref_vector tracked_assertions();
 
     /**
        \brief Hack: consume assertions if there are no scopes.

src/solver/tactic2solver.cpp

@@ -19,10 +19,11 @@ Author:
 Notes:
 
 --*/
+#include "ast/ast_translation.h"
+#include "ast/ast_pp.h"
+#include "tactic/tactic.h"
 #include "solver/tactic2solver.h"
 #include "solver/solver_na2as.h"
-#include "tactic/tactic.h"
-#include "ast/ast_translation.h"
 #include "solver/mus.h"
 
 /**