1 files changed, 9 insertions, 3 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index d6ad4cd41..b9dc1ba42 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -330,12 +330,18 @@ bool Theory::isLegalElimination(TNode x, TNode val)
   {
     return false;
   }
-  if (!options::produceModels())
+  if (!options::produceModels() && !d_logicInfo.isQuantified())
   {
-    // don't care about the model, we are fine
+    // Don't care about the model and logic is not quantified, we can eliminate.
     return true;
   }
-  // if there is a model object
+  // If models are enabled, then it depends on whether the term contains any
+  // unevaluable operators like FORALL, SINE, etc. Having such operators makes
+  // model construction contain non-constant values for variables, which is
+  // not ideal from a user perspective.
+  // We also insist on this check since the term to eliminate should never
+  // contain quantifiers, or else variable shadowing issues may arise.
+  // there should be a model object
   TheoryModel* tm = d_valuation.getModel();
   Assert(tm != nullptr);
   return tm->isLegalElimination(x, val);