From bfed237a6cd42a129ef4e280d8dd28e7ec454bac Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 1 Jul 2025 14:14:16 -0700
Subject: [PATCH] expose scope level

---
 src/math/lp/lar_solver.cpp | 4 ++++
 src/math/lp/lar_solver.h   | 1 +
 2 files changed, 5 insertions(+)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 14faba63c..5fbde7f42 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -528,6 +528,10 @@ namespace lp {
         m_imp->m_usage_in_terms.push();
         m_imp->m_dependencies.push_scope();
     }
+
+    unsigned lar_solver::get_scope_level() const {
+        return m_imp->m_trail.get_num_scopes();
+    }
     
     void lar_solver::clean_popped_elements(unsigned n, indexed_uint_set& set) {
         vector<int> to_remove;
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 468601aa2..0f84df63b 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -503,6 +503,7 @@ public:
     const constraint_set & constraints() const;
     void push();
     void pop();
+    unsigned get_scope_level() const;
 
     u_dependency* get_column_lower_bound_witness(unsigned j) const;