diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1950a199d..69177e290 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -265,6 +265,9 @@ namespace opt { normalize(); internalize(); update_solver(); + if (contains_quantifiers()) { + warning_msg("optimization with quantified constraints is not supported"); + } #if 0 if (is_qsat_opt()) { return run_qsat_opt(); @@ -368,7 +371,6 @@ namespace opt { if (result == l_true && committed) m_optsmt.commit_assignment(index); if (result == l_true && m_optsmt.is_unbounded(index, is_max) && contains_quantifiers()) { throw default_exception("unbounded objectives on quantified constraints is not supported"); - result = l_undef; } return result; }