From c2610cb37c214a1a58c4cd992bf0a2349d4fc6a2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Nov 2023 14:32:53 -0800
Subject: [PATCH] #6523
malformed models on giveup status
---
src/sat/smt/arith_solver.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 2a9566873..fe7b0aa46 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -632,7 +632,7 @@ namespace arith {
else if (v != euf::null_theory_var) {
rational r = get_value(v);
TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
- SASSERT("integer variables should have integer values: " && (ctx.get_config().m_arith_ignore_int || !a.is_int(o) || r.is_int() || m.limit().is_canceled()));
+ SASSERT("integer variables should have integer values: " && (ctx.get_config().m_arith_ignore_int || !a.is_int(o) || r.is_int() || m_not_handled != nullptr || m.limit().is_canceled()));
if (a.is_int(o) && !r.is_int())
r = floor(r);
value = a.mk_numeral(r, o->get_sort());