diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5b7c38361..b98bd1dea 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -580,7 +580,7 @@ Node TheoryStrings::expandDefinition(Node node) if (node.getKind() == STRING_FROM_CODE) { // str.from_code(t) ---> - // choice k. ite(0 <= t < |A|, t = str.to_code(k), k = "") + // witness k. ite(0 <= t < |A|, t = str.to_code(k), k = "") NodeManager* nm = NodeManager::currentNM(); Node t = node[0]; Node card = nm->mkConst(Rational(utils::getAlphabetCardinality())); @@ -590,7 +590,7 @@ Node TheoryStrings::expandDefinition(Node node) Node bvl = nm->mkNode(BOUND_VAR_LIST, k); Node emp = Word::mkEmptyWord(node.getType()); node = nm->mkNode( - CHOICE, + WITNESS, bvl, nm->mkNode( ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp))); |