diff --git a/src/tests/util/lazy_list.cpp b/src/tests/util/lazy_list.cpp
index 489c67676..9c133b0cb 100644
--- a/src/tests/util/lazy_list.cpp
+++ b/src/tests/util/lazy_list.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <iostream>
 #include <utility>
+#include "util/interrupt.h"
 #include "util/test.h"
 #include "util/optional.h"
 #include "util/numerics/mpz.h"
@@ -50,6 +51,16 @@ lazy_list<int> mk_simple3() {
     return map_append(from(0, 2, 100), [=](int v) { return from(1, 1, v); });
 }
 
+lazy_list<int> loop() {
+    return lazy_list<int>([=]() {
+            while (true) {
+                check_interrupted();
+            }
+            return some(mk_pair(0, lazy_list<int>()));
+        });
+}
+
+
 template<typename T>
 void display(lazy_list<T> const & l) {
     int buffer[20000];
@@ -84,6 +95,9 @@ static void tst1() {
     display(orelse(lazy_list<int>(), take(10, seq(100))));
     display(orelse(take(0, seq(1)), take(10, seq(100))));
     display(orelse(filter(take(100, seq(1)), [](int i) { return i < 0; }), take(10, seq(1000))));
+#ifndef __APPLE__
+    display(timeout(append(append(take(10, seq(1)), loop()), seq(100)), 5));
+#endif
 }
 
 int main() {
diff --git a/src/util/lazy_list_fn.h b/src/util/lazy_list_fn.h
index 17355067d..166865262 100644
--- a/src/util/lazy_list_fn.h
+++ b/src/util/lazy_list_fn.h
@@ -25,6 +25,9 @@ void for_each(lazy_list<T> l, F && f) {
     }
 }
 
+/**
+   \brief Create a lazy list that contains the first \c sz elements in \c l.
+*/
 template<typename T>
 lazy_list<T> take(unsigned sz, lazy_list<T> const & l) {
     if (sz == 0) {
@@ -40,6 +43,9 @@ lazy_list<T> take(unsigned sz, lazy_list<T> const & l) {
     }
 }
 
+/**
+   \brief Create a lazy list based on the list \c l.
+*/
 template<typename T>
 lazy_list<T> to_lazy(list<T> l) {
     if (l) {
@@ -51,6 +57,9 @@ lazy_list<T> to_lazy(list<T> l) {
     }
 }
 
+/**
+   \brief Appends the given lazy lists.
+*/
 template<typename T>
 lazy_list<T> append(lazy_list<T> const & l1, lazy_list<T> const & l2) {
     return lazy_list<T>([=]() {
@@ -64,6 +73,9 @@ lazy_list<T> append(lazy_list<T> const & l1, lazy_list<T> const & l2) {
         });
 }
 
+/**
+   \brief Return \c l1 if l1 is not empty, and \c l2 otherwise.
+*/
 template<typename T>
 lazy_list<T> orelse(lazy_list<T> const & l1, lazy_list<T> const & l2) {
     return lazy_list<T>([=]() {
@@ -77,6 +89,10 @@ lazy_list<T> orelse(lazy_list<T> const & l1, lazy_list<T> const & l2) {
         });
 }
 
+/**
+   \brief "Fair" version of \c append. That is, the elements of \c l1 and \c l2
+   are interleaved.
+*/
 template<typename T>
 lazy_list<T> interleave(lazy_list<T> const & l1, lazy_list<T> const & l2) {
     return lazy_list<T>([=]() {
@@ -90,6 +106,9 @@ lazy_list<T> interleave(lazy_list<T> const & l1, lazy_list<T> const & l2) {
         });
 }
 
+/**
+   \brief Create a lazy list by applying \c f to the elements of \c l.
+*/
 template<typename T, typename F>
 lazy_list<T> map(lazy_list<T> const & l, F && f) {
     return lazy_list<T>([=]() {
@@ -101,6 +120,13 @@ lazy_list<T> map(lazy_list<T> const & l, F && f) {
         });
 }
 
+/**
+   \brief Create a lazy list that contains only the elements of \c l that satisfies \c pred.
+
+   \remark Lazy lists may be infinite, and none of them may satisfy \c pred.
+
+   \remark \c check_interrupted() is invoked whenever \c pred returns false.
+*/
 template<typename T, typename P>
 lazy_list<T> filter(lazy_list<T> const & l, P && pred) {
     return lazy_list<T>([=]() {
@@ -116,6 +142,9 @@ lazy_list<T> filter(lazy_list<T> const & l, P && pred) {
         });
 }
 
+/**
+   \brief Auxiliary template for \c map_append.
+*/
 template<typename T, typename F>
 lazy_list<T> map_append_aux(lazy_list<T> const & h, lazy_list<T> const & l, F && f) {
     return lazy_list<T>([=]() {
@@ -135,8 +164,63 @@ lazy_list<T> map_append_aux(lazy_list<T> const & h, lazy_list<T> const & l, F &&
         });
 }
 
+/**
+   \brief Applies \c f to each element of \c l. The function \c must return a lazy_list.
+   All lazy_lists are appended together.
+*/
 template<typename T, typename F>
 lazy_list<T> map_append(lazy_list<T> const & l, F && f) {
     return map_append_aux(lazy_list<T>(), l, f);
 }
+
+/**
+   \brief Return a lazy list such that only the elements that can be computed in
+   less than \c ms milliseconds are kept. That is, it uses a timeout for the \c pull
+   method in the class lazy_list. If the \c pull method timeouts, the lazy list
+   is truncated.
+
+   \remark the \c method is executed in a separate execution thread.
+
+   \remark \c check_ms is how often the main thread checks whether the child
+   thread finished.
+*/
+template<typename T>
+lazy_list<T> timeout(lazy_list<T> const & l, unsigned ms, unsigned check_ms = g_small_sleep) {
+    if (check_ms == 0)
+        check_ms = 1;
+    return lazy_list<T>([=]() {
+            typename lazy_list<T>::maybe_pair r;
+            std::atomic<bool> done(false);
+            interruptible_thread th([&]() {
+                    try {
+                        r = l.pull();
+                    } catch (...) {
+                        r = typename lazy_list<T>::maybe_pair();
+                    }
+                    done = true;
+                });
+            try {
+                auto start = std::chrono::steady_clock::now();
+                std::chrono::milliseconds d(ms);
+                std::chrono::milliseconds small(check_ms);
+                while (!done) {
+                    auto curr = std::chrono::steady_clock::now();
+                    if (std::chrono::duration_cast<std::chrono::milliseconds>(curr - start) > d)
+                        break;
+                    check_interrupted();
+                    std::this_thread::sleep_for(small);
+                }
+                th.request_interrupt();
+                th.join();
+                if (r)
+                    return some(mk_pair(r->first, timeout(r->second, ms, check_ms)));
+                else
+                    return r;
+            } catch (...) {
+                th.request_interrupt();
+                th.join();
+                throw;
+            }
+        });
+}
 }