From 480e1c4daba6a9f5cae5a7c12010613e88584cae Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 23 Apr 2018 07:20:24 +0200
Subject: [PATCH] add warning message for optimization with quantifiers. Fix
 #1580

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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;
     }