diff --git a/ChangeLog b/ChangeLog
index 274ec4e0f..fa0fc46e1 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,8 @@
+2011-04-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	* iface/dve2/dve2check.cc (main): Catch out-of-memory errors
+	during emptiness check or counterexample generation.
+
 2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc: Use
diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc
index 555c356a9..f289f032d 100644
--- a/iface/dve2/dve2check.cc
+++ b/iface/dve2/dve2check.cc
@@ -29,9 +29,10 @@
 #include "tgbaalgos/reducerun.hh"
 #include "tgba/tgbaproduct.hh"
 #include "misc/timer.hh"
+#include "misc/memusage.hh"
 #include <cstring>
 
-void
+static void
 syntax(char* prog)
 {
   // Display the supplied name unless it appears to be a libtool wrapper.
@@ -256,7 +257,18 @@ main(int argc, char **argv)
     do
       {
 	tm.start("running emptiness check");
-	spot::emptiness_check_result* res = ec->check();
+	spot::emptiness_check_result* res;
+	try
+	  {
+	    res = ec->check();
+	  }
+	catch (std::bad_alloc)
+	  {
+	    std::cerr << "Out of memory during emptiness check."
+		      << std::endl;
+	    exit_code = 2;
+	    exit(exit_code);
+	  }
 	tm.stop("running emptiness check");
 
 	ec->print_stats(std::cout);
@@ -283,8 +295,19 @@ main(int argc, char **argv)
 	else if (accepting_run)
 	  {
 
+	    spot::tgba_run* run;
 	    tm.start("computing accepting run");
-	    spot::tgba_run* run = res->accepting_run();
+	    try
+	      {
+		run = res->accepting_run();
+	      }
+	    catch (std::bad_alloc)
+	      {
+		std::cerr << "Out of memory while looking for counterexample."
+			  << std::endl;
+		exit_code = 2;
+		exit(exit_code);
+	      }
 	    tm.stop("computing accepting run");
 
 	    if (!run)