From 8bd325cdaa6b292a8b89524d4851ccd23e400594 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 18 Jan 2019 18:12:49 -0800
Subject: add option to disable contains commit

---
 src/options/strings_options.toml               | 9 +++++++++
 src/theory/strings/theory_strings_rewriter.cpp | 5 +++++
 2 files changed, 14 insertions(+)

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);
 
-- 
cgit v1.2.3