Fix and simplify handling of --force-logic (#3062)

The `--force-logic` command line argument can be used to override a
logic specified in an input file or to set a logic when none is given.
Before this commit, both the `SmtEngine` and the parser were aware of
that argument. However, there were two issues if an input file didn't
specify a logic but `--force-logic` was used:

- Upon parsing `--force-logic`, the `SmtEngine` was informed about it
  and set the logic to the forced logic. Then, the parser detected that
  there was no `set-logic` command, so it set the logic to `ALL` and
  emitted a corresponding warning. Finally, `SmtEngine::setDefaults()`
  detected that `forceLogic` was set by the user and changed the logic
  back to the forced logic. The warning was confusing and setting the
  logic multiple times was not elegant.
- For eager bit-blasting, the logic was checked before resetting the
  logic to the forced logic, so it would emit an error that eager
  bit-blasting couldn't be used with the logic (which was `ALL` at that
  point of the execution). This was a problem in the competition because
  our runscript parses the `set-logic` command to decide on the
  appropriate arguments to use and passes the logic to CVC4 via
  `--force-logic`.

This commit moves the handling of `--force-logic` entirely into the
parser. The rationale for that is that this is not an API-level issue
(if you use the API you simply set the logic you want, forcing a
different logic in addition doesn't make sense) and simplifies the
handling of the option (no listeners need to be installed and the logic
is set only once). This commit also removes the option to set the logic
via `(set-option :cvc4-logic ...)` because it complicates matters (e.g.
which method of setting the logic takes precedence?). For the CVC and
the TPTP languages the commit creates a command to set the logic in
`SmtEngine` when the logic is forced in the parser instead of relying on
`SmtEngine` to figure it out itself.

22 files changed, 220 insertions, 151 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index ab34e62b4..7750823d3 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3389,41 +3389,23 @@ void Solver::setLogicHelper(const std::string& logic) const
  */
 void Solver::setInfo(const std::string& keyword, const std::string& value) const
 {
-  bool is_cvc4_keyword = false;
-
-  /* Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_") */
-  if (keyword.length() > 5)
-  {
-    std::string prefix = keyword.substr(0, 5);
-    if (prefix == "cvc4-" || prefix == "cvc4_")
-    {
-      is_cvc4_keyword = true;
-      std::string cvc4key = keyword.substr(5);
-      CVC4_API_ARG_CHECK_EXPECTED(cvc4key == "logic", keyword)
-          << "keyword 'cvc4-logic'";
-      setLogicHelper(value);
-    }
-  }
-  if (!is_cvc4_keyword)
-  {
-    CVC4_API_ARG_CHECK_EXPECTED(
-        keyword == "source" || keyword == "category" || keyword == "difficulty"
-            || keyword == "filename" || keyword == "license"
-            || keyword == "name" || keyword == "notes"
-            || keyword == "smt-lib-version" || keyword == "status",
-        keyword)
-        << "'source', 'category', 'difficulty', 'filename', 'license', 'name', "
-           "'notes', 'smt-lib-version' or 'status'";
-    CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2"
-                                    || value == "2.0" || value == "2.5"
-                                    || value == "2.6" || value == "2.6.1",
-                                value)
-        << "'2.0', '2.5', '2.6' or '2.6.1'";
-    CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat"
-                                    || value == "unsat" || value == "unknown",
-                                value)
-        << "'sat', 'unsat' or 'unknown'";
-  }
+  CVC4_API_ARG_CHECK_EXPECTED(
+      keyword == "source" || keyword == "category" || keyword == "difficulty"
+          || keyword == "filename" || keyword == "license" || keyword == "name"
+          || keyword == "notes" || keyword == "smt-lib-version"
+          || keyword == "status",
+      keyword)
+      << "'source', 'category', 'difficulty', 'filename', 'license', 'name', "
+         "'notes', 'smt-lib-version' or 'status'";
+  CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2"
+                                  || value == "2.0" || value == "2.5"
+                                  || value == "2.6" || value == "2.6.1",
+                              value)
+      << "'2.0', '2.5', '2.6' or '2.6.1'";
+  CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat"
+                                  || value == "unsat" || value == "unknown",
+                              value)
+      << "'sat', 'unsat' or 'unknown'";
 
   d_smtEngine->setInfo(keyword, value);
 }
diff --git a/src/options/options.h b/src/options/options.h
index 3f2d72b7e..1fc7ed51a 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -52,9 +52,6 @@ class CVC4_PUBLIC Options {
   /** The current Options in effect */
   static thread_local Options* s_current;
 
-  /** Listeners for options::forceLogicString being set. */
-  ListenerCollection d_forceLogicListeners;
-
   /** Listeners for notifyBeforeSearch. */
   ListenerCollection d_beforeSearchListeners;
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 5e98f8f5a..b145da639 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -74,10 +74,6 @@ void throwLazyBBUnsupported(theory::bv::SatSolverMode m)
 
 OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
 
-void OptionsHandler::notifyForceLogic(const std::string& option){
-  d_options->d_forceLogicListeners.notify();
-}
-
 void OptionsHandler::notifyBeforeSearch(const std::string& option)
 {
   try{
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 06f7ab6e4..7ae461fd8 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -174,9 +174,6 @@ public:
   decision::DecisionWeightInternal stringToDecisionWeightInternal(
       std::string option, std::string optarg);
 
-  /* smt/options_handlers.h */
-  void notifyForceLogic(const std::string& option);
-
   /**
    * Throws a ModalException if this option is being set after final
    * initialization.
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 1f7ba05fc..f67493f87 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -231,7 +231,6 @@ void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* h
 Options::Options()
     : d_holder(new options::OptionsHolder())
     , d_handler(new options::OptionsHandler(this))
-    , d_forceLogicListeners()
     , d_beforeSearchListeners()
     , d_tlimitListeners()
     , d_tlimitPerListeners()
@@ -283,13 +282,6 @@ ListenerCollection::Registration* Options::registerAndNotify(
   return registration;
 }
 
-ListenerCollection::Registration* Options::registerForceLogicListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::forceLogicString);
-  return registerAndNotify(d_forceLogicListeners, listener, notify);
-}
-
 ListenerCollection::Registration* Options::registerBeforeSearchListener(
    Listener* listener)
 {
diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml
index 988bcb6eb..71074d420 100644
--- a/src/options/parser_options.toml
+++ b/src/options/parser_options.toml
@@ -65,3 +65,12 @@ header = "options/parser_options.h"
   category   = "undocumented"
   long       = "no-include-file"
   links      = ["--no-filesystem-access"]
+
+[[option]]
+  name       = "forceLogicString"
+  smt_name   = "force-logic"
+  category   = "expert"
+  long       = "force-logic=LOGIC"
+  type       = "std::string"
+  read_only  = true
+  help       = "set the logic, and override all further user attempts to change it"
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index e0041774a..72dfdd7f8 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -23,16 +23,6 @@ header = "options/smt_options.h"
   help       = "all dumping goes to FILE (instead of stdout)"
 
 [[option]]
-  name       = "forceLogicString"
-  smt_name   = "force-logic"
-  category   = "expert"
-  long       = "force-logic=LOGIC"
-  type       = "std::string"
-  notifies   = ["notifyForceLogic"]
-  read_only  = true
-  help       = "set the logic, and override all further user attempts to change it"
-
-[[option]]
   name       = "simplificationMode"
   smt_name   = "simplification-mode"
   category   = "regular"
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index d79d7b22c..03e194b90 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -22,6 +22,8 @@ set(libcvc4parser_src_files
   bounded_token_buffer.h
   bounded_token_factory.cpp
   bounded_token_factory.h
+  cvc/cvc.cpp
+  cvc/cvc.h
   cvc/cvc_input.cpp
   cvc/cvc_input.h
   input.cpp
diff --git a/src/parser/cvc/cvc.cpp b/src/parser/cvc/cvc.cpp
new file mode 100644
index 000000000..9b7e1f403
--- /dev/null
+++ b/src/parser/cvc/cvc.cpp
@@ -0,0 +1,29 @@
+/*********************                                                        */
+/*! \file cvc.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The parser class for the CVC language.
+ **
+ ** The parser class for the CVC language.
+ **/
+
+#include "parser/cvc/cvc.h"
+
+namespace CVC4 {
+namespace parser {
+
+void Cvc::forceLogic(const std::string& logic)
+{
+  Parser::forceLogic(logic);
+  preemptCommand(new SetBenchmarkLogicCommand(logic));
+}
+
+}  // namespace parser
+}  // namespace CVC4
diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h
new file mode 100644
index 000000000..feb962a09
--- /dev/null
+++ b/src/parser/cvc/cvc.h
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file cvc.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The parser class for the CVC language.
+ **
+ ** The parser class for the CVC language.
+ **/
+
+#include "cvc4parser_private.h"
+
+#ifndef CVC4__PARSER__CVC_H
+#define CVC4__PARSER__CVC_H
+
+#include "api/cvc4cpp.h"
+#include "parser/parser.h"
+#include "smt/command.h"
+
+namespace CVC4 {
+
+namespace parser {
+
+class Cvc : public Parser
+{
+  friend class ParserBuilder;
+
+ public:
+  void forceLogic(const std::string& logic) override;
+
+ protected:
+  Cvc(api::Solver* solver,
+      Input* input,
+      bool strictMode = false,
+      bool parseOnly = false)
+      : Parser(solver, input, strictMode, parseOnly)
+  {
+  }
+};
+
+}  // namespace parser
+}  // namespace CVC4
+
+#endif /* CVC4__PARSER__CVC_H */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index fcc37d5d3..8f9cc425a 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -322,7 +322,12 @@ public:
       implementation optional by returning false by default. */
   virtual bool logicIsSet() { return false; }
 
-  void forceLogic(const std::string& logic) { assert(!d_logicIsForced); d_logicIsForced = true; d_forcedLogic = logic; }
+  virtual void forceLogic(const std::string& logic)
+  {
+    assert(!d_logicIsForced);
+    d_logicIsForced = true;
+    d_forcedLogic = logic;
+  }
   const std::string& getForcedLogic() const { return d_forcedLogic; }
   bool logicIsForced() const { return d_logicIsForced; }
 
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 57b63cc0f..f0e6ad284 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -22,6 +22,7 @@
 #include <string>
 
 #include "api/cvc4cpp.h"
+#include "cvc/cvc.h"
 #include "expr/expr_manager.h"
 #include "options/options.h"
 #include "parser/input.h"
@@ -105,7 +106,7 @@ Parser* ParserBuilder::build()
       }
       else
       {
-        parser = new Parser(d_solver, input, d_strictMode, d_parseOnly);
+        parser = new Cvc(d_solver, input, d_strictMode, d_parseOnly);
       }
       break;
   }
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4a30841e6..b49b62604 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -269,16 +269,8 @@ command [std::unique_ptr<CVC4::Command>* cmd]
 }
   : /* set the logic */
     SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
-    { Debug("parser") << "set logic: '" << name << "'" << std::endl;
-      if( PARSER_STATE->logicIsSet() ) {
-        PARSER_STATE->parseError("Only one set-logic is allowed.");
-      }
-      PARSER_STATE->setLogic(name);
-      if( PARSER_STATE->sygus() ){
-        cmd->reset(new SetBenchmarkLogicCommand(PARSER_STATE->getLogic().getLogicString()));
-      }else{
-        cmd->reset(new SetBenchmarkLogicCommand(name));
-      }
+    {
+      cmd->reset(PARSER_STATE->setLogic(name));
     }
   | /* set-info */
     SET_INFO_TOK metaInfoInternal[cmd]
@@ -1029,9 +1021,6 @@ metaInfoInternal[std::unique_ptr<CVC4::Command>* cmd]
 }
   : KEYWORD symbolicExpr[sexpr]
     { name = AntlrInput::tokenText($KEYWORD);
-      if(name == ":cvc4-logic" || name == ":cvc4_logic") {
-        PARSER_STATE->setLogic(sexpr.getValue());
-      }
       PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
       cmd->reset(new SetInfoCommand(name.c_str() + 1, sexpr));
     }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 12b43f346..c072c535f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -22,7 +22,6 @@
 #include "parser/smt1/smt1.h"
 #include "parser/smt2/smt2_input.h"
 #include "printer/sygus_print_callback.h"
-#include "smt/command.h"
 #include "util/bitvector.h"
 
 #include <algorithm>
@@ -35,7 +34,9 @@ namespace CVC4 {
 namespace parser {
 
 Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
-    : Parser(solver, input, strictMode, parseOnly), d_logicSet(false)
+    : Parser(solver, input, strictMode, parseOnly),
+      d_logicSet(false),
+      d_seenSetLogic(false)
 {
   if (!strictModeEnabled())
   {
@@ -626,7 +627,22 @@ void Smt2::resetAssertions() {
   }
 }
 
-void Smt2::setLogic(std::string name) {
+Command* Smt2::setLogic(std::string name, bool fromCommand)
+{
+  if (fromCommand)
+  {
+    if (d_seenSetLogic)
+    {
+      parseError("Only one set-logic is allowed.");
+    }
+    d_seenSetLogic = true;
+
+    if (logicIsForced())
+    {
+      // If the logic is forced, we ignore all set-logic requests from commands.
+      return new EmptyCommand();
+    }
+  }
 
   if(sygus()) {
     // non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2)
@@ -638,11 +654,7 @@ void Smt2::setLogic(std::string name) {
   }
 
   d_logicSet = true;
-  if(logicIsForced()) {
-    d_logic = getForcedLogic();
-  } else {
-    d_logic = name;
-  }
+  d_logic = name;
 
   // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
   // higher-order
@@ -718,8 +730,16 @@ void Smt2::setLogic(std::string name) {
   if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
     addTheory(THEORY_SEP);
   }
-  
-}/* Smt2::setLogic() */
+
+  if (sygus())
+  {
+    return new SetBenchmarkLogicCommand(d_logic.getLogicString());
+  }
+  else
+  {
+    return new SetBenchmarkLogicCommand(name);
+  }
+} /* Smt2::setLogic() */
 
 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
   // TODO: ???
@@ -729,21 +749,33 @@ void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
   // TODO: ???
 }
 
-void Smt2::checkThatLogicIsSet() {
-  if( ! logicIsSet() ) {
-    if(strictModeEnabled()) {
+void Smt2::checkThatLogicIsSet()
+{
+  if (!logicIsSet())
+  {
+    if (strictModeEnabled())
+    {
       parseError("set-logic must appear before this point.");
-    } else {
-      warning("No set-logic command was given before this point.");
-      warning("CVC4 will make all theories available.");
-      warning("Consider setting a stricter logic for (likely) better performance.");
-      warning("To suppress this warning in the future use (set-logic ALL).");
-
-      setLogic("ALL");
-
-      Command* c = new SetBenchmarkLogicCommand("ALL");
-      c->setMuted(true);
-      preemptCommand(c);
+    }
+    else
+    {
+      Command* cmd = nullptr;
+      if (logicIsForced())
+      {
+        cmd = setLogic(getForcedLogic(), false);
+      }
+      else
+      {
+        warning("No set-logic command was given before this point.");
+        warning("CVC4 will make all theories available.");
+        warning(
+            "Consider setting a stricter logic for (likely) better "
+            "performance.");
+        warning("To suppress this warning in the future use (set-logic ALL).");
+
+        cmd = setLogic("ALL", false);
+      }
+      preemptCommand(cmd);
     }
   }
 }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index d4d310b89..2ac796166 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -28,6 +28,7 @@
 #include "api/cvc4cpp.h"
 #include "parser/parser.h"
 #include "parser/smt1/smt1.h"
+#include "smt/command.h"
 #include "theory/logic_info.h"
 #include "util/abstract_value.h"
 
@@ -65,7 +66,11 @@ class Smt2 : public Parser
   };
 
  private:
+  /** Has the logic been set (either by forcing it or a set-logic command)? */
   bool d_logicSet;
+  /** Have we seen a set-logic command yet? */
+  bool d_seenSetLogic;
+
   LogicInfo d_logic;
   std::unordered_map<std::string, Kind> operatorKindMap;
   /**
@@ -197,8 +202,11 @@ class Smt2 : public Parser
    * theory symbols.
    *
    * @param name the name of the logic (e.g., QF_UF, AUFLIA)
+   * @param fromCommand should be set to true if the request originates from a
+   *                    set-logic command and false otherwise
+   * @return the command corresponding to setting the logic
    */
-  void setLogic(std::string name);
+  Command* setLogic(std::string name, bool fromCommand = true);
 
   /**
    * Get the logic.
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();
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2b81b3835..5cf690147 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -285,18 +285,6 @@ class HardResourceOutListener : public Listener {
   SmtEngine* d_smt;
 }; /* class HardResourceOutListener */
 
-class SetLogicListener : public Listener {
- public:
-  SetLogicListener(SmtEngine& smt) : d_smt(&smt) {}
-  void notify() override
-  {
-    LogicInfo inOptions(options::forceLogicString());
-    d_smt->setLogic(inOptions);
-  }
- private:
-  SmtEngine* d_smt;
-}; /* class SetLogicListener */
-
 class BeforeSearchListener : public Listener {
  public:
   BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {}
@@ -452,7 +440,6 @@ class SmtEnginePrivate : public NodeManagerListener {
    * This list contains:
    *  softResourceOut
    *  hardResourceOut
-   *  setForceLogic
    *  beforeSearchListener
    *  UseTheoryListListener
    *
@@ -600,9 +587,6 @@ class SmtEnginePrivate : public NodeManagerListener {
     try
     {
       Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
-      d_listenerRegistrations->add(
-          nodeManagerOptions.registerForceLogicListener(
-              new SetLogicListener(d_smt), true));
 
       // Multiple options reuse BeforeSearchListener so registration requires an
       // extra bit of care.
@@ -1209,9 +1193,8 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  if(options::forceLogicString.wasSetByUser()) {
-    d_logic = LogicInfo(options::forceLogicString());
-  }else if (options::solveIntAsBV() > 0) {
+  if (options::solveIntAsBV() > 0)
+  {
     if (!(d_logic <= LogicInfo("QF_NIA")))
     {
       throw OptionException(
@@ -1219,11 +1202,15 @@ void SmtEngine::setDefaults() {
           "QF_LIA, QF_IDL)");
     }
     d_logic = LogicInfo("QF_BV");
-  }else if (d_logic.getLogicString() == "QF_NRA" && options::solveRealAsInt()) {
+  }
+  else if (d_logic.getLogicString() == "QF_NRA" && options::solveRealAsInt())
+  {
     d_logic = LogicInfo("QF_NIA");
-  } else if ((d_logic.getLogicString() == "QF_UFBV" ||
-              d_logic.getLogicString() == "QF_ABV") &&
-             options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  }
+  else if ((d_logic.getLogicString() == "QF_UFBV"
+            || d_logic.getLogicString() == "QF_ABV")
+           && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  {
     d_logic = LogicInfo("QF_BV");
   }
 
@@ -2346,25 +2333,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
     }
   }
 
-  // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
-  if(key.length() > 5) {
-    string prefix = key.substr(0, 5);
-    if(prefix == "cvc4-" || prefix == "cvc4_") {
-      string cvc4key = key.substr(5);
-      if(cvc4key == "logic") {
-        if(! value.isAtom()) {
-          throw OptionException("argument to (set-info :cvc4-logic ..) must be a string");
-        }
-        SmtScope smts(this);
-        d_logic = value.getValue();
-        setLogicInternal();
-        return;
-      } else {
-        throw UnrecognizedOptionException();
-      }
-    }
-  }
-
   // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
   if (key == "source" || key == "category" || key == "difficulty"
       || key == "notes" || key == "name" || key == "license")
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f5571349f..f3abe2c87 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -251,6 +251,7 @@ set(regress_0_tests
   regress0/bv/divtest_2_5.smt2
   regress0/bv/divtest_2_6.smt2
   regress0/bv/eager-inc-cryptominisat.smt2
+  regress0/bv/eager-force-logic.smt2
   regress0/bv/fuzz01.smt
   regress0/bv/fuzz02.delta01.smt
   regress0/bv/fuzz02.smt
@@ -543,6 +544,7 @@ set(regress_0_tests
   regress0/parser/bv_arity_smt2.6.smt2
   regress0/parser/constraint.smt2
   regress0/parser/declarefun-emptyset-uf.smt2
+  regress0/parser/force_logic_set_logic.smt2
   regress0/parser/shadow_fun_symbol_all.smt2
   regress0/parser/shadow_fun_symbol_nirat.smt2
   regress0/parser/strings20.smt2
diff --git a/test/regress/regress0/bv/eager-force-logic.smt2 b/test/regress/regress0/bv/eager-force-logic.smt2
new file mode 100644
index 000000000..9b7dee8c2
--- /dev/null
+++ b/test/regress/regress0/bv/eager-force-logic.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --bitblast=eager --force-logic="QF_BV"
+; EXPECT: sat
+(set-option :produce-models true)
+(declare-fun a () (_ BitVec 16))
+(declare-fun b () (_ BitVec 16))
+(declare-fun c () (_ BitVec 16))
+
+(assert (bvult a (bvadd b c)))
+(check-sat)
diff --git a/test/regress/regress0/parser/force_logic_set_logic.smt2 b/test/regress/regress0/parser/force_logic_set_logic.smt2
new file mode 100644
index 000000000..1bab02ef9
--- /dev/null
+++ b/test/regress/regress0/parser/force_logic_set_logic.smt2
@@ -0,0 +1,9 @@
+; This regression ensures that we detect repeated set-logic commands even when
+; --force-logic is used.
+
+; COMMAND-LINE: --force-logic="QF_BV"
+; SCRUBBER: grep -o "Only one set-logic is allowed."
+; EXPECT: Only one set-logic is allowed.
+; EXIT: 1
+(set-logic QF_BV)
+(set-logic QF_BV)
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 289fc26f0..33ee51007 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -881,8 +881,6 @@ void SolverBlack::testDefineFunsRec()
 
 void SolverBlack::testSetInfo()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("cvc4-logic", "QF_BV"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("cvc4_logic", "QF_BV"));
   TS_ASSERT_THROWS(d_solver->setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->setInfo("cvc2-logic", "QF_BV"), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->setInfo("cvc4-logic", "asdf"), CVC4ApiException&);
@@ -907,10 +905,6 @@ void SolverBlack::testSetInfo()
   TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("status", "unsat"));
   TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("status", "unknown"));
   TS_ASSERT_THROWS(d_solver->setInfo("status", "asdf"), CVC4ApiException&);
-
-  d_solver->assertFormula(d_solver->mkTrue());
-  TS_ASSERT_THROWS(d_solver->setInfo("cvc4-logic", "QF_BV"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->setInfo("cvc4_logic", "QF_BV"), CVC4ApiException&);
 }
 
 void SolverBlack::testSetLogic()