diff --git a/src/limbo/formula.h b/src/limbo/formula.h
index dd758ffda1ab18b0809755da248cd289da82121f..0d6a58daa8684a2fd974bb28ac18ea0cb42cde6f 100644
--- a/src/limbo/formula.h
+++ b/src/limbo/formula.h
@@ -130,8 +130,8 @@ class Formula {
   Ref NF(Symbol::Factory* sf, Term::Factory* tf, bool distribute = true) const {
     Formula::Ref c = Clone();
     c->Rectify(sf, tf);
-    c = c->Normalize(distribute);
     c = c->Flatten(0, sf, tf);
+    c = c->Normalize(distribute);
     return Ref(std::move(c));
   }