From e5e6f481f9ffdcc6c2fdf5560563946b0bece242 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 25 Mar 2020 04:05:58 -0700
Subject: [PATCH] update bounds and assert values during initialization

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

diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp
index 6f5349967..0e4c9a9a0 100644
--- a/src/opt/maxlex.cpp
+++ b/src/opt/maxlex.cpp
@@ -129,6 +129,18 @@ namespace opt {
             for (auto & soft : m_soft) {
                 soft.set_value(l_undef);
             }
+            model_ref mdl;
+            s().get_model(mdl);
+            if (mdl) {
+                for (auto & soft : m_soft) {
+                    if (!mdl->is_true(soft.s)) {
+                        break;
+                    }
+                    soft.set_value(l_true);
+                    assert_value(soft);
+                }
+                update_bounds();
+            }
         }
 
         //