diff --git a/src/tests/util/options.cpp b/src/tests/util/options.cpp
index 8d07a85060..7514617ae7 100644
--- a/src/tests/util/options.cpp
+++ b/src/tests/util/options.cpp
@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "options.h"
+#include <cstring>
+#include <sstream>
 #include "test.h"
+#include "options.h"
 using namespace lean;
 
 static void tst1() {
@@ -39,9 +41,76 @@ static void tst3() {
     std::cout << pp(opt) << "\n";
 }
 
+static void tst4() {
+    options opt;
+    lean_assert(opt.empty());
+    lean_assert(opt.size() == 0);
+    opt = update(opt, "color", 10);
+    lean_assert(!opt.empty());
+    lean_assert(opt.size() == 1);
+    lean_assert(opt.contains("color"));
+    lean_assert(!opt.contains("name"));
+    std::cout << opt << "\n";
+    lean_assert(opt.get_int(name("color"), 0) == 10);
+    lean_assert(opt.get_int("color", 0) == 10);
+    lean_assert(opt.get_int("name", 20) == 20);
+    opt = update(opt, "color", 3);
+    lean_assert(opt.size() == 1);
+    lean_assert(opt.get_int("color", 0) == 3);
+    opt = update(opt, "freq", 0.5);
+    std::cout << opt << "\n";
+    lean_assert(opt.size() == 2);
+    lean_assert(opt.get_double("freq", 0.0) == 0.5);
+    lean_assert(opt.get_double(name("freq"), 0.0) == 0.5);
+    lean_assert(opt.get_unsigned("color", 0) == 3);
+    lean_assert(opt.get_unsigned(name("color"), 0) == 3);
+    opt = update(opt, "name", "Leo");
+    lean_assert(opt.size() == 3);
+    lean_assert(strcmp(opt.get_string("name", ""), "Leo") == 0);
+    lean_assert(strcmp(opt.get_string("name2", ""), "Leo") != 0);
+    lean_assert(strcmp(opt.get_string("name2", ""), "") == 0);
+    opt = update(opt, "name", "Soon Ho");
+    lean_assert(opt.size() == 3);
+    lean_assert(strcmp(opt.get_string("name", ""), "Soon Ho") == 0);
+    opt = update(opt, "flag", true);
+    lean_assert(opt.get_bool("flag", false));
+    lean_assert(opt.get_bool(name("flag"), false));
+    lean_assert(!opt.get_bool("flag2", false));
+    opt = update(opt, "list", sexpr{1, 2, 3});
+    std::cout << opt << "\n";
+    lean_assert(opt.get_sexpr("list", sexpr()) == sexpr({1, 2, 3}));
+    lean_assert(opt.get_sexpr(name("list"), sexpr()) == sexpr({1, 2, 3}));
+    lean_assert(opt.contains("name"));
+    lean_assert(!opt.contains("name2"));
+    lean_assert(opt.contains("color"));
+    options opt2;
+    opt2 = update(opt2, "name", "Leo");
+    opt2 = update(opt2, "value", 10);
+    opt2 = update(opt2, "flag", false);
+    std::cout << "# " << opt << "\n# " << opt2 << "\n";
+    options opt3 = join(opt, opt2);
+    std::cout << "> " << opt3 << "\n";
+    lean_assert(strcmp(opt3.get_string("name", ""), "Leo") == 0);
+    lean_assert(opt3.get_unsigned("value", 0) == 10);
+    lean_assert(opt3.get_unsigned("color", 0) == 3);
+    lean_assert(opt3.get_double(name("freq"), 0.0) == 0.5);
+    lean_assert(opt3.get_unsigned(name("freq"), 0) == 0);
+    std::ostringstream s;
+    option_kind k;
+    k = BoolOption; s << k << " ";
+    k = IntOption; s << k << " ";
+    k = UnsignedOption; s << k << " ";
+    k = DoubleOption; s << k << " ";
+    k = StringOption; s << k << " ";
+    k = SExprOption; s << k;
+    std::cout << s.str() << "\n";
+    lean_assert(s.str() == "Bool Int Unsigned Int Double String S-Expression");
+}
+
 int main() {
     tst1();
     tst2();
     tst3();
+    tst4();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/sexpr/options.cpp b/src/util/sexpr/options.cpp
index 0c33c30233..3a680f9f11 100644
--- a/src/util/sexpr/options.cpp
+++ b/src/util/sexpr/options.cpp
@@ -42,7 +42,7 @@ bool options::empty() const {
     return is_nil(m_value);
 }
 
-bool options::size() const {
+unsigned options::size() const {
     return length(m_value);
 }
 
@@ -86,7 +86,7 @@ char const * options::get_string(name const & n, char const * default_value) con
 
 sexpr options::get_sexpr(char const * n, sexpr const & default_value) const {
     sexpr const * r = find(m_value, [&](sexpr const & p) { return to_name(head(p)) == n; });
-    return r == nullptr ? default_value : *r;
+    return r == nullptr ? default_value : tail(*r);
 }
 
 int options::get_int(char const * n, int default_value) const {
diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h
index 45c0c1d4a1..e4b7828563 100644
--- a/src/util/sexpr/options.h
+++ b/src/util/sexpr/options.h
@@ -28,7 +28,7 @@ public:
     options & operator=(options const & o) { m_value = o.m_value; return *this; }
 
     bool empty() const;
-    bool size() const;
+    unsigned size() const;
     bool contains(name const & n) const;
     bool contains(char const * n) const;