diff --git a/src/api/python/z3rcf.py b/src/api/python/z3rcf.py
index 66a6890c3..84c724910 100644
--- a/src/api/python/z3rcf.py
+++ b/src/api/python/z3rcf.py
@@ -51,7 +51,6 @@ def MkRoots(p, ctx=None):
     return r
 
 class RCFNum:
-    html = False
     def __init__(self, num, ctx=None):
         # TODO: add support for converting AST numeral values into RCFNum
         if isinstance(num, RCFNumObj):
@@ -68,10 +67,10 @@ class RCFNum:
         return self.ctx.ref()
                   
     def __repr__(self):
-        return Z3_rcf_num_to_string(self.ctx_ref(), self.num, False, RCFNum.html)
+        return Z3_rcf_num_to_string(self.ctx_ref(), self.num, False, in_html_mode())
 
     def compact_str(self):
-        return Z3_rcf_num_to_string(self.ctx_ref(), self.num, True, RCFNum.html)
+        return Z3_rcf_num_to_string(self.ctx_ref(), self.num, True, in_html_mode())
 
     def __add__(self, other):
         v = _to_rcfnum(other, self.ctx)
diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp
index 8c6a1d232..87b1ef8a4 100644
--- a/src/math/realclosure/realclosure.cpp
+++ b/src/math/realclosure/realclosure.cpp
@@ -1300,7 +1300,7 @@ namespace realclosure {
         }
 
         void mk_infinitesimal(numeral & r) {
-            mk_infinitesimal(symbol(next_infinitesimal_idx()), symbol(next_infinitesimal_idx()), r);
+            mk_infinitesimal(symbol(next_infinitesimal_idx()+1), symbol(next_infinitesimal_idx()+1), r);
         }
 
         void refine_transcendental_interval(transcendental * t) {
@@ -1352,7 +1352,7 @@ namespace realclosure {
         }
 
         void mk_transcendental(mk_interval & proc, numeral & r) {
-            mk_transcendental(symbol(next_transcendental_idx()), symbol(next_transcendental_idx()), proc, r);
+            mk_transcendental(symbol(next_transcendental_idx()+1), symbol(next_transcendental_idx()+1), proc, r);
         }
 
         void mk_pi(numeral & r) {
diff --git a/src/util/ext_numeral.h b/src/util/ext_numeral.h
index 83d326243..03a364bdb 100644
--- a/src/util/ext_numeral.h
+++ b/src/util/ext_numeral.h
@@ -339,7 +339,7 @@ void display_pp(std::ostream & out,
                 ext_numeral_kind ak) {
     switch (ak) {
     case EN_MINUS_INFINITY: out << "-&infin;"; break;
-    case EN_NUMERAL: m.display(out, a); break;
+    case EN_NUMERAL: m.display_pp(out, a); break;
     case EN_PLUS_INFINITY: out << "+&infin;"; break;
     }
 }
diff --git a/src/util/mpbq.cpp b/src/util/mpbq.cpp
index ad2eae770..1ff7fb04d 100644
--- a/src/util/mpbq.cpp
+++ b/src/util/mpbq.cpp
@@ -399,6 +399,14 @@ void mpbq_manager::display(std::ostream & out, mpbq const & a) {
         out << "^" << a.m_k;
 }
 
+void mpbq_manager::display_pp(std::ostream & out, mpbq const & a) {
+    out << m_manager.to_string(a.m_num);
+    if (a.m_k > 0)
+        out << "/2";
+    if (a.m_k > 1)
+        out << "<sup>" << a.m_k << "</sup>";
+}
+
 void mpbq_manager::display_smt2(std::ostream & out, mpbq const & a, bool decimal) {
     if (a.m_k == 0) {
         m_manager.display_smt2(out, a.m_num, decimal);
diff --git a/src/util/mpbq.h b/src/util/mpbq.h
index 3427ab59f..85332d02f 100644
--- a/src/util/mpbq.h
+++ b/src/util/mpbq.h
@@ -260,6 +260,7 @@ public:
 
 
     void display(std::ostream & out, mpbq const & a);
+    void display_pp(std::ostream & out, mpbq const & a);
     void display_decimal(std::ostream & out, mpbq const & a, unsigned prec = 8);
     /**
        \brief Display a in decimal while its digits match b digits.
diff --git a/src/util/mpff.h b/src/util/mpff.h
index 0295901c4..de71ec75e 100644
--- a/src/util/mpff.h
+++ b/src/util/mpff.h
@@ -464,6 +464,7 @@ public:
 
     void display_raw(std::ostream & out, mpff const & n) const;
     void display(std::ostream & out, mpff const & n) const;
+    void display_pp(std::ostream & out, mpff const & n) const { display(out, n); }
     void display_decimal(std::ostream & out, mpff const & n, unsigned prec=32, unsigned max_power=128) const;
     void display_smt2(std::ostream & out, mpff const & n, bool decimal=true) const;
 
diff --git a/src/util/mpfx.h b/src/util/mpfx.h
index 476da79e3..b4eeaebe6 100644
--- a/src/util/mpfx.h
+++ b/src/util/mpfx.h
@@ -382,6 +382,7 @@ public:
     unsigned prev_power_of_two(mpfx const & a);
 
     void display(std::ostream & out, mpfx const & n) const;
+    void display_pp(std::ostream & out, mpfx const & n) const { display(out, n); }
     void display_smt2(std::ostream & out, mpfx const & n) const;
     void display_decimal(std::ostream & out, mpfx const & n, unsigned prec = UINT_MAX) const;
     void display_raw(std::ostream & out, mpfx const & n) const;
diff --git a/src/util/mpq.h b/src/util/mpq.h
index 26a34aff6..0c94936ba 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -259,6 +259,7 @@ public:
     void display(std::ostream & out, mpz const & a) const { return mpz_manager<SYNCH>::display(out, a); }
 
     void display(std::ostream & out, mpq const & a) const;
+    void display_pp(std::ostream & out, mpq const & a) const { display(out, a); }
 
     void display_smt2(std::ostream & out, mpz const & a, bool decimal) const { return mpz_manager<SYNCH>::display_smt2(out, a, decimal); }