From 444e178a016dc047666059abe96495109e925986 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Dec 2017 10:24:48 -0800 Subject: [PATCH 1/2] fix up convertion and printing Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 1 + src/tactic/model_converter.cpp | 13 +++++++++---- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 4e7719f56..d8a1a7be3 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -131,6 +131,7 @@ extern "C" { void Z3_API Z3_solver_import_model_converter(Z3_context c, Z3_solver src, Z3_solver dst) { Z3_TRY; LOG_Z3_solver_import_model_converter(c, src, dst); + std::cout << "import converter\n"; model_converter_ref mc = to_solver_ref(src)->get_model_converter(); to_solver_ref(dst)->set_model_converter(mc.get()); Z3_CATCH; diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index 2598aa4f1..6055105c0 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -24,16 +24,21 @@ Notes: * Add or overwrite value in model. */ void model_converter::display_add(std::ostream& out, ast_manager& m, func_decl* f, expr* e) const { - VERIFY(m_env); - ast_smt2_pp(out, f, e, *m_env, params_ref(), 0, "model-add") << "\n"; + smt2_pp_environment_dbg env(m); + smt2_pp_environment* _env = m_env ? m_env : &env; + ast_smt2_pp(out, f, e, *_env, params_ref(), 0, "model-add") << "\n"; } /* * A value is removed from the model. */ void model_converter::display_del(std::ostream& out, func_decl* f) const { - VERIFY(m_env); - ast_smt2_pp(out << "(model-del ", f->get_name(), f->is_skolem(), *m_env) << ")\n"; + if (m_env) { + ast_smt2_pp(out << "(model-del ", f->get_name(), f->is_skolem(), *m_env) << ")\n"; + } + else { + out << "(model-del " << f->get_name() << ")\n"; + } } void model_converter::display_add(std::ostream& out, ast_manager& m) { From 69879322d8633505a89a8ead9e7936cbea79fa2d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Dec 2017 10:26:32 -0800 Subject: [PATCH 2/2] fix up convertion and printing Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index d8a1a7be3..4e7719f56 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -131,7 +131,6 @@ extern "C" { void Z3_API Z3_solver_import_model_converter(Z3_context c, Z3_solver src, Z3_solver dst) { Z3_TRY; LOG_Z3_solver_import_model_converter(c, src, dst); - std::cout << "import converter\n"; model_converter_ref mc = to_solver_ref(src)->get_model_converter(); to_solver_ref(dst)->set_model_converter(mc.get()); Z3_CATCH;