fix #7493

Z3Prover · Feb 2, 2025 · 17d47ca · 17d47ca
1 parent 99cbfa7
commit 17d47ca
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 5 deletions.
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
@@ -241,6 +241,7 @@ namespace opt {
         smt::theory_var v = m_objective_vars[i];
         bool has_shared = false;
         m_last_model = nullptr;
+        blocker = nullptr;
         //
         // compute an optimization hint.
         // The hint is valid if there are no shared symbols (a pure LP).
@@ -256,6 +257,7 @@ namespace opt {
         if (!m_models[i]) 
             m_models.set(i, m_last_model.get());
 
+        TRACE("opt", tout << "maximize " << i << " " << val << " " << m_objective_values[i] << " " << blocker << "\n";);
         if (val > m_objective_values[i]) {
             m_objective_values[i] = val;
         }

diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
@@ -202,9 +202,6 @@ namespace opt {
         for (unsigned i = 0; i < obj_index; ++i) 
             commit_assignment(i);
 
-//        m_s->maximize_objective(obj_index, bound);
-//        m_s->assert_expr(bound);
-
         unsigned steps = 0;
         unsigned step_incs = 0;
         rational delta_per_step(1);
@@ -216,9 +213,10 @@ namespace opt {
             SASSERT(delta_per_step.is_pos());
             is_sat = m_s->check_sat(0, nullptr);
             TRACE("opt", tout << "check " << is_sat << "\n";
-                  tout << "last bound: " << last_bound << "\n";
+                  tout << "last bound: " << last_bound << " bound " << bound << "\n";
                   tout << "lower: " << m_lower[obj_index] << "\n";
                   tout << "upper: " << m_upper[obj_index] << "\n";
+                  if (is_sat == l_true) m_s->display(tout);
                   );
             if (is_sat == l_true) {                
                 m_s->maximize_objective(obj_index, bound);

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -3858,12 +3858,21 @@ class theory_lra::imp {
             vi = get_lpvar(v);
 
             st = lp().maximize_term(vi, term_max);
+
             if (has_int() && lp().has_inf_int()) {
                 st = lp::lp_status::FEASIBLE;
                 lp().restore_x();
             }
             if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) {
-                st = lp::lp_status::FEASIBLE;
+                switch (check_nla()) {
+                case FC_DONE:
+                    st = lp::lp_status::FEASIBLE;
+                    break;
+                case FC_GIVEUP:
+                case FC_CONTINUE:
+                    st = lp::lp_status::UNBOUNDED;
+                    break;
+                }                
                 lp().restore_x();
             }                
         }