1 files changed, 9 insertions, 0 deletions
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 5d544ae57..b74909824 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -91,6 +91,15 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
         d_unconstrained.insert(current);
       }
     }
+    else if (current.isClosure())
+    {
+      // Throw an exception. This should never happen in practice unless the
+      // user specifically enabled unconstrained simplification in an illegal
+      // logic.
+      throw LogicException(
+          "Cannot use unconstrained simplification in this logic, due to "
+          "(possibly internally introduced) quantified formula.");
+    }
     else
     {
       for (TNode childNode : current)