diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-12-22 16:22:42 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-12-22 16:23:34 -0600 |
commit | cea82f89852e3ee2b051627c3402bd23827f6c52 (patch) | |
tree | 622ba859b095e8f7dab0e4d532d55f39d9eb1974 /src/theory/theory_model.cpp | |
parent | 76da4764db903c503ac339584db667aa50748179 (diff) |
bug fix for constant regular expression model building
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 10 |
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; } |