diff --git a/src/util/lazy.h b/src/util/lazy.h
index dc1d35db937..46458200e40 100644
--- a/src/util/lazy.h
+++ b/src/util/lazy.h
@@ -43,4 +43,12 @@ class lazyt
   }
 };
 
+/// Delay the computation of \p fun to the next time the \c force method
+/// is called.
+template <typename funt>
+auto lazy(funt fun) -> lazyt<decltype(fun())>
+{
+  return lazyt<decltype(fun())>::from_fun(std::move(fun));
+}
+
 #endif // CPROVER_UTIL_LAZY_H
diff --git a/unit/util/lazy.cpp b/unit/util/lazy.cpp
index 757a02aedd2..04b6acdf7e6 100644
--- a/unit/util/lazy.cpp
+++ b/unit/util/lazy.cpp
@@ -9,7 +9,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include <testing-utils/use_catch.h>
 #include <util/lazy.h>
 
-SCENARIO("lazy test", "[core][util][lazy]")
+SCENARIO("lazyt::from_fun test", "[core][util][lazy]")
 {
   std::size_t call_counter = 0;
   auto length_with_counter = [&call_counter](const std::string &s) {
@@ -27,3 +27,22 @@ SCENARIO("lazy test", "[core][util][lazy]")
   REQUIRE(call_counter == 1);
   REQUIRE(result == 3);
 }
+
+SCENARIO("lazy test", "[core][util][lazy]")
+{
+  std::size_t call_counter = 0;
+  auto length_with_counter = [&call_counter](const std::string &s) {
+    ++call_counter;
+    return s.length();
+  };
+  lazyt<std::size_t> lazy_length =
+    lazy([&] { return length_with_counter("foobar"); });
+
+  REQUIRE(call_counter == 0);
+  auto result = lazy_length.force();
+  REQUIRE(call_counter == 1);
+  REQUIRE(result == 6);
+  result = lazy_length.force();
+  REQUIRE(call_counter == 1);
+  REQUIRE(result == 6);
+}