Register lower bound for str.to_int (#4408)

This commit changes the term registration for str.to_int terms. Before, we were not sending out any lemmas when registering str.to_int terms. Now, we send a simple lemma that asserts that the value is greater or equal to negative one.

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 4f1e41ebb87abe198de0f8700828c82192c9ff8c..3d898b40b9879e45e9755df325ef1d2aa015ddcb 100644 (file)
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -225,6 +225,10 @@ void TermRegistry::registerTerm(Node n, int effort)
                             nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
                             nm->mkNode(LEQ, n, len));
   }
+  else if (n.getKind() == STRING_STOI)
+  {
+    regTermLem = nm->mkNode(GEQ, n, nm->mkConst(Rational(-1)));
+  }
   if (!regTermLem.isNull())
   {
     Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem