From 92613f26b389febe3bc6d568d3fd00156bc47615 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 27 Apr 2019 13:56:16 -0700
Subject: [PATCH] remove additional push/pop on fixedpoint

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/fp/dl_cmds.cpp | 40 ----------------------------------------
 1 file changed, 40 deletions(-)

diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index 8bea46bea..811511050 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -479,44 +479,6 @@ public:
     }
 };
 
-/**
-   \brief fixedpoint-push command.
-*/
-class dl_push_cmd : public cmd {
-    ref<dl_context> m_dl_ctx;
-public:
-    dl_push_cmd(dl_context * dl_ctx):
-      cmd("fixedpoint-push"),
-      m_dl_ctx(dl_ctx)
-    {}
-
-    char const * get_usage() const override { return ""; }
-    char const * get_descr(cmd_context & ctx) const override { return "push the fixedpoint context"; }
-    unsigned get_arity() const override { return 0; }
-    void execute(cmd_context & ctx) override {
-        m_dl_ctx->push();
-    }
-};
-
-/**
-   \brief fixedpoint-pop command.
-*/
-class dl_pop_cmd : public cmd {
-    ref<dl_context> m_dl_ctx;
-public:
-    dl_pop_cmd(dl_context * dl_ctx):
-      cmd("fixedpoint-pop"),
-      m_dl_ctx(dl_ctx)
-    {}
-
-    char const * get_usage() const override { return ""; }
-    char const * get_descr(cmd_context & ctx) const override { return "pop the fixedpoint context"; }
-    unsigned get_arity() const override { return 0; }
-    void execute(cmd_context & ctx) override {
-        m_dl_ctx->pop();
-    }
-};
-
 
 static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_cmds) {
     dl_context * dl_ctx = alloc(dl_context, ctx, collected_cmds);
@@ -524,8 +486,6 @@ static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_c
     ctx.insert(alloc(dl_query_cmd, dl_ctx));
     ctx.insert(alloc(dl_declare_rel_cmd, dl_ctx));
     ctx.insert(alloc(dl_declare_var_cmd, dl_ctx));
-    ctx.insert(alloc(dl_push_cmd, dl_ctx));
-    ctx.insert(alloc(dl_pop_cmd, dl_ctx));
 }
 
 void install_dl_cmds(cmd_context & ctx) {