From fdac93fff30fcb093474c009203f472f5326979c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 26 Sep 2025 23:05:02 +0300
Subject: [PATCH] v0.1 of nla saturation

---
 .clang-format            | 1 +
 src/math/lp/nla_core.cpp | 1 +
 src/smt/theory_lra.cpp   | 5 ++++-
 3 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/.clang-format b/.clang-format
index 676707898..c6d1e16b7 100644
--- a/.clang-format
+++ b/.clang-format
@@ -8,6 +8,7 @@ BasedOnStyle: LLVM
 IndentWidth: 4
 TabWidth: 4
 UseTab: Never
+IndentCaseLabels: false
 
 
 
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 1cefffec5..b7085086c 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1318,6 +1318,7 @@ lbool core::check() {
             return l_false;
     }
 
+
     if (no_effect() && lp_settings().m_enable_stellensatz)
         ret = m_stellensatz.saturate();
     
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 605c88599..15c60f0a2 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3475,9 +3475,12 @@ public:
         ++m_stats.m_conflicts;
         for (auto ev : m_explanation)
             set_evidence(ev.ci(), m_core, m_eqs);
-
         if (m_eqs.empty() && all_of(m_core, [&](literal l) { return ctx().get_assignment(l) == l_false; }))
             is_conflict = true;
+        for (auto l : m_core) {
+            IF_VERBOSE(1, verbose_stream() << l << " " << ctx().get_assignment(l) << "\n");
+        }
+
         TRACE(arith_conflict,
               tout << "@" << ctx().get_scope_level() << (is_conflict ? " conflict":" lemma");
               for (auto const& p : m_params) tout << " " << p;