diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc
index 64aadec6b..30fef393e 100644
--- a/iface/dve2/dve2check.cc
+++ b/iface/dve2/dve2check.cc
@@ -24,10 +24,9 @@
 #include "ltlast/allnodes.hh"
 #include "ltlparse/public.hh"
 #include "tgbaalgos/ltl2tgba_fm.hh"
-#include "tgbaalgos/sccfilter.hh"
-#include "tgbaalgos/minimize.hh"
 #include "tgbaalgos/emptiness.hh"
 #include "tgbaalgos/reducerun.hh"
+#include "tgbaalgos/postproc.hh"
 #include "tgba/tgbaproduct.hh"
 #include "misc/timer.hh"
 #include "misc/memusage.hh"
@@ -43,36 +42,23 @@ syntax(char* prog)
   if (slash && (strncmp(slash + 1, "lt-", 3) == 0))
     prog = slash + 4;
 
-  std::cerr << "usage: " << prog << " [options] model formula" << std::endl
-	    << std::endl
-	    << "Options:" << std::endl
-	    << "  -dDEAD use DEAD as property for marking DEAD states"
-	    << std::endl
-	    << "          (by default DEAD = true)" << std::endl
-	    << "  -e[ALGO]  run emptiness check, expect an accepting run"
-	    << std::endl
-	    << "  -E[ALGO]  run emptiness check, expect no accepting run"
-	    << std::endl
-	    << "  -C     compute an accepting run (Counterexample) if it exists"
-	    << std::endl
-	    << "  -gf    output the automaton of the formula in dot format"
-	    << std::endl
-	    << "  -gm    output the model state-space in dot format"
-	    << std::endl
-            << "  -gK    output the model state-space in Kripke format"
-            << std::endl
-	    << "  -gp    output the product state-space in dot format"
-	    << std::endl
-            << "  -T     time the different phases of the execution"
-	    << std::endl
-            << "  -W     enable WDBA minimization"
-	    << std::endl
-            << "  -z     compress states to handle larger models"
-	    << std::endl
-            << "  -Z     compress states (faster) "
-	    << "assuming all values in [0 .. 2^28-1]"
-	    << std::endl;
-
+  std::cerr << "usage: " << prog << " [options] model formula\n\
+\n\
+Options:\n\
+  -dDEAD use DEAD as property for marking DEAD states\n\
+          (by default DEAD = true)\n\
+  -e[ALGO]  run emptiness check, expect an accepting run\n\
+  -E[ALGO]  run emptiness check, expect no accepting run\n\
+  -C     compute an accepting run (Counterexample) if it exists\n\
+  -D     favor a deterministic translation over a small transition\n\
+  -gf    output the automaton of the formula in dot format\n\
+  -gm    output the model state-space in dot format\n\
+  -gK    output the model state-space in Kripke format\n\
+  -gp    output the product state-space in dot format\n\
+  -T     time the different phases of the execution\n\
+  -z     compress states to handle larger models\n\
+  -Z     compress states (faster) assuming all values in [0 .. 2^28-1]\n\
+";
   exit(1);
 }
 
@@ -87,7 +73,7 @@ main(int argc, char **argv)
   output = EmptinessCheck;
   bool accepting_run = false;
   bool expect_counter_example = false;
-  bool wdba = false;
+  bool deterministic = false;
   char *dead = 0;
   int compress_states = 0;
 
@@ -108,6 +94,9 @@ main(int argc, char **argv)
 	    case 'd':
 	      dead = opt + 1;
 	      break;
+	    case 'D':
+	      deterministic = true;
+	      break;
 	    case 'e':
 	    case 'E':
 	      {
@@ -141,9 +130,6 @@ main(int argc, char **argv)
 	    case 'T':
 	      use_timer = true;
 	      break;
-	    case 'W':
-	      wdba = true;
-	      break;
 	    case 'z':
 	      compress_states = 1;
 	      break;
@@ -179,6 +165,7 @@ main(int argc, char **argv)
   int exit_code = 0;
   const spot::ltl::formula* f = 0;
   const spot::ltl::formula* deadf = 0;
+  spot::postprocessor post;
 
   if (dead == 0 || !strcasecmp(dead, "true"))
     {
@@ -230,7 +217,6 @@ main(int argc, char **argv)
 
   atomic_prop_collect(f, &ap);
 
-
   if (output != DotFormula)
     {
       tm.start("loading dve2");
@@ -264,29 +250,12 @@ main(int argc, char **argv)
   prop = spot::ltl_to_tgba_fm(f, dict);
   tm.stop("translating formula");
 
-  tm.start("reducing A_f w/ SCC");
-  {
-    spot::tgba* aut_scc = spot::scc_filter(prop, true);
-    delete prop;
-    prop = aut_scc;
-  }
-  tm.stop("reducing A_f w/ SCC");
+  if (deterministic)
+    post.set_pref(spot::postprocessor::Deterministic);
 
-  if (wdba)
-    {
-      tm.start("WDBA minimization");
-      const spot::tgba* minimized = 0;
-
-      minimized = minimize_obligation(prop, f);
-
-      if (minimized != prop)
-	{
-	  delete prop;
-	  prop = minimized;
-	}
-
-      tm.stop("WDBA minimization");
-    }
+  tm.start("postprocessing A_f");
+  prop = post.run(prop, f);
+  tm.stop("postprocessing A_f");
 
   if (output == DotFormula)
     {
@@ -306,7 +275,6 @@ main(int argc, char **argv)
       goto safe_exit;
     }
 
-
   assert(echeck_inst);
 
   {
diff --git a/iface/dve2/dve2check.test b/iface/dve2/dve2check.test
index 5b7744d5d..6cda6ff32 100755
--- a/iface/dve2/dve2check.test
+++ b/iface/dve2/dve2check.test
@@ -39,13 +39,15 @@ for opt in '' '-z'; do
   # time with valgrind.).
 
   ../dve2check $opt -E $srcdir/beem-peterson.4.dve \
-    '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
-  run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \
-    '!G(P_0.wait -> F P_0.CS)' | grep -v pages > stdout1
+    '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' \
+    | grep -v pages > stdout1
   # same formula, different syntax.
-  run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \
-	    '!G("P_0 == wait" -> F "P_0 == CS")' | grep -v pages > stdout2
+  ../dve2check $opt -E $srcdir/beem-peterson.4.dve \
+    '!GF("P_0==CS"|"P_1 == CS"|"P_2 ==CS"|"P_3==  CS")' \
+    | grep -v pages > stdout2
   cmp stdout1 stdout2
+  run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \
+    '!G(P_0.wait -> F P_0.CS)'
   run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")'
 done