diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 08027558f..83e573b14 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1067,10 +1067,12 @@ lemma_builder::~lemma_builder() {
     TRACE(nla_solver, tout << name << " " << (++i) << "\n" << *this; );
 }
 
-lemma& lemma_builder::current() const {
+lemma& lemma_builder::current() {
+    return c.m_lemmas.back();
+}
+const lemma& lemma_builder::current() const {
     return c.m_lemmas.back();
 }
-
 lemma_builder& lemma_builder::operator&=(lp::explanation const& e) {
     expl().add_expl(e);
     return *this;
diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h
index 2f061559d..c300d72c1 100644
--- a/src/math/lp/nla_types.h
+++ b/src/math/lp/nla_types.h
@@ -60,6 +60,7 @@ namespace nla {
         lp::explanation& expl() { return m_expl; }
         const lp::explanation& expl() const { return m_expl; }
         bool is_conflict() const { return m_ineqs.empty() && !m_expl.empty(); }
+        bool is_empty() const { return m_ineqs.empty() && m_expl.empty(); }
     };
     
     class core;
@@ -72,12 +73,13 @@ namespace nla {
     class lemma_builder {
         char const* name;
         core& c;
-        lemma& current() const;
+        // the non-const version is private
+        lemma& current();
+        const lemma& current() const;
         
     public:
         lemma_builder(core& c, char const* name);
         ~lemma_builder();
-        lemma& operator()() { return current(); }
         std::ostream& display(std::ostream& out) const;
         lemma_builder& operator&=(lp::explanation const& e);
         lemma_builder& operator&=(const monic& m);