diff --git a/divine/mc/bitcode.cpp b/divine/mc/bitcode.cpp
index 19f89a4f66bb2653d4505a240758dcb1d7f65aee..ba755f798c7e3ef92b221b2a531616ea04b450ec 100644
--- a/divine/mc/bitcode.cpp
+++ b/divine/mc/bitcode.cpp
@@ -22,6 +22,7 @@
 #include <divine/vm/program.hpp>
 #include <lart/driver.h>
 #include <lart/mcsema/libcindirectcalls.hpp>
+#include <lart/mcsema/lowerreturn.hpp>
 #include <lart/mcsema/segmentmasks.hpp>
 #include <lart/support/util.h>
 
@@ -158,6 +159,7 @@ void BitCode::do_lart()
     // TODO: Unify with lart::Driver once it is rewritten
     if ( _opts.mcsema )
     {
+        lart::mcsema::lower_ret_agg( *_module.get() ).run();
         lart::mcsema::segment_masks().run( *_module.get() );
         lart::mcsema::libc_indirect_calls().run( *_module.get() );
     }