diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt
index 3a0cd42c6..6970390c8 100644
--- a/src/tests/library/CMakeLists.txt
+++ b/src/tests/library/CMakeLists.txt
@@ -16,3 +16,6 @@ add_test(deep_copy ${CMAKE_CURRENT_BINARY_DIR}/deep_copy)
 add_executable(arith_tst arith.cpp)
 target_link_libraries(arith_tst ${EXTRA_LIBS})
 add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst)
+add_executable(update_expr update_expr.cpp)
+target_link_libraries(update_expr ${EXTRA_LIBS})
+add_test(update_expr ${CMAKE_CURRENT_BINARY_DIR}/update_expr)
diff --git a/src/tests/library/update_expr.cpp b/src/tests/library/update_expr.cpp
new file mode 100644
index 000000000..27bd61a59
--- /dev/null
+++ b/src/tests/library/update_expr.cpp
@@ -0,0 +1,55 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/test.h"
+#include "kernel/abstract.h"
+#include "library/update_expr.h"
+using namespace lean;
+
+static void tst1() {
+    expr a = Const("a");
+    expr b = Const("b");
+    expr eq1 = Eq(a, b);
+    expr eq2 = update_eq(eq1, a, a);
+    expr eq3 = update_eq(eq1, a, b);
+    lean_assert(eq_lhs(eq3) == a);
+    lean_assert(eq_rhs(eq3) == b);
+    lean_assert(is_eqp(eq1, eq3));
+}
+
+static void tst2() {
+    expr a  = Const("a");
+    expr N  = Const("N");
+    expr t1 = Fun(a, N, a);
+    expr b  = Const("b");
+    expr t2 = update_abstraction(t1, N, abst_body(t1));
+    lean_assert(is_eqp(t1, t2));
+    t2 = update_abstraction(t1, N, a);
+    lean_assert(!is_eqp(t1, t2));
+    lean_assert(abst_body(t2) ==  a);
+    t1 = Pi(a, N, a);
+    t2 = update_abstraction(t1, N, abst_body(t1));
+    lean_assert(is_eqp(t1, t2));
+}
+
+void tst3() {
+    expr a   = Const("a");
+    expr b   = Const("b");
+    expr f   = Const("f");
+    expr t1  = Let(a, b, f(a));
+    expr t2  = update_let(t1, expr(), b, let_body(t1));
+    lean_assert(is_eqp(t1, t2));
+    t2  = update_let(t1, expr(), a, let_body(t1));
+    lean_assert(!is_eqp(t1, t2));
+    lean_assert(t2 == Let(a, a, f(a)));
+}
+
+int main() {
+    tst1();
+    tst2();
+    tst3();
+    return has_violations() ? 1 : 0;
+}