From 4842c710199db11cb0d64a7bbfd2a089bf0c0c78 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Apr 2020 00:38:14 -0700
Subject: [PATCH] fix #3537
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/api_parsers.cpp | 2 +-
src/api/api_solver.cpp | 2 +-
src/cmd_context/cmd_context.cpp | 23 +++++++++++++++++++++++
src/cmd_context/cmd_context.h | 1 +
src/solver/tactic2solver.cpp | 5 +++--
5 files changed, 29 insertions(+), 4 deletions(-)
diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index 226d625a5..c0da66164 100644
--- a/src/api/api_parsers.cpp
+++ b/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);
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 90929416e..373d49d19 100644
--- a/src/api/api_solver.cpp
+++ b/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());
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 497a5e716..2a4c29688 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/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)");
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index fa9c2f296..8f0d8dbed 100644
--- a/src/cmd_context/cmd_context.h
+++ b/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.
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 041ae32cd..f1fcc8567 100644
--- a/src/solver/tactic2solver.cpp
+++ b/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"
/**