From 0c402c2b3cc036748c83bd75629e9845f9b5a397 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 30 Apr 2020 18:48:21 -0500
Subject: [PATCH] Remove skolem share involving pre_first_ctn. (#4423)

This fixes a soundness issue in strings caused by an incorrect skolem share.

This adds a regression that corresponds to the rewrite that this skolem share was justified by, which is "sat" (the rewrite does not hold). This benchmark in fact was answered "unsat" by CVC4 prior to this PR.
---
 src/theory/strings/skolem_cache.cpp           |  9 --------
 test/regress/CMakeLists.txt                   |  1 +
 .../strings/pre_ctn_no_skolem_share.smt2      | 18 +++++++++++++++
 .../theory_strings_skolem_cache_black.h       | 22 -------------------
 4 files changed, 19 insertions(+), 31 deletions(-)
 create mode 100644 test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index bdce86d06..4d92c372f 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -182,15 +182,6 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
     b = b[1];
   }
 
-  if (id == SK_FIRST_CTN_PRE)
-  {
-    // SK_FIRST_CTN_PRE((str.substr x 0 n), y) ---> SK_FIRST_CTN_PRE(x, y)
-    while (a.getKind() == kind::STRING_SUBSTR && a[1] == d_zero)
-    {
-      a = a[0];
-    }
-  }
-
   Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
                         << ", " << b << ")" << std::endl;
   return std::make_tuple(id, a, b);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 38b741ced..1dcdb0a44 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1775,6 +1775,7 @@ set(regress_1_tests
   regress1/strings/nterm-re-inter-sigma.smt2
   regress1/strings/pierre150331.smt2
   regress1/strings/policy_variable.smt2
+  regress1/strings/pre_ctn_no_skolem_share.smt2
   regress1/strings/query4674.smt2
   regress1/strings/query8485.smt2
   regress1/strings/re-all-char-hard.smt2
diff --git a/test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2 b/test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2
new file mode 100644
index 000000000..277a14df8
--- /dev/null
+++ b/test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2
@@ -0,0 +1,18 @@
+(set-info :smt-lib-version 2.6)
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun z () String)
+(declare-fun n () Int)
+(declare-fun y () String)
+
+;(define-fun z () String "AB")
+;(define-fun n () Int 0)
+;(define-fun y () String "B")
+
+(assert (not (=
+(str.substr (str.substr z 0 n) 0 (str.indexof (str.substr z 0 n) y 0))
+(str.substr z 0 (str.indexof z y 0))
+)))
+
+(check-sat)
+(get-model)
diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h
index 8f41153f3..7cb735a16 100644
--- a/test/unit/theory/theory_strings_skolem_cache_black.h
+++ b/test/unit/theory/theory_strings_skolem_cache_black.h
@@ -72,28 +72,6 @@ class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite
       Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
       TS_ASSERT_EQUALS(s1, s2);
     }
-
-    // Check that skolems are shared between:
-    //
-    // SK_FIRST_CTN(c, b)
-    //
-    // SK_FIRST_CTN((str.substr c), b)
-    {
-      Node s1 = sk.mkSkolemCached(c, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
-      Node s2 = sk.mkSkolemCached(sc, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
-      TS_ASSERT_EQUALS(s1, s2);
-    }
-
-    // Check that skolems are shared between:
-    //
-    // SK_PURIFY((str.substr a 0 (str.indexof a b 0)))
-    //
-    // SK_FIRST_CTN(a, b)
-    {
-      Node s1 = sk.mkSkolemCached(sa, b, SkolemCache::SK_PURIFY, "foo");
-      Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
-      TS_ASSERT_EQUALS(s1, s2);
-    }
   }
 
  private:
-- 
2.30.2