Merge pull request #6679 from ethereum/smt_fix_ssa_reset

[SMTChecker] Fix ICE in touched vars

Changelog.md

@@ -16,6 +16,7 @@ Bugfixes:
  * SMTChecker: Fix internal error when visiting state variable inherited from base class.
  * SMTChecker: Fix internal error in fixed point operations.
  * SMTChecker: Fix internal error in assignment to unsupported type.
+ * SMTChecker: Fix internal error in branching when inlining function calls that modify local variables.
 
 
 

libsolidity/ast/AST.cpp

@@ -400,6 +400,21 @@ SourceUnit const& Scopable::sourceUnit() const
 	return dynamic_cast<SourceUnit const&>(*s);
 }
 
+CallableDeclaration const* Scopable::functionOrModifierDefinition() const
+{
+	ASTNode const* s = scope();
+	solAssert(s, "");
+	while (dynamic_cast<Scopable const*>(s))
+	{
+		if (auto funDef = dynamic_cast<FunctionDefinition const*>(s))
+			return funDef;
+		if (auto modDef = dynamic_cast<ModifierDefinition const*>(s))
+			return modDef;
+		s = dynamic_cast<Scopable const*>(s)->scope();
+	}
+	return nullptr;
+}
+
 string Scopable::sourceUnitName() const
 {
 	return sourceUnit().annotation().path;

libsolidity/ast/AST.h

@@ -161,6 +161,9 @@ public:
 	/// @returns the source unit this scopable is present in.
 	SourceUnit const& sourceUnit() const;
 
+	/// @returns the function or modifier definition this scopable is present in or nullptr.
+	CallableDeclaration const* functionOrModifierDefinition() const;
+
 	/// @returns the source name this scopable is present in.
 	/// Can be combined with annotation().canonicalName (if present) to form a globally unique name.
 	std::string sourceUnitName() const;

libsolidity/ast/ASTForward.h

@@ -38,6 +38,7 @@ class SourceUnit;
 class PragmaDirective;
 class ImportDirective;
 class Declaration;
+class CallableDeclaration;
 class ContractDefinition;
 class InheritanceSpecifier;
 class UsingForDirective;

libsolidity/formal/SMTChecker.cpp

@@ -103,25 +103,14 @@ bool SMTChecker::visit(ModifierDefinition const&)
 
 bool SMTChecker::visit(FunctionDefinition const& _function)
 {
-	m_functionPath.push_back(&_function);
-	m_modifierDepthStack.push_back(-1);
-
-	if (_function.isConstructor())
-	{
-		m_errorReporter.warning(
-			_function.location(),
-			"Assertion checker does not yet support constructors."
-		);
-		return false;
-	}
-
 	// Not visited by a function call
-	if (isRootFunction())
+	if (m_callStack.empty())
 	{
 		m_interface->reset();
 		m_context.reset();
 		m_pathConditions.clear();
 		m_callStack.clear();
+		pushCallStack({&_function, nullptr});
 		m_expressions.clear();
 		m_globalContext.clear();
 		m_uninterpretedTerms.clear();
@@ -132,20 +121,31 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 		m_arrayAssignmentHappened = false;
 		m_externalFunctionCallHappened = false;
 	}
-	_function.parameterList().accept(*this);
+	m_modifierDepthStack.push_back(-1);
-	if (_function.returnParameterList())
+	if (_function.isConstructor())
-		_function.returnParameterList()->accept(*this);
+	{
-	visitFunctionOrModifier();
+		m_errorReporter.warning(
+			_function.location(),
+			"Assertion checker does not yet support constructors."
+		);
+	}
+	else
+	{
+		_function.parameterList().accept(*this);
+		if (_function.returnParameterList())
+			_function.returnParameterList()->accept(*this);
+		visitFunctionOrModifier();
+	}
 	return false;
 }
 
 void SMTChecker::visitFunctionOrModifier()
 {
-	solAssert(!m_functionPath.empty(), "");
+	solAssert(!m_callStack.empty(), "");
 	solAssert(!m_modifierDepthStack.empty(), "");
 
 	++m_modifierDepthStack.back();
-	FunctionDefinition const& function = *m_functionPath.back();
+	FunctionDefinition const& function = dynamic_cast<FunctionDefinition const&>(*m_callStack.back().first);
 
 	if (m_modifierDepthStack.back() == int(function.modifiers().size()))
 	{
@@ -166,7 +166,7 @@ void SMTChecker::visitFunctionOrModifier()
 			for (auto arg: *modifierInvocation->arguments())
 				modifierArgsExpr.push_back(expr(*arg));
 		initializeFunctionCallParameters(modifierDef, modifierArgsExpr);
-		pushCallStack(modifierInvocation.get());
+		pushCallStack({&modifierDef, modifierInvocation.get()});
 		modifierDef.body().accept(*this);
 		popCallStack();
 	}
@@ -176,8 +176,8 @@ void SMTChecker::visitFunctionOrModifier()
 
 bool SMTChecker::visit(PlaceholderStatement const&)
 {
-	solAssert(!m_functionPath.empty(), "");
+	solAssert(!m_callStack.empty(), "");
-	ASTNode const* lastCall = popCallStack();
+	auto lastCall = popCallStack();
 	visitFunctionOrModifier();
 	pushCallStack(lastCall);
 	return true;
@@ -185,20 +185,20 @@ bool SMTChecker::visit(PlaceholderStatement const&)
 
 void SMTChecker::endVisit(FunctionDefinition const&)
 {
+	m_callStack.pop_back();
+	solAssert(m_modifierDepthStack.back() == -1, "");
+	m_modifierDepthStack.pop_back();
 	// If _function was visited from a function call we don't remove
 	// the local variables just yet, since we might need them for
 	// future calls.
 	// Otherwise we remove any local variables from the context and
 	// keep the state variables.
-	if (isRootFunction())
+	if (m_callStack.empty())
 	{
 		checkUnderOverflow();
 		removeLocalVariables();
 		solAssert(m_callStack.empty(), "");
 	}
-	m_functionPath.pop_back();
-	solAssert(m_modifierDepthStack.back() == -1, "");
-	m_modifierDepthStack.pop_back();
 }
 
 bool SMTChecker::visit(InlineAssembly const& _inlineAsm)
@@ -391,7 +391,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 		vector<smt::Expression> rightArguments;
 		if (_assignment.rightHandSide().annotation().type->category() == Type::Category::Tuple)
 		{
-			auto const& symbTuple = dynamic_pointer_cast<SymbolicTupleVariable>(m_expressions[&_assignment.rightHandSide()]);
+			auto symbTuple = dynamic_pointer_cast<SymbolicTupleVariable>(m_expressions[&_assignment.rightHandSide()]);
 			solAssert(symbTuple, "");
 			for (auto const& component: symbTuple->components())
 			{
@@ -666,9 +666,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 		visitGasLeft(_funCall);
 		break;
 	case FunctionType::Kind::Internal:
-		pushCallStack(&_funCall);
 		inlineFunctionCall(_funCall);
-		popCallStack();
 		break;
 	case FunctionType::Kind::External:
 	case FunctionType::Kind::DelegateCall:
@@ -756,10 +754,8 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 			_funCall.location(),
 			"Assertion checker does not yet implement this type of function call."
 		);
-		return;
 	}
-
+	else if (visitedFunction(funDef))
-	if (visitedFunction(funDef))
 		m_errorReporter.warning(
 			_funCall.location(),
 			"Assertion checker does not support recursive function calls.",
@@ -783,7 +779,12 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 			funArgs.push_back(expr(*arg));
 		initializeFunctionCallParameters(*funDef, funArgs);
 
+		// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
+		// is that there we don't have `_funCall`.
+		pushCallStack({funDef, &_funCall});
 		funDef->accept(*this);
+		// The callstack entry is popped only in endVisit(FunctionDefinition) instead of here
+		// as well to avoid code duplication (not all entries are from inlined function calls).
 
 		createExpr(_funCall);
 		auto const& returnParams = funDef->returnParameters();
@@ -920,7 +921,7 @@ void SMTChecker::endVisit(Return const& _return)
 {
 	if (_return.expression() && knownExpr(*_return.expression()))
 	{
-		auto returnParams = m_functionPath.back()->returnParameters();
+		auto returnParams = m_callStack.back().first->returnParameters();
 		if (returnParams.size() > 1)
 		{
 			auto tuple = dynamic_cast<TupleExpression const*>(_return.expression());
@@ -1423,7 +1424,7 @@ void SMTChecker::checkCondition(
 
 	vector<smt::Expression> expressionsToEvaluate;
 	vector<string> expressionNames;
-	if (m_functionPath.size())
+	if (m_callStack.size())
 	{
 		solAssert(m_scanner, "");
 		if (_additionalValue)
@@ -1491,7 +1492,7 @@ void SMTChecker::checkCondition(
 	{
 		std::ostringstream message;
 		message << _description << " happens here";
-		if (m_functionPath.size())
+		if (m_callStack.size())
 		{
 			std::ostringstream modelMessage;
 			modelMessage << "  for:\n";
@@ -1864,25 +1865,27 @@ smt::Expression SMTChecker::currentPathConditions()
 SecondarySourceLocation SMTChecker::currentCallStack()
 {
 	SecondarySourceLocation callStackLocation;
-	if (m_callStack.empty())
+	solAssert(!m_callStack.empty(), "");
-		return callStackLocation;
 	callStackLocation.append("Callstack: ", SourceLocation());
 	for (auto const& call: m_callStack | boost::adaptors::reversed)
-		callStackLocation.append("", call->location());
+		if (call.second)
+			callStackLocation.append("", call.second->location());
+	// The first function in the tx has no FunctionCall.
+	solAssert(m_callStack.front().second == nullptr, "");
 	return callStackLocation;
 }
 
-ASTNode const* SMTChecker::popCallStack()
+pair<CallableDeclaration const*, ASTNode const*> SMTChecker::popCallStack()
 {
 	solAssert(!m_callStack.empty(), "");
-	ASTNode const* lastCalled = m_callStack.back();
+	auto lastCalled = m_callStack.back();
 	m_callStack.pop_back();
 	return lastCalled;
 }
 
-void SMTChecker::pushCallStack(ASTNode const* _node)
+void SMTChecker::pushCallStack(CallStackEntry _entry)
 {
-	m_callStack.push_back(_node);
+	m_callStack.push_back(_entry);
 }
 
 void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e)
@@ -1897,12 +1900,15 @@ void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
 
 bool SMTChecker::isRootFunction()
 {
-	return m_functionPath.size() == 1;
+	return m_callStack.size() == 1;
 }
 
 bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef)
 {
-	return contains(m_functionPath, _funDef);
+	for (auto const& call: m_callStack)
+		if (call.first == _funDef)
+			return true;
+	return false;
 }
 
 SMTChecker::VariableIndices SMTChecker::copyVariableIndices()
@@ -1950,8 +1956,11 @@ FunctionDefinition const* SMTChecker::inlinedFunctionCallToDefinition(FunctionCa
 
 set<VariableDeclaration const*> SMTChecker::touchedVariables(ASTNode const& _node)
 {
-	solAssert(!m_functionPath.empty(), "");
+	solAssert(!m_callStack.empty(), "");
-	return m_variableUsage.touchedVariables(_node, m_functionPath);
+	vector<CallableDeclaration const*> callStack;
+	for (auto const& call: m_callStack)
+		callStack.push_back(call.first);
+	return m_variableUsage.touchedVariables(_node, callStack);
 }
 
 VariableDeclaration const* SMTChecker::identifierToVariable(Expression const& _expr)

libsolidity/formal/SMTChecker.h

@@ -173,6 +173,8 @@ private:
 		std::string const& _description
 	);
 
+	using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
+
 	struct OverflowTarget
 	{
 		enum class Type { Underflow, Overflow, All } type;
@@ -180,9 +182,9 @@ private:
 		smt::Expression value;
 		smt::Expression path;
 		langutil::SourceLocation const& location;
-		std::vector<ASTNode const*> callStack;
+		std::vector<CallStackEntry> callStack;
 
-		OverflowTarget(Type _type, TypePointer _intType, smt::Expression _value, smt::Expression _path, langutil::SourceLocation const& _location, std::vector<ASTNode const*> _callStack):
+		OverflowTarget(Type _type, TypePointer _intType, smt::Expression _value, smt::Expression _path, langutil::SourceLocation const& _location, std::vector<CallStackEntry> _callStack):
 			type(_type),
 			intType(_intType),
 			value(_value),
@@ -266,9 +268,9 @@ private:
 	/// Returns the current callstack. Used for models.
 	langutil::SecondarySourceLocation currentCallStack();
 	/// Copies and pops the last called node.
-	ASTNode const* popCallStack();
+	CallStackEntry popCallStack();
-	/// Adds @param _node to the callstack.
+	/// Adds (_definition, _node) to the callstack.
-	void pushCallStack(ASTNode const* _node);
+	void pushCallStack(CallStackEntry _entry);
 	/// Conjoin the current path conditions with the given parameter and add to the solver
 	void addPathConjoinedExpression(smt::Expression const& _e);
 	/// Add to the solver: the given expression implied by the current path conditions
@@ -315,10 +317,8 @@ private:
 	langutil::ErrorList m_smtErrors;
 	std::shared_ptr<langutil::Scanner> m_scanner;
 
-	/// Stores the current path of function calls.
+	/// Stores the current function/modifier call/invocation path.
-	std::vector<FunctionDefinition const*> m_functionPath;
+	std::vector<CallStackEntry> m_callStack;
-	/// Stores the current call/invocation path.
-	std::vector<ASTNode const*> m_callStack;
 	/// Returns true if the current function was not visited by
 	/// a function call.
 	bool isRootFunction();

libsolidity/formal/VariableUsage.cpp

@@ -31,26 +31,30 @@ void VariableUsage::endVisit(Identifier const& _identifier)
 	solAssert(declaration, "");
 	if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
 		if (_identifier.annotation().lValueRequested)
-			m_touchedVariables.insert(varDecl);
+		{
+			solAssert(m_lastCall, "");
+			if (!varDecl->isLocalVariable() || varDecl->functionOrModifierDefinition() == m_lastCall)
+				m_touchedVariables.insert(varDecl);
+		}
 }
 
 void VariableUsage::endVisit(FunctionCall const& _funCall)
 {
 	if (auto const& funDef = SMTChecker::inlinedFunctionCallToDefinition(_funCall))
-		if (find(m_functionPath.begin(), m_functionPath.end(), funDef) == m_functionPath.end())
+		if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end())
 			funDef->accept(*this);
 }
 
 bool VariableUsage::visit(FunctionDefinition const& _function)
 {
-	m_functionPath.push_back(&_function);
+	m_callStack.push_back(&_function);
 	return true;
 }
 
 void VariableUsage::endVisit(FunctionDefinition const&)
 {
-	solAssert(!m_functionPath.empty(), "");
+	solAssert(!m_callStack.empty(), "");
-	m_functionPath.pop_back();
+	m_callStack.pop_back();
 }
 
 void VariableUsage::endVisit(ModifierInvocation const& _modifierInv)
@@ -62,18 +66,21 @@ void VariableUsage::endVisit(ModifierInvocation const& _modifierInv)
 
 void VariableUsage::endVisit(PlaceholderStatement const&)
 {
-	solAssert(!m_functionPath.empty(), "");
+	solAssert(!m_callStack.empty(), "");
-	FunctionDefinition const* function = m_functionPath.back();
+	FunctionDefinition const* funDef = nullptr;
-	solAssert(function, "");
+	for (auto it = m_callStack.rbegin(); it != m_callStack.rend() && !funDef; ++it)
-	if (function->isImplemented())
+		funDef = dynamic_cast<FunctionDefinition const*>(*it);
-		function->body().accept(*this);
+	solAssert(funDef, "");
+	if (funDef->isImplemented())
+		funDef->body().accept(*this);
 }
 
-set<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node, vector<FunctionDefinition const*> const& _outerCallstack)
+set<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node, vector<CallableDeclaration const*> const& _outerCallstack)
 {
 	m_touchedVariables.clear();
-	m_functionPath.clear();
+	m_callStack.clear();
-	m_functionPath += _outerCallstack;
+	m_callStack += _outerCallstack;
+	m_lastCall = m_callStack.back();
 	_node.accept(*this);
 	return m_touchedVariables;
 }

libsolidity/formal/VariableUsage.h

@@ -34,7 +34,7 @@ class VariableUsage: private ASTConstVisitor
 {
 public:
 	/// @param _outerCallstack the current callstack in the callers context.
-	std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node, std::vector<FunctionDefinition const*> const& _outerCallstack);
+	std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node, std::vector<CallableDeclaration const*> const& _outerCallstack);
 
 private:
 	void endVisit(Identifier const& _node) override;
@@ -45,7 +45,8 @@ private:
 	void endVisit(PlaceholderStatement const& _node) override;
 
 	std::set<VariableDeclaration const*> m_touchedVariables;
-	std::vector<FunctionDefinition const*> m_functionPath;
+	std::vector<CallableDeclaration const*> m_callStack;
+	CallableDeclaration const* m_lastCall = nullptr;
 };
 
 }

test/libsolidity/smtCheckerTests/complex/slither/external_function.sol

@@ -0,0 +1,96 @@
+pragma experimental SMTChecker;
+
+contract ContractWithFunctionCalled {
+    function funcCalled() external  {
+        uint256 i = 0;
+    }
+}
+
+contract ContractWithFunctionCalledSuper is ContractWithFunctionCalled {
+    function callWithSuper() public {
+        uint256 i = 0;
+    }
+}
+
+contract ContractWithFunctionNotCalled {
+
+    function funcNotCalled3() public {
+
+    }
+
+    function funcNotCalled2() public {
+
+    }
+
+    function funcNotCalled() public {
+
+    }
+
+    function my_func() internal returns(bool){
+        return true;
+    }
+
+}
+
+contract ContractWithFunctionNotCalled2 is ContractWithFunctionCalledSuper {
+    function funcNotCalled() public {
+        uint256 i = 0;
+        address three = address(new ContractWithFunctionNotCalled());
+        three.call(abi.encode(bytes4(keccak256("helloTwo()"))));
+        super.callWithSuper();
+        ContractWithFunctionCalled c = new ContractWithFunctionCalled();
+        c.funcCalled();
+    }
+}
+
+contract InternalCall {
+
+    function() returns(uint) ptr;
+
+    function set_test1() external{
+        ptr = test1;
+    }
+
+    function set_test2() external{
+        ptr = test2;
+    }
+
+    function test1() public returns(uint){
+        return 1;
+    }
+
+    function test2() public returns(uint){
+        return 2;
+    }
+
+    function test3() public returns(uint){
+        return 3;
+    }
+
+    function exec() external returns(uint){
+        return ptr();
+    }
+
+}
+// ----
+// Warning: (760-815): Return value of low-level calls not used.
+// Warning: (117-126): Unused local variable.
+// Warning: (260-269): Unused local variable.
+// Warning: (667-676): Unused local variable.
+// Warning: (75-137): Function state mutability can be restricted to pure
+// Warning: (218-280): Function state mutability can be restricted to pure
+// Warning: (470-539): Function state mutability can be restricted to pure
+// Warning: (1144-1206): Function state mutability can be restricted to pure
+// Warning: (1212-1274): Function state mutability can be restricted to pure
+// Warning: (1280-1342): Function state mutability can be restricted to pure
+// Warning: (714-749): Internal error: Expression undefined for SMT solver.
+// Warning: (799-811): Assertion checker does not yet support the type of this literal (literal_string "helloTwo()").
+// Warning: (782-813): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (771-814): Assertion checker does not yet implement this type of function call.
+// Warning: (825-830): Assertion checker does not yet support the type of this variable.
+// Warning: (887-919): Internal error: Expression undefined for SMT solver.
+// Warning: (690-750): Underflow (resulting value less than 0) happens here
+// Warning: (690-750): Overflow (resulting value larger than 2**160 - 1) happens here
+// Warning: (1057-1068): Assertion checker does not yet implement type function () returns (uint256)
+// Warning: (1120-1131): Assertion checker does not yet implement type function () returns (uint256)
+// Warning: (1403-1408): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		if (true) {
+			address a = g();
+			assert(a == address(0));
+		}
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+}
+// ----
+// Warning: (208-218): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (208-218): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_2.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		if (true) {
+			address a = g();
+			assert(a == address(0));
+		}
+		else
+		{
+			address b = g();
+			assert(b == address(0));
+		}
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+}
+// ----
+// Warning: (271-281): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (271-281): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (186-196): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (271-281): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_3.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		if (true) {
+			address a = g();
+			assert(a == address(0));
+		}
+		if (true) {
+			address a = g();
+			assert(a == address(0));
+		}
+
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+}
+// ----
+// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (189-199): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_4.sol

@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		if (true) {
+			address a = g();
+			assert(a == address(0));
+		}
+		if (true) {
+			address a = h();
+			assert(a == address(0));
+		}
+
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+	function h() public pure returns (address) {
+		address a;
+		return a;
+	}
+
+}
+// ----
+// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (189-199): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_else_branch.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		if (true) {
+		} else {
+			address a = g();
+			assert(a == address(0));
+		}
+	}
+	function g() public pure returns (address) {
+		address x;
+		x = address(0);
+		return x;
+	}
+}
+// ----
+// Warning: (219-229): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (134-144): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (219-229): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_modifier_branch.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	modifier m(address a) {
+		if (true) {
+			a = g();
+			_;
+			assert(a == address(0));
+		}
+	}
+
+	function f(address a) m(a) public pure {
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+}
+// ----
+// Warning: (249-259): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (118-128): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (249-259): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_placeholder_inside_modifier_branch.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	modifier m {
+		if (true)
+			_;
+	}
+
+	function f(address a) m public pure {
+		if (true) {
+			a = g();
+			assert(a == address(0));
+		}
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+}
+// ----
+// Warning: (247-257): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (162-172): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (247-257): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/functions/functions_external_4.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint _x) public pure returns (uint) {
+		return _x;
+	}
+}
+
+contract D
+{
+	C c;
+	function g(uint _y) public view {
+		uint z = c.f(_y);
+		assert(z == _y);
+	}
+}
+// ----
+// Warning: (180-187): Internal error: Expression undefined for SMT solver.
+// Warning: (191-206): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_inline_function_inside_branch.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	address owner;
+	modifier m {
+		if (true)
+			owner = g();
+		_;
+	}
+	function f() m public {
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+}
+// ----
+// Warning: (205-215): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (205-215): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol

@@ -22,5 +22,4 @@ contract C
 	}
 }
 // ----
-// Warning: (86-93): Condition is always true.
 // Warning: (311-324): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_parameters.sol

@@ -15,4 +15,3 @@ contract C
 	}
 }
 // ----
-// Warning: (127-132): Condition is always true.

test/libsolidity/smtCheckerTests/modifiers/modifier_return.sol

@@ -18,4 +18,3 @@ contract C
 	}
 }
 // ----
-// Warning: (138-144): Condition is always false.

test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations.sol

@@ -17,5 +17,3 @@ contract C
 	}
 }
 // ----
-// Warning: (137-142): Condition is always true.
-// Warning: (155-164): Condition is always true.