diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp
index b466e1de3d..e454027097 100644
--- a/src/bindings/lua/leanlua_state.cpp
+++ b/src/bindings/lua/leanlua_state.cpp
@@ -63,13 +63,12 @@ static char const * reader(lua_State *, void * data, size_t * sz) {
 
 static void copy_values(lua_State * src, int first, int last, lua_State * tgt) {
     for (int i = first; i <= last; i++) {
-        if (lua_isstring(src, i)) {
-            lua_pushstring(tgt, lua_tostring(src, i));
-        } else if (lua_isnumber(src, i)) {
-            lua_pushnumber(tgt, lua_tonumber(src, i));
-        } else if (lua_isboolean(src, i)) {
-            lua_pushboolean(tgt, lua_toboolean(src, i));
-        } else if (lua_isfunction(src, i)) {
+        switch (lua_type(src, i)) {
+        case LUA_TNUMBER:   lua_pushnumber(tgt, lua_tonumber(src, i)); break;
+        case LUA_TSTRING:   lua_pushstring(tgt, lua_tostring(src, i)); break;
+        case LUA_TNIL:      lua_pushnil(tgt); break;
+        case LUA_TBOOLEAN:  lua_pushboolean(tgt, lua_toboolean(src, i)); break;
+        case LUA_TFUNCTION: {
             lua_pushvalue(src, i); // copy function to the top of the stack
             buffer<char> buffer;
             if (lua_dump(src, writer, &buffer) != 0)
@@ -89,31 +88,38 @@ static void copy_values(lua_State * src, int first, int last, lua_State * tgt) {
                 lua_setupvalue(tgt, -2, j);
                 j++;
             }
-        } else if (is_expr(src, i)) {
-            push_expr(tgt, to_expr(src, i));
-        } else if (is_context(src, i)) {
-            push_context(tgt, to_context(src, i));
-        } else if (is_environment(src, i)) {
-            push_environment(tgt, to_environment(src, i));
-        } else if (is_name(src, i)) {
-            push_name(tgt, to_name(src, i));
-        } else if (is_mpz(src, i)) {
-            push_mpz(tgt, to_mpz(src, i));
-        } else if (is_mpq(src, i)) {
-            push_mpq(tgt, to_mpq(src, i));
-        } else if (is_options(src, i)) {
-            push_options(tgt, to_options(src, i));
-        } else if (is_sexpr(src, i)) {
-            push_sexpr(tgt, to_sexpr(src, i));
-        } else if (is_format(src, i)) {
-            push_format(tgt, to_format(src, i));
-        } else if (is_context_entry(src, i)) {
-            push_context_entry(tgt, to_context_entry(src, i));
-        } else if (is_local_context(src, i)) {
-            push_local_context(tgt, to_local_context(src, i));
-        } else if (is_local_entry(src, i)) {
-            push_local_entry(tgt, to_local_entry(src, i));
-        } else {
+            break;
+        }
+        case LUA_TUSERDATA:
+            if (is_expr(src, i)) {
+                push_expr(tgt, to_expr(src, i));
+            } else if (is_context(src, i)) {
+                push_context(tgt, to_context(src, i));
+            } else if (is_environment(src, i)) {
+                push_environment(tgt, to_environment(src, i));
+            } else if (is_name(src, i)) {
+                push_name(tgt, to_name(src, i));
+            } else if (is_mpz(src, i)) {
+                push_mpz(tgt, to_mpz(src, i));
+            } else if (is_mpq(src, i)) {
+                push_mpq(tgt, to_mpq(src, i));
+            } else if (is_options(src, i)) {
+                push_options(tgt, to_options(src, i));
+            } else if (is_sexpr(src, i)) {
+                push_sexpr(tgt, to_sexpr(src, i));
+            } else if (is_format(src, i)) {
+                push_format(tgt, to_format(src, i));
+            } else if (is_context_entry(src, i)) {
+                push_context_entry(tgt, to_context_entry(src, i));
+            } else if (is_local_context(src, i)) {
+                push_local_context(tgt, to_local_context(src, i));
+            } else if (is_local_entry(src, i)) {
+                push_local_entry(tgt, to_local_entry(src, i));
+            } else {
+                throw exception("unsupported value type for inter-State call");
+            }
+            break;
+        default:
             throw exception("unsupported value type for inter-State call");
         }
     }
diff --git a/tests/lua/th1.lua b/tests/lua/th1.lua
new file mode 100644
index 0000000000..e87ae41fd5
--- /dev/null
+++ b/tests/lua/th1.lua
@@ -0,0 +1,36 @@
+S = State()
+assert(is_State(S))
+S:eval([[ local x = ...; assert(x == 10) ]], 10)
+S:eval([[ local f = ...; assert(f) ]], true)
+S:eval([[ local f = ...; assert(not f) ]], false)
+S:eval([[ local s = ...; assert(s == "foo") ]], "foo")
+S:eval([[ local f = ...; assert(f(1) == 3) ]], function (x) return x + 2 end)
+local val = 10
+S:eval([[ local f = ...; assert(f(1) == 11) ]], function (x) return x + val end)
+S:eval([[ local o = ...; assert(o == name("a")) ]], name("a"))
+S:eval([[ local o = ...; assert(o == Const("a")) ]], Const("a"))
+S:eval([[ local o = ...; assert(is_context(o)) ]], context())
+S:eval([[ local o = ...; assert(is_environment(o)) ]], environment())
+S:eval([[ local o = ...; assert(o == mpz(100)) ]], mpz(100))
+S:eval([[ local o = ...; assert(o == mpq(100)/3) ]], mpq(100)/3)
+S:eval([[ local o = ...; assert(is_options(o)) ]], options())
+S:eval([[ local o = ...; assert(is_sexpr(o)) ]], sexpr())
+S:eval([[ local o = ...; assert(o:is_cons()) ]], sexpr(1, 2))
+S:eval([[ local o = ...; assert(is_format(o)) ]], format("1"))
+S:eval([[ local o = ...; assert(is_context_entry(o)) ]], context_entry("a", Const("T")))
+S:eval([[ local o = ...; assert(is_local_entry(o)) ]], mk_lift(1, 2))
+S:eval([[ local o = ...; assert(is_local_context(o)) ]], local_context())
+S:eval([[ local o1, o2, o3 = ...; assert(is_sexpr(o1)); assert(is_name(o2)); assert(o3 == 10) ]], sexpr(), name("foo"), 10)
+assert(not pcall(function() S:eval([[ x = ]]) end))
+local T = thread(S, [[ local x = ...; return x + 10, x - 10 ]], 10)
+assert(is_thread(T))
+local r1, r2 = T:wait()
+assert(r1 == 20)
+assert(r2 == 0)
+assert(not pcall(function() S:eval([[ x = ]]) end))
+local T2 = thread(S, [[ local x = ...; error("failed") ]], 10)
+local ok, msg = pcall(function() T2:wait() end)
+assert(not ok)
+assert(string.sub(msg, -7) == "failed\n")
+local T3 = thread(S, [[ local x = ...; return x + 10, x - 10 ]], 10)
+T3 = nil