diff --git a/src/tests/util/sexpr.cpp b/src/tests/util/sexpr.cpp
index 9f867ebf8..c0a14b00a 100644
--- a/src/tests/util/sexpr.cpp
+++ b/src/tests/util/sexpr.cpp
@@ -174,6 +174,34 @@ static void tst7() {
     std::cout << mk_pair(f, update(options({"pp", "width"}, 1000), {"pp", "colors"}, false)) << "\n";
 }
 
+static void tst8() {
+    lean_assert(!(sexpr("foo") == sexpr(10)));
+    lean_assert(sexpr() == sexpr());
+    lean_assert(sexpr(true) == sexpr(true));
+    lean_assert(sexpr(false) != sexpr(true));
+    sexpr s1(10);
+    sexpr s2 = s1;
+    lean_assert(cmp(s1, s2) == 0);
+    lean_assert(cmp(s1, sexpr(20)) < 0);
+    lean_assert(cmp(sexpr(), sexpr()) == 0);
+    lean_assert(cmp(sexpr("aaa"), sexpr("aaa")) == 0);
+    lean_assert(cmp(sexpr("bbb"), sexpr("aaa")) > 0);
+    lean_assert(cmp(sexpr(true), sexpr(true)) == 0);
+    lean_assert(cmp(sexpr(true), sexpr(false)) > 0);
+    lean_assert(cmp(sexpr(false), sexpr(true)) < 0);
+    lean_assert(cmp(sexpr(1.0), sexpr(2.0)) < 0);
+    lean_assert(cmp(sexpr(name("aaa")), sexpr(name("aaa"))) == 0);
+    lean_assert(cmp(sexpr(name("aaa")), sexpr(name("bbb"))) < 0);
+    lean_assert(cmp(sexpr(mpz(10)), sexpr(mpz(10))) == 0);
+    lean_assert(cmp(sexpr(mpz(20)), sexpr(mpz(10))) > 0);
+    lean_assert(cmp(sexpr(mpq(1,2)), sexpr(mpq(1,2))) == 0);
+    lean_assert(cmp(sexpr(mpq(1,3)), sexpr(mpq(1,2))) < 0);
+    std::ostringstream s;
+    s << sexpr() << " " << sexpr(mpq(1,2));
+    std::cout << s.str() << "\n";
+    lean_assert(s.str() == "nil 1/2");
+}
+
 int main() {
     tst1();
     tst2();
@@ -182,5 +210,6 @@ int main() {
     tst5();
     tst6();
     tst7();
+    tst8();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp
index 8f534eea4..da31b9108 100644
--- a/src/util/sexpr/sexpr.cpp
+++ b/src/util/sexpr/sexpr.cpp
@@ -95,7 +95,7 @@ struct sexpr_cons : public sexpr_cell {
 
 void sexpr_cell::dealloc() {
     switch (m_kind) {
-    case sexpr_kind::NIL:         lean_unreachable();                      break;
+    case sexpr_kind::NIL:         lean_unreachable();                      break; // LCOV_EXCL_LINE
     case sexpr_kind::STRING:      delete static_cast<sexpr_string*>(this); break;
     case sexpr_kind::BOOL:        delete static_cast<sexpr_bool*>(this);   break;
     case sexpr_kind::INT:         delete static_cast<sexpr_int*>(this);    break;
@@ -192,7 +192,8 @@ bool operator==(sexpr const & a, sexpr const & b) {
     case sexpr_kind::MPQ:         return to_mpq(a) == to_mpq(b);
     case sexpr_kind::CONS:        return head(a) == head(b) && tail(a) == tail(b);
     }
-    return false;
+    lean_unreachable(); // LCOV_EXCL_LINE
+    return false;       // LCOV_EXCL_LINE
 }
 
 int cmp(sexpr const & a, sexpr const & b) {
@@ -221,7 +222,8 @@ int cmp(sexpr const & a, sexpr const & b) {
             return r;
         return cmp(tail(a), tail(b));
     }}
-    return 0;
+    lean_unreachable(); // LCOV_EXCL_LINE
+    return 0;           // LCOV_EXCL_LINE
 }
 
 std::ostream & operator<<(std::ostream & out, sexpr const & s) {
@@ -258,7 +260,6 @@ std::ostream & operator<<(std::ostream & out, sexpr const & s) {
 bool operator==(sexpr const & a, name const & b) { return is_name(a) && to_name(a) == b; }
 bool operator==(sexpr const & a, mpz const & b) { return is_mpz(a) && to_mpz(a) == b; }
 bool operator==(sexpr const & a, mpq const & b) { return is_mpq(a) && to_mpq(a) == b; }
-
 }
 
 void print(lean::sexpr const & n) { std::cout << n << "\n"; }