Do not apply unconstrained simplification when quantifiers are present (#4532)

Fixes #4437.

This is a simpler fix that aborts the preprocessing pass when a quantifier is encountered.

It also updates our smt2 parser to throw a logic exception when forall/exists is used in non-quantified logics. This is required to ensure that unconstrained simplification does not throw an exception to a user as a result of accidentally setting the wrong logic.

2 files changed, 14 insertions, 1 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)
diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h
index ac4fd0a03..7fc13e17d 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.h
+++ b/src/preprocessing/passes/unconstrained_simplifier.h
@@ -62,7 +62,11 @@ class UnconstrainedSimplifier : public PreprocessingPass
   theory::SubstitutionMap d_substitutions;
 
   const LogicInfo& d_logicInfo;
-
+  /**
+   * Visit all subterms in assertion. This method throws a LogicException if
+   * there is a subterm that is unhandled by this preprocessing pass (e.g. a
+   * quantified formula).
+   */
   void visitAll(TNode assertion);
   Node newUnconstrainedVar(TypeNode t, TNode var);
   void processUnconstrained();