diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 9980beb41..63fb833b3 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -918,6 +918,10 @@ void TheoryStrings::checkCodes() cc = Rewriter::rewrite(cc); Assert(cc.isConst()); Node cp = d_termReg.getProxyVariableFor(c); + if (cp.isNull()) { + d_termReg.registerTerm(c, 0); + cp = d_termReg.getProxyVariableFor(c); + } AlwaysAssert(!cp.isNull()); Node vc = nm->mkNode(STRING_TO_CODE, cp); if (!d_state.areEqual(cc, vc)) diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 0ad11f30d..1ee6e6adc 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -183,7 +183,7 @@ class TheoryStrings : public Theory { void eqNotifyRewrite(TNode t1, TNode t2) override { - d_termReg.registerTerm(t2, 0); + // d_termReg.registerTerm(t2, 0); } private: |