diff --git a/include/anthem/StatementVisitor.h b/include/anthem/StatementVisitor.h
index 7563be4..2aa14c4 100644
--- a/include/anthem/StatementVisitor.h
+++ b/include/anthem/StatementVisitor.h
@@ -18,7 +18,7 @@ namespace anthem
 
 struct StatementVisitor
 {
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, Context &context)
 	{
 		// TODO: refactor
 		context.logger.log(output::Priority::Debug, (std::string("[program] ") + program.name).c_str());
@@ -26,10 +26,10 @@ struct StatementVisitor
 		if (!program.parameters.empty())
 			throwErrorAtLocation(statement.location, "program parameters currently unsupported", context);
 
-		return std::experimental::nullopt;
+		return {};
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, Context &context)
 	{
 		context.reset();
 
@@ -44,7 +44,7 @@ struct StatementVisitor
 		if (!consequent)
 		{
 			context.logger.log(output::Priority::Error, "could not translate formula consequent");
-			return std::experimental::nullopt;
+			return {};
 		}
 
 		// Print auxiliary variables replacing the head atom’s arguments
@@ -82,77 +82,77 @@ struct StatementVisitor
 
 		// Use “true” as the consequent in case it is empty
 		if (antecedent.arguments.empty())
-			return ast::Formula::make<ast::Implies>(ast::Boolean(true), std::move(consequent.value()));
+			return {ast::Formula::make<ast::Implies>(ast::Boolean(true), std::move(consequent.value()))};
 		else if (antecedent.arguments.size() == 1)
-			return ast::Formula::make<ast::Implies>(std::move(antecedent.arguments[0]), std::move(consequent.value()));
+			return {ast::Formula::make<ast::Implies>(std::move(antecedent.arguments[0]), std::move(consequent.value()))};
 
-		return ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent.value()));
+		return {ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent.value()))};
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“definition” statements currently unsupported", context);
-		return std::experimental::nullopt;
+		return {};
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::ShowSignature &, const Clingo::AST::Statement &statement, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::ShowSignature &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“show signature” statements currently unsupported", context);
-		return std::experimental::nullopt;
+		return {};
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“show term” statements currently unsupported", context);
-		return std::experimental::nullopt;
+		return {};
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Minimize &, const Clingo::AST::Statement &statement, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::Minimize &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“minimize” statements currently unsupported", context);
-		return std::experimental::nullopt;
+		return {};
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Script &, const Clingo::AST::Statement &statement, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::Script &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“script” statements currently unsupported", context);
-		return std::experimental::nullopt;
+		return {};
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::External &, const Clingo::AST::Statement &statement, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::External &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“external” statements currently unsupported", context);
-		return std::experimental::nullopt;
+		return {};
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Edge &, const Clingo::AST::Statement &statement, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::Edge &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“edge” statements currently unsupported", context);
-		return std::experimental::nullopt;
+		return {};
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Heuristic &, const Clingo::AST::Statement &statement, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::Heuristic &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“heuristic” statements currently unsupported", context);
-		return std::experimental::nullopt;
+		return {};
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::ProjectAtom &, const Clingo::AST::Statement &statement, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::ProjectAtom &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“project atom” statements currently unsupported", context);
-		return std::experimental::nullopt;
+		return {};
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::ProjectSignature &, const Clingo::AST::Statement &statement, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::ProjectSignature &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“project signature” statements currently unsupported", context);
-		return std::experimental::nullopt;
+		return {};
 	}
 
-	std::experimental::optional<ast::Formula> visit(const Clingo::AST::TheoryDefinition &, const Clingo::AST::Statement &statement, Context &context)
+	std::vector<ast::Formula> visit(const Clingo::AST::TheoryDefinition &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“theory definition” statements currently unsupported", context);
-		return std::experimental::nullopt;
+		return {};
 	}
 };
 
diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp
index d71c919..e03b510 100644
--- a/src/anthem/Translation.cpp
+++ b/src/anthem/Translation.cpp
@@ -39,22 +39,31 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 
 	auto fileContent = std::string(std::istreambuf_iterator<char>(stream), {});
 
-	const auto translateStatement =
-		[&context](const Clingo::AST::Statement &statement)
+	bool isFirstStatement = true;
+
+	const auto printFormula =
+		[&context, &isFirstStatement](const ast::Formula &formula)
 		{
-			auto formula = statement.data.accept(StatementVisitor(), statement, context);
+			if (!isFirstStatement)
+				context.logger.outputStream() << std::endl;
 
-			if (!formula)
-				return;
+			context.logger.outputStream() << formula << std::endl;
 
-			if (!context.simplify)
+			isFirstStatement = false;
+		};
+
+	const auto translateStatement =
+		[&context, &printFormula](const Clingo::AST::Statement &statement)
+		{
+			auto formulas = statement.data.accept(StatementVisitor(), statement, context);
+
+			for (auto &formula : formulas)
 			{
-				context.logger.outputStream() << formula.value() << std::endl;
-				return;
-			}
+				if (context.simplify)
+					simplify(formula);
 
-			simplify(formula.value());
-			context.logger.outputStream() << formula.value() << std::endl;
+				printFormula(formula);
+			}
 		};
 
 	const auto logger =