add option to disable contains commit

2 files changed, 14 insertions, 0 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index bc5fbedd6..17d68b3b7 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -243,3 +243,12 @@ header = "options/strings_options.h"
   default    = "true"
   read_only  = true
   help       = "Enable the entailment checks in the strings rewriter"
+
+[[option]]
+  name       = "stringsRewriterEntailContainsChecks"
+  category   = "expert"
+  long       = "strings-rewriter-entail-contains-checks"
+  type       = "bool"
+  default    = "true"
+  read_only  = true
+  help       = "Enable the contains entailment checks in the strings rewriter"
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index e1f119244..ae3afb65c 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -3919,6 +3919,11 @@ Node TheoryStringsRewriter::checkEntailContains(Node a,
                                                 Node b,
                                                 bool fullRewriter)
 {
+  if (!options::stringsRewriterEntailContainsChecks())
+  {
+    return Node::null();
+  }
+
   NodeManager* nm = NodeManager::currentNM();
   Node ctn = nm->mkNode(kind::STRING_STRCTN, a, b);