Add approx opt

2 files changed, 10 insertions, 1 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index ab32ddbec..dd9599c5c 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -245,6 +245,15 @@ header = "options/strings_options.h"
   help       = "Enable the entailment checks in the strings rewriter"
 
 [[option]]
+  name       = "stringsRewriterApprox"
+  category   = "expert"
+  long       = "strings-rewriter-entail-approx"
+  type       = "bool"
+  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"
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 061493b96..b0ad90c29 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -3925,7 +3925,7 @@ bool TheoryStringsRewriter::checkEntailArith(Node a, bool strict)
   }
 
   bool ret = checkEntailArithInternal(ar);
-  if (!ret)
+  if (!ret && options::stringsRewriterApprox())
   {
     // try with approximations
     ret = checkEntailArithApprox(ar);