diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 57085a09e..fda1a78f3 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -1976,6 +1976,22 @@ public class Context implements AutoCloseable {
     {
         return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s));
     }
+
+    /**
+     * Convert an integer expression to a string.
+     */
+    public SeqExpr intToString(Expr e) 
+    {
+	return (SeqExpr) Expr.create(this, Native.Z3_mkIntToStr(nCtx(), e.getNativeObject()));
+    }
+
+    /**
+     * Convert an integer expression to a string.
+     */
+    public IntExpr stringToInt(Expr e)  
+    {
+	return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
+    }
     
     /**
      * Concatenate sequences.
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 8d7639851..8741ec419 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -292,7 +292,7 @@ namespace opt {
             model_updated(m_model.get());
         }
         if (is_sat != l_true) {
-            TRACE("opt", tout << m_hard_constraints << "\n";);            
+            TRACE("opt", tout << m_hard_constraints << " " << asms << "\n";);            
             if (!asms.empty()) {
                 s.get_unsat_core(m_core);
             }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 1d49c4386..24309ba88 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1412,7 +1412,7 @@ public:
     }
 
     final_check_status final_check_eh() {
-        IF_VERBOSE(2, verbose_stream() << "final-check\n");
+        IF_VERBOSE(2, verbose_stream() << "final-check " << m_solver->get_status() << "\n");
         m_use_nra_model = false;
         lbool is_sat = l_true;
         if (m_solver->get_status() != lp::lp_status::OPTIMAL) {