diff --git a/wrap/python/spot.py b/wrap/python/spot.py
index b03e2b5b6ad0cf5e8c84f65b7d598f82f26d49f2..2c60bd62cc895f30d77ca9f3dc207ba4c360db30 100644
--- a/wrap/python/spot.py
+++ b/wrap/python/spot.py
@@ -588,7 +588,7 @@ def translate(formula, *args):
 formula.translate = translate
 
 
-def postprocess(automaton, *args):
+def postprocess(automaton, *args, formula=None):
     """Post process an automaton.
 
     This applies a number of simlification algorithms, depending on
@@ -607,12 +607,16 @@ def postprocess(automaton, *args):
       (or 'SBAcc' for short)
 
     The default corresponds to 'generic', 'small' and 'high'.
+
+    If a formula denoted by this automaton is known, pass it to as the
+    optional `formula` argument; it can help some algorithms by
+    providing an easy way to complement the automaton.
     """
     p = postprocessor()
     if type(automaton) == str:
         automaton = globals()['automaton'](automaton)
     _postproc_translate_options(p, postprocessor.Generic, *args)
-    return p.run(automaton)
+    return p.run(automaton, formula)
 
 
 twa.postprocess = postprocess
diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i
index 40b1ea67e34ce1f0802df94313c4203426aac020..13fe3b940fcec349be151b23d2caa6d785a3ae12 100644
--- a/wrap/python/spot_impl.i
+++ b/wrap/python/spot_impl.i
@@ -180,6 +180,24 @@ using namespace spot;
  };
 %apply char** OUTPUT { char** err };
 
+// Allow None to be passed for formula.  Some functions like
+// postprocessor::run() take an optional formula that defaults to
+// nullptr.  So it make sense to have function that take formulas that
+// default to None on the Python side.
+%typemap(in) spot::formula {
+    void *tmp;
+    int res = SWIG_ConvertPtr($input, &tmp, $descriptor(spot::formula*), 0);
+    if (!SWIG_IsOK(res)) {
+      %argument_fail(res, "spot::formula", $symname, $argnum);
+    }
+    if (tmp) {
+      spot::formula* temp = reinterpret_cast< spot::formula * >(tmp);
+      $1 = *temp;
+      if (SWIG_IsNewObj(res)) delete temp;
+    }
+    // if tmp == nullptr, then the default value of $1 is fine.
+}
+
 %typemap(out) spot::formula {
   if (!$1)
     $result = SWIG_Py_Void();