Merge branch 'master' into fix2982fix2982

5 files changed, 26 insertions, 26 deletions

diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index 204a13583..f7513a401 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -204,7 +204,7 @@ class Mapper {
     } else {
       vector<Expr> children = e.getChildren();
       children.insert(children.begin(), setoperators[ make_pair(t, e.getKind()) ]);
-      ret = em->mkExpr(kind::APPLY, children);
+      ret = em->mkExpr(kind::APPLY_UF, children);
     }
     // cout << "returning " << ret  << endl;
     return ret;
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 2e50ade0c..47f29e814 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -599,30 +599,9 @@ Node TheoryStringsRewriter::rewriteArithEqualityExt(Node node)
 {
   Assert(node.getKind() == EQUAL && node[0].getType().isInteger());
 
-  NodeManager* nm = NodeManager::currentNM();
-
   // cases where we can solve the equality
-  for (unsigned i = 0; i < 2; i++)
-  {
-    if (node[i].isConst())
-    {
-      Node on = node[1 - i];
-      Kind onk = on.getKind();
-      if (onk == STRING_STOI)
-      {
-        Rational r = node[i].getConst<Rational>();
-        int sgn = r.sgn();
-        Node onEq;
-        std::stringstream ss;
-        if (sgn >= 0)
-        {
-          ss << r.getNumerator();
-        }
-        Node new_ret = on[0].eqNode(nm->mkConst(String(ss.str())));
-        return returnRewrite(node, new_ret, "stoi-solve");
-      }
-    }
-  }
+
+  // notice we cannot rewrite str.to.int(x)=n to x="n" due to leading zeroes.
 
   return node;
 }
@@ -1490,7 +1469,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
       if(s.isNumber()) {
         retNode = nm->mkConst(s.toNumber());
       } else {
-        retNode = nm->mkConst(::CVC4::Rational(-1));
+        retNode = nm->mkConst(Rational(-1));
       }
     } else if(node[0].getKind() == kind::STRING_CONCAT) {
       for(unsigned i=0; i<node[0].getNumChildren(); ++i) {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 85dfd4c45..714459a85 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -846,7 +846,6 @@ set(regress_0_tests
   regress0/strings/rewrites-re-concat.smt2
   regress0/strings/rewrites-v2.smt2
   regress0/strings/std2.6.1.smt2
-  regress0/strings/stoi-solve.smt2
   regress0/strings/str003.smt2
   regress0/strings/str004.smt2
   regress0/strings/str005.smt2
@@ -1537,6 +1536,7 @@ set(regress_1_tests
   regress1/strings/issue1684-regex.smt2
   regress1/strings/issue2060.smt2
   regress1/strings/issue2429-code.smt2
+  regress1/strings/issue2981.smt2
   regress1/strings/issue2982.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
@@ -1570,6 +1570,7 @@ set(regress_1_tests
   regress1/strings/replaceall-replace.smt2
   regress1/strings/rew-020618.smt2
   regress1/strings/stoi-400million.smt2
+  regress1/strings/stoi-solve.smt2
   regress1/strings/str-code-sat.smt2
   regress1/strings/str-code-unsat-2.smt2
   regress1/strings/str-code-unsat-3.smt2
diff --git a/test/regress/regress1/strings/issue2981.smt2 b/test/regress/regress1/strings/issue2981.smt2
new file mode 100644
index 000000000..78cdb2a8c
--- /dev/null
+++ b/test/regress/regress1/strings/issue2981.smt2
@@ -0,0 +1,20 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_SLIA)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-const x String)
+(declare-const y String)
+(declare-const m String)
+(declare-const n String)
+(assert (str.in.re x (re.+ (re.range "0" "9"))))
+(assert (= 0 (str.to.int x)))                   
+(assert (not (= x ""))) 
+(assert (not (= x "0")))
+(assert (not (= x "3")))
+(assert (not (= x "T")))
+(assert (not (= x "8")))
+(assert (not (= x ""))) 
+(assert (not (= x "5")))
+(assert (not (= x "<")))
+(assert (not (= x "N")))               
+(check-sat)
diff --git a/test/regress/regress0/strings/stoi-solve.smt2 b/test/regress/regress1/strings/stoi-solve.smt2
index 4fbbdcfc1..4fbbdcfc1 100644
--- a/test/regress/regress0/strings/stoi-solve.smt2
+++ b/test/regress/regress1/strings/stoi-solve.smt2