bug fix for constant regular expression model building

1 files changed, 7 insertions, 3 deletions

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 1c62717c8..cb50bf355 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -198,9 +198,13 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
     }
 
     if (!d_equalityEngine->hasTerm(n)) {
-      // Unknown term - return first enumerated value for this type
-      TypeEnumerator te(n.getType());
-      ret = *te;
+      if(n.getType().isRegExp()) { 
+        ret = Rewriter::rewrite(ret);
+      } else {
+        // Unknown term - return first enumerated value for this type
+        TypeEnumerator te(n.getType());
+        ret = *te;
+      }
       d_modelCache[n] = ret;
       return ret;
     }