Encode types after encoding Horn clauses.

nick8325 · Sep 3, 2017 · c44f8bd · c44f8bd
1 parent 7b35651
commit c44f8bd
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/executable/Main.hs b/executable/Main.hs
@@ -589,10 +589,14 @@ main = do
       -- hack: get --quiet and --no-proof options to appear before --tstp
     forAllFilesBox <*>
       (readProblemBox =>>=
-       expert (toFof <$> clausifyBox <*> pure (tags True)) =>>=
        expert clausifyBox =>>=
        forAllConjecturesBox <*>
-         (combine <$> pure (hornToUnitIO (HornFlags False)) <*>
+         (combine <$>
+           (pure (hornToUnitIO (HornFlags False)) =>>=
+            toFormulasBox =>>=
+            expert (toFof <$> clausifyBox <*> pure (tags True)) =>>=
+            clausifyBox =>>=
+            oneConjectureBox) <*>
            (runTwee <$> globalFlags <*> tstpFlags <*> parseMainFlags <*> parseConfig <*> parsePrecedence)))
   where
     combine horn prove later prob =