From ea93832797ad548416a87c287b65e6f470f883e6 Mon Sep 17 00:00:00 2001
From: Christoph Schwering <c.schwering@unsw.edu.au>
Date: Mon, 31 Jul 2017 06:51:53 +1000
Subject: [PATCH] Formula::NF() now flattens before normalizing.

Formula::Flatten() may introduce new universally quantified variables.
Formula::Normalize() pull universally quantified variables out of K
modalities.
So it makes sense to flatten first.
---
 src/limbo/formula.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/limbo/formula.h b/src/limbo/formula.h
index dd758ff..0d6a58d 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));
   }
 
-- 
GitLab