From d9af8ea9fbaa543cc0f0d73523578c1bd150ec3e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 7 Apr 2021 12:20:12 -0700
Subject: [PATCH] fix #5113

---
 src/api/api_parsers.cpp         | 1 +
 src/cmd_context/cmd_context.cpp | 4 ++++
 src/cmd_context/cmd_context.h   | 1 +
 3 files changed, 6 insertions(+)

diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index b49d6b99c..aeb1e3d3f 100644
--- a/src/api/api_parsers.cpp
+++ b/src/api/api_parsers.cpp
@@ -42,6 +42,7 @@ extern "C" {
         Z3_TRY;
         ast_manager& m = mk_c(c)->m();
         scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(m));
+        ctx->register_plist();
         ctx->set_ignore_check(true);
         Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), m);
         
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 43d68e82c..1bd9af0d5 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -760,6 +760,10 @@ void cmd_context::init_manager_core(bool new_manager) {
     m_check_logic.set_logic(m(), m_logic);
 }
 
+void cmd_context::register_plist() {
+    insert(pm().mk_plist_decl());
+}
+
 void cmd_context::init_manager() {
     if (m_manager_initialized) {
         // no-op
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 2cbe30a72..be5c8f465 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -330,6 +330,7 @@ public:
     cmd_context(bool main_ctx = true, ast_manager * m = nullptr, symbol const & l = symbol::null);
     ~cmd_context() override;
     void set_cancel(bool f);
+    void register_plist();
     context_params  & params() { return m_params; }
     solver_factory &get_solver_factory() { return *m_solver_factory; }
     opt_wrapper*  get_opt();