2 files changed, 8 insertions, 0 deletions
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index fd593c68b..c4efe5e09 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -214,6 +214,12 @@ void Tptp::checkLetBinding(const std::vector<Expr>& bvlist, Expr lhs, Expr rhs,
   }
 }
 
+void Tptp::forceLogic(const std::string& logic)
+{
+  Parser::forceLogic(logic);
+  preemptCommand(new SetBenchmarkLogicCommand(logic));
+}
+
 void Tptp::addFreeVar(Expr var) {
   assert(cnf());
   d_freeVar.push_back(var);
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 082b905df..605748d88 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -47,6 +47,8 @@ class Tptp : public Parser {
   bool fof() const { return d_fof; }
   void setFof(bool fof) { d_fof = fof; }
 
+  void forceLogic(const std::string& logic) override;
+
   void addFreeVar(Expr var);
   std::vector< Expr > getFreeVar();