From ca5fd891038a93bd63b3863faa8c5e39fff88ed0 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 5 Apr 2021 12:17:39 -0500
Subject: Enable UF when pre-skolem nested option is enabled (#6282)

Fixes #4328.
---
 src/smt/set_defaults.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src')

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 5fed0d664..6c10eeb94 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -631,6 +631,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     Notice() << "Enabling UF because bvAbstraction requires it." << std::endl;
     needsUf = true;
   }
+  else if (options::preSkolemQuantNested()
+           && options::preSkolemQuantNested.wasSetByUser())
+  {
+    // if pre-skolem nested is explictly set, then we require UF. If it is
+    // not explicitly set, it is disabled below if UF is not present.
+    Notice() << "Enabling UF because preSkolemQuantNested requires it."
+             << std::endl;
+    needsUf = true;
+  }
   if (needsUf
       // Arrays, datatypes and sets permit Boolean terms and thus require UF
       || logic.isTheoryEnabled(THEORY_ARRAYS)
-- 
cgit v1.2.3