fix #6997

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Nov 16, 2023 · 5b9fdcf · 5b9fdcf
1 parent f1a39b8
commit 5b9fdcf
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
@@ -316,7 +316,7 @@ class create_cut {
         lar_term t = lia.lra.unfold_nested_subterms(m_t);
         auto pol = t.coeffs_as_vector();
         m_t.clear();
-        if (pol.size() == 1) {
+        if (pol.size() == 1 && is_int(pol[0].second)) {
             TRACE("gomory_cut_detail", tout << "pol.size() is 1" << std::endl;);
             auto const& [a, v] = pol[0];
             lp_assert(is_int(v));