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;