diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
index 01c18fa04..5c8c30c5d 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -49,6 +49,9 @@ class non_parallel_tactic : public tactic {
     void operator()(const goal_ref & g,goal_ref_buffer & result) override {
         throw default_exception("parallel tactic is disabled in single threaded mode");
     }
+    tactic * translate(ast_manager & m) override { return nullptr; }
+    void cleanup() override {}
+
 };
 
 #ifdef SINGLE_THREAD
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 1b5094cdc..25f8365e3 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -429,7 +429,9 @@ 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");
-    }   
+    }
+    tactic * translate(ast_manager & m) override { return nullptr; }
+    void cleanup() override {}
 };
 
 #ifdef SINGLE_THREAD
@@ -589,7 +591,9 @@ 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");
-    }   
+    }
+    tactic * translate(ast_manager & m) override { return nullptr; }
+    void cleanup() override {}
 };