summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-04-30 16:04:29 -0700
committerAndres Noetzli <andres.noetzli@gmail.com>2019-04-30 16:04:29 -0700
commit172e0bd41cbd410fb1e66bc32a9a9b8523bc40e2 (patch)
treeb052bec1c8a117f029f945c38090a5bb49e3761c /src
parent309ea1524efa686bf1ef5ee4fb927f24d54db5f5 (diff)
fix
Diffstat (limited to 'src')
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 3bed01ea2..35e966b78 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -703,6 +703,7 @@ Node TheoryStringsRewriter::rewriteArithEqualityExt(Node node)
// notice we cannot rewrite str.to.int(x)=n to x="n" due to leading zeroes.
+ NodeManager* nm = NodeManager::currentNM();
if (checkEntailArith(node[0], node[1], true)
|| checkEntailArith(node[1], node[0], true))
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback