Remove stdPrintAscii option (#6280)

Fixes #4179.

3 files changed, 0 insertions, 22 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 75da2a35b..208b4483f 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -11,15 +11,6 @@ header = "options/strings_options.h"
   help       = "experimental features in the theory of strings"
 
 [[option]]
-  name       = "stdPrintASCII"
-  category   = "regular"
-  long       = "strings-print-ascii"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "the alphabet contains only printable characters from the standard extended ASCII"
-
-[[option]]
   name       = "stringFMF"
   category   = "regular"
   long       = "strings-fmf"
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 0892af4de..4baabec69 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -340,14 +340,6 @@ public:
       if(ch[0] > ch[1]) {
         throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
       }
-      unsigned maxCh = options::stdPrintASCII() ? 127 : 255;
-      if (ch[1] > maxCh)
-      {
-        std::stringstream ss;
-        ss << "expecting characters whose code point is less than or equal to "
-           << maxCh;
-        throw TypeCheckingExceptionPrivate(n, ss.str());
-      }
     }
     return nodeManager->regExpType();
   }
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 510214e0f..8a2f3fe62 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -33,11 +33,6 @@ namespace utils {
 
 uint32_t getAlphabetCardinality()
 {
-  if (options::stdPrintASCII())
-  {
-    Assert(128 <= String::num_codes());
-    return 128;
-  }
   // 3*16^4 = 196608 values in the SMT-LIB standard for Unicode strings
   Assert(196608 <= String::num_codes());
   return 196608;