2 files changed, 22 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index cb1f006b3..2ce325862 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -701,6 +701,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
 void TheoryStrings::preRegisterTerm(TNode n) {
   if( d_pregistered_terms_cache.find(n) == d_pregistered_terms_cache.end() ) {
     d_pregistered_terms_cache.insert(n);
+    Trace("strings-preregister")
+        << "TheoryString::preregister : " << n << std::endl;
     //check for logic exceptions
     Kind k = n.getKind();
     if( !options::stringExp() ){
@@ -732,6 +734,12 @@ void TheoryStrings::preRegisterTerm(TNode n) {
       default: {
         registerTerm(n, 0);
         TypeNode tn = n.getType();
+        if (tn.isRegExp() && n.isVar())
+        {
+          std::stringstream ss;
+          ss << "Regular expression variables are not supported.";
+          throw LogicException(ss.str());
+        }
         if( tn.isString() ) {
           // if finite model finding is enabled,
           // then we minimize the length of this term if it is a variable
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 9651fe980..fe92dd8ff 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -73,8 +73,15 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren,
         }else if( xc.isConst() ){
           //check for constants
           CVC4::String s = xc.getConst<String>();
-          Assert( s.size()>0 );
-          if( rc.getKind() == kind::REGEXP_RANGE || rc.getKind()==kind::REGEXP_SIGMA ){
+          if (s.size() == 0)
+          {
+            // ignore and continue
+            mchildren.pop_back();
+            do_next = true;
+          }
+          else if (rc.getKind() == kind::REGEXP_RANGE
+                   || rc.getKind() == kind::REGEXP_SIGMA)
+          {
             CVC4::String ss( t==0 ? s.getLastChar() : s.getFirstChar() );
             if( testConstStringInRegExp( ss, 0, rc ) ){
               //strip off one character
@@ -698,6 +705,10 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node)
 bool TheoryStringsRewriter::isConstRegExp( TNode t ) {
   if( t.getKind()==kind::STRING_TO_REGEXP ) {
     return t[0].isConst();
+  }
+  else if (t.isVar())
+  {
+    return false;
   }else{
     for( unsigned i = 0; i<t.getNumChildren(); ++i ) {
       if( !isConstRegExp(t[i]) ){
@@ -711,6 +722,7 @@ bool TheoryStringsRewriter::isConstRegExp( TNode t ) {
 bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r ) {
   Assert( index_start <= s.size() );
   Trace("regexp-debug") << "Checking " << s << " in " << r << ", starting at " << index_start << std::endl;
+  Assert(!r.isVar());
   int k = r.getKind();
   switch( k ) {
     case kind::STRING_TO_REGEXP: {