fix #5675

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Nov 19, 2021 · 4928c28 · 4928c28
1 parent 99d5215
commit 4928c28
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -3477,7 +3477,7 @@ class theory_lra::imp {
                 st = lp::lp_status::FEASIBLE;
                 lp().restore_x();
             }
-            if (m_nla && st == lp::lp_status::OPTIMAL) {
+            if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) {
                 st = lp::lp_status::FEASIBLE;
                 lp().restore_x();
             }