diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp
index 0ccbd3cb1..8df9fe355 100644
--- a/libsmtutil/CHCSmtLib2Interface.cpp
+++ b/libsmtutil/CHCSmtLib2Interface.cpp
@@ -675,10 +675,19 @@ CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromZ3Proof(std::string c
 	if (parser.isEOF()) // No proof from Z3
 		return {};
 	// For some reason Z3 outputs everything as a single s-expression
-	auto all = parser.parseExpression();
+	SMTLib2Expression parsedOutput;
+	try
+	{
+		parsedOutput = parser.parseExpression();
+	}
+	catch (SMTLib2Parser::ParsingException&)
+	{
+		// TODO: What should we do in this case?
+		smtAssert(false, "SMTLIb2Parser: Error parsing input");
+	}
 	solAssert(parser.isEOF());
-	solAssert(!isAtom(all));
-	auto& commands = std::get<SMTLib2Expression::args_t>(all.data);
+	solAssert(!isAtom(parsedOutput));
+	auto& commands = asSubExpressions(parsedOutput);
 	SMTLibTranslationContext context(*m_smtlib2);
 	for (auto& command: commands)
 	{
@@ -720,10 +729,17 @@ smtutil::Expression CHCSmtLib2Interface::invariantsFromSMTLib(std::string const&
 	if (parser.isEOF()) // No model
 		return Expression(true);
 	// For some reason Z3 outputs everything as a single s-expression
-	auto all = parser.parseExpression();
+	SMTLib2Expression parsedOutput;
+	try {
+		parsedOutput = parser.parseExpression();
+	} catch(SMTLib2Parser::ParsingException&)
+	{
+		// TODO: What should we do in this case?
+		smtAssert(false, "SMTLIb2Parser: Error parsing input");
+	}
 	solAssert(parser.isEOF());
-	solAssert(!isAtom(all));
-	auto& commands = std::get<SMTLib2Expression::args_t>(all.data);
+	solAssert(!isAtom(parsedOutput));
+	auto& commands = asSubExpressions(parsedOutput);
 	std::vector<Expression> definitions;
 	for (auto& command: commands)
 	{
diff --git a/libsmtutil/SMTLibParser.cpp b/libsmtutil/SMTLibParser.cpp
index cfc922dc6..3812f2f6a 100644
--- a/libsmtutil/SMTLibParser.cpp
+++ b/libsmtutil/SMTLibParser.cpp
@@ -65,6 +65,8 @@ std::string SMTLib2Parser::parseToken() {
 }
 
 void SMTLib2Parser::advance() {
+	if (!m_input.good())
+		throw ParsingException{};
 	m_token = static_cast<char>(m_input.get());
 	if (token() == ';')
 		while (token() != '\n' && token() != 0)
diff --git a/libsmtutil/SMTLibParser.h b/libsmtutil/SMTLibParser.h
index f34bb66be..fed05d0e8 100644
--- a/libsmtutil/SMTLibParser.h
+++ b/libsmtutil/SMTLibParser.h
@@ -60,6 +60,8 @@ inline auto& asSubExpressions(SMTLib2Expression& expr)
 
 class SMTLib2Parser {
 public:
+	class ParsingException {};
+
 	SMTLib2Parser(std::istream& _input) :
 			m_input(_input),
 			m_token(static_cast<char>(m_input.get())) {}