From 4f9ef12f3419a220362f34ab65530bf14589e073 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 1 Jul 2022 18:13:28 -0700
Subject: [PATCH] create dummy tactics for single threaded mode

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/solver/parallel_tactic.cpp | 14 +++++++++++++-
 src/tactic/tactical.cpp        | 22 ++++++++++++++++++++--
 2 files changed, 33 insertions(+), 3 deletions(-)

diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
index 2f3ba7798..01c18fa04 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -39,10 +39,22 @@ Notes:
 #include "solver/parallel_tactic.h"
 #include "solver/parallel_params.hpp"
 
+
+class non_parallel_tactic : public tactic {
+    non_parallel_tactic(solver* s, params_ref const& p) {
+    }
+
+    char const* name() const override { return "parallel_tactic"; }
+
+    void operator()(const goal_ref & g,goal_ref_buffer & result) override {
+        throw default_exception("parallel tactic is disabled in single threaded mode");
+    }
+};
+
 #ifdef SINGLE_THREAD
 
 tactic * mk_parallel_tactic(solver* s, params_ref const& p) {
-    throw default_exception("parallel tactic is disabled in single threaded mode");
+    return alloc(non_parallel_tactic, s, p);
 }
 
 #else
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 67a0e3062..1b5094cdc 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -424,10 +424,18 @@ tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5
     return or_else(10, ts);
 }
 
+class no_par_tactical : public tactic {
+public:
+    char const* name() const override { return "par"; }
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
+        throw default_exception("par_tactical is unavailable in single threaded mode");
+    }   
+};
+
 #ifdef SINGLE_THREAD
 
 tactic * par(unsigned num, tactic * const * ts) {
-    throw default_exception("par_tactical is unavailable in single threaded mode");
+    return alloc(no_par_tactical);
 }
 
 #else
@@ -576,11 +584,21 @@ tactic * par(tactic * t1, tactic * t2, tactic * t3, tactic * t4) {
     return par(4, ts);
 }
 
+class no_par_and_then_tactical : public tactic {
+public:
+    char const* name() const override { return "par_then"; }
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
+        throw default_exception("par_and_then is not available in single threaded mode");
+    }   
+};
+
+
 #ifdef SINGLE_THREAD
 
 tactic * par_and_then(tactic * t1, tactic * t2) {
-    throw default_exception("par_and_then is not available in single threaded mode");
+    return alloc(no_par_and_then_tactical);
 }
+
 #else
 class par_and_then_tactical : public and_then_tactical {
 public: