Adding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA"); works.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b5ed599123598228ae1a6dced73771381a4f848e..0f755aa01670be29e5a9da0665ea7aaee48ef9d7 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -735,6 +735,12 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
   setLogic(LogicInfo(s));
 }
 
+void SmtEngine::setLogic(const char* logic) throw(ModalException){
+  SmtScope smts(this);
+
+  setLogic(LogicInfo(string(logic)));
+}
+
 LogicInfo SmtEngine::getLogicInfo() const {
   return d_logic;
 }

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index bbb0a95e96a7e7f5349af0868a9cd7a51dd7d11f..3edcd687205a3789b4d6c81e431bcf84df40ff11 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -352,6 +352,11 @@ public:
    */
   void setLogic(const std::string& logic) throw(ModalException);
 
+  /**
+   * Set the logic of the script.
+   */
+  void setLogic(const char* logic) throw(ModalException);
+
   /**
    * Set the logic of the script.
    */