Test

1 files changed, 7 insertions, 0 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 90bd91070..3ec38e306 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -624,6 +624,13 @@ Node TheoryStringsRewriter::rewriteArithEqualityExt(Node node)
     }
   }
 
+  if (checkEntailArith(node[0], node[1], true)
+      || checkEntailArith(node[1], node[0], true))
+  {
+    Node ret = nm->mkConst(false);
+    return returnRewrite(node, ret, "int-eq-false");
+  }
+
   return node;
 }