diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-27 12:05:48 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-27 12:05:48 -0700 |
| commit | 6633def81a5cf40333464e1ed0d9612ffd6763ac (patch) | |
| tree | 44b09ae99906956208702a4888a78e5fc55b0b50 /src/theory/quantifiers/term_util.cpp | |
| parent | 4477a899a8d18a8bb901e77317892443c2df3aa2 (diff) | |
| parent | 4b7fc20dcce9eefdf568937f5e2c54141c4f5c5b (diff) | |
Merge branch 'master' into issue4151
Diffstat (limited to 'src/theory/quantifiers/term_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_util.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 7f94130f3..cc920f1d7 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers_engine.h" +#include "theory/strings/word.h" #include "theory/theory_engine.h" using namespace std; @@ -464,11 +465,11 @@ Node TermUtil::mkTypeValue(TypeNode tn, int val) n = NodeManager::currentNM()->mkConst(false); } } - else if (tn.isString()) + else if (tn.isStringLike()) { if (val == 0) { - n = NodeManager::currentNM()->mkConst(::CVC4::String("")); + n = strings::Word::mkEmptyWord(tn); } } return n; |