diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 4d5bfe765..88812df15 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1674,6 +1674,20 @@ namespace z3 {
         return func_decl(c, f);
     }
 
+    /**
+       \brief signed less than or equal to operator for bitvectors.
+    */
+    inline expr sle(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsle(a.ctx(), a, b)); }
+    inline expr sle(expr const & a, int b) { return sle(a, a.ctx().num_val(b, a.get_sort())); }
+    inline expr sle(int a, expr const & b) { return sle(b.ctx().num_val(a, b.get_sort()), b); }
+    /**
+       \brief signed less than operator for bitvectors.
+    */
+    inline expr slt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvslt(a.ctx(), a, b)); }
+    inline expr slt(expr const & a, int b) { return slt(a, a.ctx().num_val(b, a.get_sort())); }
+    inline expr slt(int a, expr const & b) { return slt(b.ctx().num_val(a, b.get_sort()), b); }
+
+
     /**
        \brief unsigned less than or equal to operator for bitvectors.
     */
@@ -2337,7 +2351,7 @@ namespace z3 {
             check_error();
             return to_check_result(r);
         }
-        check_result check(expr_vector assumptions) {
+        check_result check(expr_vector const& assumptions) {
             unsigned n = assumptions.size();
             array<Z3_ast> _assumptions(n);
             for (unsigned i = 0; i < n; i++) {
diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp
index 6979ac149..36910a47b 100644
--- a/src/util/symbol.cpp
+++ b/src/util/symbol.cpp
@@ -141,6 +141,10 @@ bool lt(symbol const & s1, symbol const & s2) {
         SASSERT(!s1.is_numerical());
         return false;
     }
+    if (!s1.bare_str())
+        return true;
+    if (!s2.bare_str())
+        return false;
     SASSERT(!s1.is_numerical() && !s2.is_numerical());
     auto cmp = strcmp(s1.bare_str(), s2.bare_str());
     SASSERT(cmp != 0);