From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 16 Jan 2019 05:15:27 +0000 (-0600)
Subject: Fix constant contains ITOS rewrite (#2799)
X-Git-Tag: cvc5-1.0.0~4284
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=534a9b73dae2c0a3b6040f6a51f824ca69850c4b;p=cvc5.git

Fix constant contains ITOS rewrite (#2799)
---

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 57a99532e..b4c80e55b 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -3234,7 +3234,7 @@ bool TheoryStringsRewriter::canConstantContainConcat( Node c, Node n, int& first
         pos = new_pos + s.size();
       }
     }
-    else if (n[i].getKind() == kind::STRING_ITOS)
+    else if (n[i].getKind() == kind::STRING_ITOS && checkEntailArith(n[i][0]))
     {
       // find the first occurrence of a digit starting at pos
       while (pos < tvec.size() && !String::isDigit(tvec[pos]))
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index dbefe3af2..15dbf0df8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -822,6 +822,7 @@ set(regress_0_tests
   regress0/strings/ilc-like.smt2
   regress0/strings/indexof-sym-simp.smt2
   regress0/strings/issue1189.smt2
+  regress0/strings/itos-entail.smt2
   regress0/strings/leadingzero001.smt2
   regress0/strings/loop001.smt2
   regress0/strings/model001.smt2
diff --git a/test/regress/regress0/strings/itos-entail.smt2 b/test/regress/regress0/strings/itos-entail.smt2
new file mode 100644
index 000000000..f9dcf4c77
--- /dev/null
+++ b/test/regress/regress0/strings/itos-entail.smt2
@@ -0,0 +1,11 @@
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status sat)
+(set-option :strings-exp true)
+(declare-fun x () Int)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (str.contains "ABCD" (str.++ y (int.to.str x) z)))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/rewrites-v2.smt2 b/test/regress/regress0/strings/rewrites-v2.smt2
index ce2f140ae..15954525f 100644
--- a/test/regress/regress0/strings/rewrites-v2.smt2
+++ b/test/regress/regress0/strings/rewrites-v2.smt2
@@ -5,12 +5,12 @@
 (set-info :status unsat)
 (declare-fun x () String)
 (declare-fun y () String)
-(declare-fun z () Int)
+(declare-fun z () String)
 
 ; these should all rewrite to false
 (assert (or
-(str.contains "abcdef0ghij1abced" (str.++ "g" (int.to.str z) x "a" y (int.to.str (+ z 1))))
-(str.contains "abc23cd" (str.++ (int.to.str z) (int.to.str z) (int.to.str z)))
+(str.contains "abcdef0ghij1abced" (str.++ "g" (int.to.str (str.len z)) x "a" y (int.to.str (+ (str.len z) 1))))
+(str.contains "abc23cd" (str.++ (int.to.str (str.len z)) (int.to.str (str.len z)) (int.to.str (str.len z))))
 (not (str.contains (str.++ x "ab" y) (str.++ "b" (str.substr y 0 4))))
 (not (str.contains (str.++ x "ab" y) (str.++ (str.substr x 5 (str.len x)) "a")))
 (str.contains (str.++ x y) (str.++ x "a" y))