1 files changed, 15 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 7a1fdf174..db242d101 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -86,6 +86,12 @@ void Smt2::addBitvectorOperators() {
   addOperator(kind::BITVECTOR_ROTATE_RIGHT);
 }
 
+void Smt2::addStringOperators() {
+  addOperator(kind::STRING_CONCAT);
+  addOperator(kind::STRING_LENGTH);
+  //addOperator(kind::STRING_IN_REGEXP);
+}
+
 void Smt2::addTheory(Theory theory) {
   switch(theory) {
   case THEORY_CORE:
@@ -135,6 +141,11 @@ void Smt2::addTheory(Theory theory) {
     addBitvectorOperators();
     break;
 
+  case THEORY_STRINGS:
+    defineType("String", getExprManager()->stringType());
+    addStringOperators();
+    break;
+
   case THEORY_QUANTIFIERS:
     break;
 
@@ -180,6 +191,10 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
   }
 
+  if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
+    addTheory(THEORY_STRINGS);
+  }
+
   if(d_logic.isQuantified()) {
     addTheory(THEORY_QUANTIFIERS);
   }