From d3c85276c4e7ae06f0c4f2f299c9eda9924358d9 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 23 Jan 2020 18:51:53 -0800
Subject: Make skolem depurification an option

---
 src/options/strings_options.toml    | 9 +++++++++
 src/theory/strings/skolem_cache.cpp | 4 ++--
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 809f48b6d..471a69d71 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -241,6 +241,15 @@ header = "options/strings_options.h"
   read_only  = true
   help       = "use skolem sharing"
 
+[[option]]
+  name       = "skolemDepurification"
+  category   = "expert"
+  long       = "skolem-depurification"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "perform skolem depurification in skolem normalization"
+
 [[option]]
   name       = "stringRegExpInterMode"
   category   = "expert"
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 81cbd235d..bdfdeb7cd 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -66,7 +66,7 @@ Node SkolemCache::mkTypedSkolemCached(
   {
     NodeManager* nm = NodeManager::currentNM();
     Node sk;
-    if (id == SK_PREFIX)
+    if (options::skolemDepurification() && id == SK_PREFIX)
     {
       Node da = depurify(a);
       Node db = depurify(b);
@@ -76,7 +76,7 @@ Node SkolemCache::mkTypedSkolemCached(
           SK_PURIFY,
           name, ls);
     }
-    else if (id == SK_SUFFIX_REM)
+    else if (options::skolemDepurification() && id == SK_SUFFIX_REM)
     {
       Node da = depurify(a);
       Node db = depurify(b);
-- 
cgit v1.2.3