diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 8 |
1 files changed, 8 insertions, 0 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 |