From 10529e994f9a587436c57bfdeef52476da9770bb Mon Sep 17 00:00:00 2001
From: Alex Beregszaszi <alex@rtfs.hu>
Date: Wed, 4 Oct 2017 12:18:40 +0100
Subject: SMT should not crash on typecast/structs

---
 libsolidity/formal/SMTChecker.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'libsolidity/formal')

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index fd78e578..7c8c089e 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -234,6 +234,16 @@ void SMTChecker::endVisit(BinaryOperation const& _op)
 
 void SMTChecker::endVisit(FunctionCall const& _funCall)
 {
+	solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, "");
+	if (_funCall.annotation().kind != FunctionCallKind::FunctionCall)
+	{
+		m_errorReporter.warning(
+			_funCall.location(),
+			"Assertion checker does not yet implement this expression."
+		);
+		return;
+	}
+
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 
 	std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
-- 
cgit v1.2.3