From 839f87a10c919d1c61040c1e91e4d831c3d46071 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 2 Feb 2023 20:50:46 -0800
Subject: [PATCH] don't apply tactics in parse mode

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/tactic_cmds.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index 4559586f3..a0805110b 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -296,9 +296,10 @@ public:
     }
 
     void execute(cmd_context & ctx) override {
-        if (!m_tactic) {
+        if (!m_tactic) 
             throw cmd_exception("apply needs a tactic argument");
-        }
+        if (ctx.ignore_check())
+            return;
         params_ref p = ctx.params().merge_default_params(ps());
         tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
         {