Preprare central model building for RANs (#7951)

[cvc5.git] / src / smt / solver_engine.cpp

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 97774a739fc71a1ad5b86a27291e1c03c9543af5..ef25d7819b89d6855656a821a4b1cf3d4ab427aa 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1019,10 +1019,10 @@ Node SolverEngine::getValue(const Node& ex) const
          || resultNode.getType().isSubtypeOf(expectedType))
       << "Run with -t smt for details.";
 
-  // Ensure it's a constant, or a lambda (for uninterpreted functions). This
-  // assertion only holds for models that do not have approximate values.
-  Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA
-         || resultNode.isConst());
+  // Ensure it's a value (constant or const-ish like real algebraic
+  // numbers), or a lambda (for uninterpreted functions). This assertion only
+  // holds for models that do not have approximate values.
+  Assert(m->hasApproximations() || TheoryModel::isValue(resultNode));
 
   if (d_env->getOptions().smt.abstractValues && resultNode.getType().isArray())
   {