[SMTChecker] Add loop support

Changelog.md

@@ -7,6 +7,7 @@ Language Features:
 Compiler Features:
  * ABI Output: Change sorting order of functions from selector to kind, name.
  * Optimizer: Add rule that replaces the BYTE opcode by 0 if the first argument is larger than 31.
+ * SMTChecker: Add loop support to the CHC engine.
  * Yul Optimizer: Take side-effect-freeness of user-defined functions into account.
  * Yul Optimizer: Remove redundant mload/sload operations.
 

libsolidity/formal/CHC.cpp

@@ -74,8 +74,10 @@ bool CHC::visit(ContractDefinition const& _contract)
 		else
 			m_stateSorts.push_back(smt::smtSort(*var->type()));
 
+	clearIndices();
+
 	string interfaceName = "interface_" + _contract.name() + "_" + to_string(_contract.id());
-	m_interfacePredicate = createBlock(interfaceSort(),	interfaceName);
+	m_interfacePredicate = createSymbolicBlock(interfaceSort(), interfaceName);
 
 	// TODO create static instances for Bool/Int sorts in SolverInterface.
 	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
@@ -83,7 +85,7 @@ bool CHC::visit(ContractDefinition const& _contract)
 		vector<smt::SortPointer>(),
 		boolSort
 	);
-	m_errorPredicate = createBlock(errorFunctionSort, "error");
+	m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error");
 
 	// If the contract has a constructor it is handled as a function.
 	// Otherwise we zero-initialize all state vars.
@@ -91,7 +93,9 @@ bool CHC::visit(ContractDefinition const& _contract)
 	if (!_contract.constructor())
 	{
 		string constructorName = "constructor_" + _contract.name() + "_" + to_string(_contract.id());
-		m_constructorPredicate = createBlock(constructorSort(), constructorName);
+		m_constructorPredicate = createSymbolicBlock(constructorSort(), constructorName);
+		smt::Expression constructorPred = (*m_constructorPredicate)({});
+		addRule(constructorPred, constructorName);
 
 		for (auto const& var: m_stateVariables)
 		{
@@ -101,14 +105,7 @@ bool CHC::visit(ContractDefinition const& _contract)
 			m_context.setZeroValue(*symbVar);
 		}
 
-		smt::Expression constructorAppl = (*m_constructorPredicate)({});
-		m_interface->addRule(constructorAppl, constructorName);
-
-		smt::Expression constructorInterface = smt::Expression::implies(
-			constructorAppl && m_context.assertions(),
-			interface()
-		);
-		m_interface->addRule(constructorInterface, constructorName + "_to_" + interfaceName);
+		connectBlocks(constructorPred, interface());
 	}
 
 	return true;
@@ -119,10 +116,13 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	if (!shouldVisit(_contract))
 		return;
 
-	auto errorAppl = (*m_errorPredicate)({});
-	for (auto const& target: m_verificationTargets)
+	for (unsigned i = 0; i < m_verificationTargets.size(); ++i)
+	{
+		auto const& target = m_verificationTargets.at(i);
+		auto errorAppl = error(i + 1);
 		if (query(errorAppl, target->location()))
 			m_safeAssertions.insert(target);
+	}
 
 	SMTEncoder::endVisit(_contract);
 }
@@ -139,39 +139,25 @@ bool CHC::visit(FunctionDefinition const& _function)
 
 	// Store the constraints related to variable initialization.
 	smt::Expression const& initAssertions = m_context.assertions();
-
-	createFunctionBlock(*m_currentFunction);
-
-	// Rule Interface -> FunctionEntry, uses no constraints.
-	smt::Expression interfaceFunction = smt::Expression::implies(
-		interface(),
-		predicateCurrent(m_currentFunction)
-	);
-	m_interface->addRule(
-		interfaceFunction,
-		m_interfacePredicate->currentName() + "_to_" + m_predicates.at(m_currentFunction)->currentName()
-	);
-
-	pushBlock(predicateCurrent(m_currentFunction));
-
-	createFunctionBlock(m_currentFunction->body());
-
-	// Rule FunctionEntry -> FunctionBody, also no constraints.
-	smt::Expression functionBody = smt::Expression::implies(
-		predicateEntry(m_currentFunction),
-		predicateBodyCurrent(&m_currentFunction->body())
-	);
-	m_interface->addRule(
-		functionBody,
-		m_predicates.at(m_currentFunction)->currentName() + "_to_" + m_predicates.at(&m_currentFunction->body())->currentName()
-	);
-
-	pushBlock(predicateBodyCurrent(&m_currentFunction->body()));
-	// We need to re-add the constraints that were created for initialization of variables.
-	m_context.addAssertion(initAssertions);
+	m_context.pushSolver();
 
 	solAssert(m_functionBlocks == 0, "");
-	m_functionBlocks = 2;
+
+	createBlock(m_currentFunction);
+	createBlock(&m_currentFunction->body(), "block_");
+
+	auto functionPred = predicate(m_currentFunction);
+	auto bodyPred = predicate(&m_currentFunction->body());
+
+	connectBlocks(interface(), functionPred);
+	connectBlocks(functionPred, bodyPred);
+
+	m_context.popSolver();
+
+	pushBlock(&m_currentFunction->body());
+
+	// We need to re-add the constraints that were created for initialization of variables.
+	m_context.addAssertion(initAssertions);
 
 	SMTEncoder::visit(*m_currentFunction);
 
@@ -185,35 +171,22 @@ void CHC::endVisit(FunctionDefinition const& _function)
 
 	solAssert(m_currentFunction == &_function, "Inlining internal function calls not yet implemented");
 
-	// Create Function Exit block.
-	createFunctionBlock(*m_currentFunction);
-
-	// Rule FunctionBody -> FunctionExit.
-	smt::Expression bodyFunction = smt::Expression::implies(
-		predicateEntry(&_function.body()) && m_context.assertions(),
-		predicateCurrent(&_function)
-	);
-	m_interface->addRule(
-		bodyFunction,
-		m_predicates.at(&_function.body())->currentName() + "_to_" + m_predicates.at(&_function.body())->currentName()
-	);
+	// Function Exit block.
+	createBlock(m_currentFunction);
+	connectBlocks(m_path.back(), predicate(&_function));
 
 	// Rule FunctionExit -> Interface, uses no constraints.
-	smt::Expression functionInterface = smt::Expression::implies(
-		predicateCurrent(&_function),
-		interface()
-	);
-	m_interface->addRule(
-		functionInterface,
-		m_predicates.at(&_function)->currentName() + "_to_" + m_interfacePredicate->currentName()
-	);
+	clearIndices();
+	m_context.pushSolver();
+	connectBlocks(predicate(&_function), interface());
+	m_context.popSolver();
 
 	m_currentFunction = nullptr;
 	solAssert(m_path.size() == m_functionBlocks, "");
-	for (unsigned i = 0; i < m_path.size(); ++i)
-		m_context.popSolver();
-	m_functionBlocks = 0;
-	m_path.clear();
+	while (m_functionBlocks > 0)
+		popBlock();
+
+	solAssert(m_path.empty(), "");
 
 	SMTEncoder::endVisit(_function);
 }
@@ -237,15 +210,51 @@ bool CHC::visit(IfStatement const& _if)
 
 bool CHC::visit(WhileStatement const& _while)
 {
-	eraseKnowledge();
-	m_context.resetVariables(touchedVariables(_while));
+	bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen;
+	m_unknownFunctionCallSeen = false;
+
+	solAssert(m_currentFunction, "");
+
+	if (_while.isDoWhile())
+		_while.body().accept(*this);
+
+	visitLoop(
+		_while,
+		&_while.condition(),
+		_while.body(),
+		nullptr
+	);
+
+	if (m_unknownFunctionCallSeen)
+		eraseKnowledge();
+
+	m_unknownFunctionCallSeen = unknownFunctionCallWasSeen;
+
 	return false;
 }
 
 bool CHC::visit(ForStatement const& _for)
 {
-	eraseKnowledge();
-	m_context.resetVariables(touchedVariables(_for));
+	bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen;
+	m_unknownFunctionCallSeen = false;
+
+	solAssert(m_currentFunction, "");
+
+	if (auto init = _for.initializationExpression())
+		init->accept(*this);
+
+	visitLoop(
+		_for,
+		_for.condition(),
+		_for.body(),
+		_for.loopExpression()
+	);
+
+	if (m_unknownFunctionCallSeen)
+		eraseKnowledge();
+
+	m_unknownFunctionCallSeen = unknownFunctionCallWasSeen;
+
 	return false;
 }
 
@@ -292,6 +301,18 @@ void CHC::endVisit(FunctionCall const& _funCall)
 	createReturnedExpressions(_funCall);
 }
 
+void CHC::endVisit(Break const&)
+{
+	solAssert(m_breakDest, "");
+	m_breakSeen = true;
+}
+
+void CHC::endVisit(Continue const&)
+{
+	solAssert(m_continueDest, "");
+	m_continueSeen = true;
+}
+
 void CHC::visitAssert(FunctionCall const& _funCall)
 {
 	auto const& args = _funCall.arguments();
@@ -300,13 +321,10 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 
 	solAssert(!m_path.empty(), "");
 
+	createErrorBlock();
+
 	smt::Expression assertNeg = !(m_context.expression(*args.front())->currentValue());
-	smt::Expression assertionError = smt::Expression::implies(
-		m_path.back() && m_context.assertions() && currentPathConditions() && assertNeg,
-		error()
-	);
-	string predicateName = "assert_" + to_string(_funCall.id());
-	m_interface->addRule(assertionError, predicateName + "_to_error");
+	connectBlocks(m_path.back(), error(), currentPathConditions() && assertNeg);
 
 	m_verificationTargets.push_back(&_funCall);
 }
@@ -323,6 +341,85 @@ void CHC::unknownFunctionCall(FunctionCall const&)
 	m_unknownFunctionCallSeen = true;
 }
 
+void CHC::visitLoop(
+	BreakableStatement const& _loop,
+	Expression const* _condition,
+	Statement const& _body,
+	ASTNode const* _postLoop
+)
+{
+	bool breakWasSeen = m_breakSeen;
+	bool continueWasSeen = m_continueSeen;
+	m_breakSeen = false;
+	m_continueSeen = false;
+
+	solAssert(m_currentFunction, "");
+	auto const& functionBody = m_currentFunction->body();
+
+	createBlock(&_loop, "loop_header_");
+	createBlock(&_body, "loop_body_");
+	createBlock(&functionBody, "block_");
+
+	connectBlocks(m_path.back(), predicate(&_loop));
+
+	// We need to save the next block here because new blocks
+	// might be created inside the loop body.
+	// This will be m_path.back() in the end of this function.
+	pushBlock(&functionBody);
+
+	smt::Expression loopHeader = predicate(&_loop);
+	pushBlock(&_loop);
+
+	if (_condition)
+		_condition->accept(*this);
+	auto condition = _condition ? expr(*_condition) : smt::Expression(true);
+
+	connectBlocks(loopHeader, predicate(&_body), condition);
+	connectBlocks(loopHeader, predicate(&functionBody), !condition);
+
+	// Loop body visit.
+	pushBlock(&_body);
+
+	m_breakDest = &functionBody;
+	m_continueDest = _postLoop ? _postLoop : &_loop;
+
+	auto functionBlocks = m_functionBlocks;
+	_body.accept(*this);
+	if (_postLoop)
+	{
+		createBlock(_postLoop, "loop_post_");
+		connectBlocks(m_path.back(), predicate(_postLoop));
+		pushBlock(_postLoop);
+		_postLoop->accept(*this);
+	}
+
+	// Back edge.
+	connectBlocks(m_path.back(), predicate(&_loop));
+
+	// Pop all function blocks created by nested inner loops
+	// to adjust the assertion context.
+	for (unsigned i = m_functionBlocks; i > functionBlocks; --i)
+		popBlock();
+	m_functionBlocks = functionBlocks;
+
+	// Loop body
+	popBlock();
+	// Loop header
+	popBlock();
+
+	// New function block starts with indices = 0
+	clearIndices();
+
+	if (m_breakSeen || m_continueSeen)
+	{
+		eraseKnowledge();
+		m_context.resetVariables([](VariableDeclaration const&) { return true; });
+	}
+
+	m_breakSeen = breakWasSeen;
+	m_continueSeen = continueWasSeen;
+}
+
 void CHC::reset()
 {
 	m_stateSorts.clear();
@@ -330,6 +427,8 @@ void CHC::reset()
 	m_verificationTargets.clear();
 	m_safeAssertions.clear();
 	m_unknownFunctionCallSeen = false;
+	m_breakSeen = false;
+	m_continueSeen = false;
 }
 
 void CHC::eraseKnowledge()
@@ -352,22 +451,26 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const
 {
 	if (
 		_function.isPublic() &&
-		_function.isImplemented()
+		_function.isImplemented() &&
+		!_function.isConstructor()
 	)
 		return true;
 	return false;
 }
 
-void CHC::pushBlock(smt::Expression const& _block)
+void CHC::pushBlock(ASTNode const* _node)
 {
+	clearIndices();
 	m_context.pushSolver();
-	m_path.push_back(_block);
+	m_path.push_back(predicate(_node));
+	++m_functionBlocks;
 }
 
 void CHC::popBlock()
 {
 	m_context.popSolver();
 	m_path.pop_back();
+	--m_functionBlocks;
 }
 
 smt::SortPointer CHC::constructorSort()
@@ -404,12 +507,13 @@ smt::SortPointer CHC::sort(FunctionDefinition const& _function)
 	return m_nodeSorts[&_function] = move(sort);
 }
 
-smt::SortPointer CHC::sort(Block const& _block)
+smt::SortPointer CHC::sort(ASTNode const* _node)
 {
-	if (m_nodeSorts.count(&_block))
-		return m_nodeSorts.at(&_block);
+	if (m_nodeSorts.count(_node))
+		return m_nodeSorts.at(_node);
 
-	solAssert(_block.scope() == m_currentFunction, "");
+	if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
+		return sort(*funDef);
 
 	auto fSort = dynamic_pointer_cast<smt::FunctionSort>(sort(*m_currentFunction));
 	solAssert(fSort, "");
@@ -422,10 +526,10 @@ smt::SortPointer CHC::sort(Block const& _block)
 		fSort->domain + varSorts,
 		boolSort
 	);
-	return m_nodeSorts[&_block] = move(functionBodySort);
+	return m_nodeSorts[_node] = move(functionBodySort);
 }
 
-unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(smt::SortPointer _sort, string const& _name)
+unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPointer _sort, string const& _name)
 {
 	auto block = make_unique<smt::SymbolicFunctionVariable>(
 		_sort,
@@ -462,33 +566,36 @@ smt::Expression CHC::error()
 	return (*m_errorPredicate)({});
 }
 
-void CHC::createFunctionBlock(FunctionDefinition const& _function)
+smt::Expression CHC::error(unsigned _idx)
 {
-	if (m_predicates.count(&_function))
-	{
-		m_predicates.at(&_function)->increaseIndex();
-		m_interface->registerRelation(m_predicates.at(&_function)->currentValue());
-	}
-	else
-		m_predicates[&_function] = createBlock(
-			sort(_function),
-			predicateName(_function)
-		);
+	return m_errorPredicate->valueAtIndex(_idx)({});
 }
 
-void CHC::createFunctionBlock(Block const& _block)
+void CHC::createBlock(ASTNode const* _node, string const& _prefix)
 {
-	solAssert(_block.scope() == m_currentFunction, "");
-	if (m_predicates.count(&_block))
+	if (m_predicates.count(_node))
 	{
-		m_predicates.at(&_block)->increaseIndex();
-		m_interface->registerRelation(m_predicates.at(&_block)->currentValue());
+		m_predicates.at(_node)->increaseIndex();
+		m_interface->registerRelation(m_predicates.at(_node)->currentValue());
 	}
 	else
-		m_predicates[&_block] = createBlock(
-			sort(_block),
-			predicateName(*m_currentFunction) + "_body"
-		);
+		m_predicates[_node] = createSymbolicBlock(sort(_node), _prefix + predicateName(_node));
+}
+
+void CHC::createErrorBlock()
+{
+	solAssert(m_errorPredicate, "");
+	m_errorPredicate->increaseIndex();
+	m_interface->registerRelation(m_errorPredicate->currentValue());
+}
+
+void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints)
+{
+	smt::Expression edge = smt::Expression::implies(
+		_from && m_context.assertions() && _constraints,
+		_to
+	);
+	addRule(edge, _from.name + "_to_" + _to.name);
 }
 
 vector<smt::Expression> CHC::currentFunctionVariables()
@@ -511,30 +618,44 @@ vector<smt::Expression> CHC::currentBlockVariables()
 	return currentFunctionVariables() + paramExprs;
 }
 
-string CHC::predicateName(FunctionDefinition const& _function)
+void CHC::clearIndices()
 {
-	string functionName = _function.isConstructor() ?
-		"constructor" :
-		_function.isFallback() ?
-			"fallback" :
-			"function_" + _function.name();
-	return functionName + "_" + to_string(_function.id());
+	for (auto const& var: m_stateVariables)
+		m_context.variable(*var)->resetIndex();
+	if (m_currentFunction)
+	{
+		for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
+			m_context.variable(*var)->resetIndex();
+		for (auto const& var: m_currentFunction->localVariables())
+			m_context.variable(*var)->resetIndex();
+	}
 }
 
-smt::Expression CHC::predicateCurrent(ASTNode const* _node)
+string CHC::predicateName(ASTNode const* _node)
 {
-	return (*m_predicates.at(_node))(currentFunctionVariables());
+	string prefix;
+	if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
+	{
+		prefix = funDef->isConstructor() ?
+			"constructor" :
+			funDef->isFallback() ?
+				"fallback" :
+				"function_" + funDef->name();
+		prefix += "_";
+	}
+	return prefix + to_string(_node->id());
 }
 
-smt::Expression CHC::predicateBodyCurrent(ASTNode const* _node)
+smt::Expression CHC::predicate(ASTNode const* _node)
 {
+	if (dynamic_cast<FunctionDefinition const*>(_node))
+		return (*m_predicates.at(_node))(currentFunctionVariables());
 	return (*m_predicates.at(_node))(currentBlockVariables());
 }
 
-smt::Expression CHC::predicateEntry(ASTNode const* _node)
+void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
 {
-	solAssert(!m_path.empty(), "");
-	return (*m_predicates.at(_node))(m_path.back().arguments);
+	m_interface->addRule(_rule, _ruleName);
 }
 
 bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location)

libsolidity/formal/CHC.h

@@ -61,9 +61,17 @@ private:
 	bool visit(WhileStatement const&) override;
 	bool visit(ForStatement const&) override;
 	void endVisit(FunctionCall const& _node) override;
+	void endVisit(Break const& _node) override;
+	void endVisit(Continue const& _node) override;
 
 	void visitAssert(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);
+	void visitLoop(
+		BreakableStatement const& _loop,
+		Expression const* _condition,
+		Statement const& _body,
+		ASTNode const* _postLoop
+	);
 	//@}
 
 	/// Helpers.
@@ -72,7 +80,7 @@ private:
 	void eraseKnowledge();
 	bool shouldVisit(ContractDefinition const& _contract) const;
 	bool shouldVisit(FunctionDefinition const& _function) const;
-	void pushBlock(smt::Expression const& _block);
+	void pushBlock(ASTNode const* _node);
 	void popBlock();
 	//@}
 
@@ -81,13 +89,13 @@ private:
 	smt::SortPointer constructorSort();
 	smt::SortPointer interfaceSort();
 	smt::SortPointer sort(FunctionDefinition const& _function);
-	smt::SortPointer sort(Block const& _block);
+	smt::SortPointer sort(ASTNode const* _block);
 	//@}
 
 	/// Predicate helpers.
 	//@{
 	/// @returns a new block of given _sort and _name.
-	std::unique_ptr<smt::SymbolicFunctionVariable> createBlock(smt::SortPointer _sort, std::string const& _name);
+	std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smt::SortPointer _sort, std::string const& _name);
 
 	/// Constructor predicate over current variables.
 	smt::Expression constructor();
@@ -95,16 +103,17 @@ private:
 	smt::Expression interface();
 	/// Error predicate over current variables.
 	smt::Expression error();
+	smt::Expression error(unsigned _idx);
 
-	/// Creates a block for the given _function or increases its SSA index
+	/// Creates a block for the given _node or increases its SSA index
 	/// if the block already exists which in practice creates a new function.
-	/// The predicate parameters are _function input and output parameters.
-	void createFunctionBlock(FunctionDefinition const& _function);
-	/// Creates a block for the given _function or increases its SSA index
-	/// if the block already exists which in practice creates a new function.
-	/// The predicate parameters are m_currentFunction input, output
-	/// and local variables.
-	void createFunctionBlock(Block const& _block);
+	void createBlock(ASTNode const* _node, std::string const& _prefix = "");
+
+	/// Creates a new error block to be used by an assertion.
+	/// Also registers the predicate.
+	void createErrorBlock();
+
+	void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true));
 
 	/// @returns the current symbolic values of the current function's
 	/// input and output parameters.
@@ -113,19 +122,20 @@ private:
 	/// local variables.
 	std::vector<smt::Expression> currentBlockVariables();
 
-	/// @returns the predicate name for a given function.
-	std::string predicateName(FunctionDefinition const& _function);
-	/// @returns a predicate application over the current function's parameters.
-	smt::Expression predicateCurrent(ASTNode const* _node);
-	/// @returns a predicate application over the current function's parameters plus local variables.
-	smt::Expression predicateBodyCurrent(ASTNode const* _node);
-	/// Predicate for block _node over the variables at the latest
-	/// block entry.
-	smt::Expression predicateEntry(ASTNode const* _node);
+	/// Sets the SSA indices of the variables in scope to 0.
+	/// Used when starting a new block.
+	void clearIndices();
+
+	/// @returns the predicate name for a given node.
+	std::string predicateName(ASTNode const* _node);
+	/// @returns a predicate application over the current scoped variables.
+	smt::Expression predicate(ASTNode const* _node);
 	//@}
 
 	/// Solver related.
 	//@{
+	/// Adds Horn rule to the solver.
+	void addRule(smt::Expression const& _rule, std::string const& _ruleName);
 	/// @returns true if query is unsatisfiable (safe).
 	bool query(smt::Expression const& _query, langutil::SourceLocation const& _location);
 	//@}
@@ -179,6 +189,15 @@ private:
 	std::vector<smt::Expression> m_path;
 	/// Whether a function call was seen in the current scope.
 	bool m_unknownFunctionCallSeen = false;
+	/// Whether a break statement was seen in the current scope.
+	bool m_breakSeen = false;
+	/// Whether a continue statement was seen in the current scope.
+	bool m_continueSeen = false;
+
+	/// Block where a loop break should go to.
+	ASTNode const* m_breakDest;
+	/// Block where a loop continue should go to.
+	ASTNode const* m_continueDest;
 	//@}
 
 	/// CHC solver.

libsolidity/formal/SMTEncoder.cpp

@@ -953,18 +953,21 @@ pair<smt::Expression, smt::Expression> SMTEncoder::arithmeticOperation(
 
 	smt::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1;
 	auto value = smt::Expression::ite(
-		valueNoMod > smt::maxValue(intType) || valueNoMod < smt::minValue(intType),
+		valueNoMod > smt::maxValue(intType),
 		valueNoMod % intValueRange,
-		valueNoMod
+		smt::Expression::ite(
+			valueNoMod < smt::minValue(intType),
+			valueNoMod % intValueRange,
+			valueNoMod
+		)
 	);
+
 	if (intType.isSigned())
-	{
 		value = smt::Expression::ite(
 			value > smt::maxValue(intType),
 			value - intValueRange,
 			value
 		);
-	}
 
 	return {value, valueNoMod};
 }

libsolidity/formal/SMTEncoder.h

@@ -87,6 +87,8 @@ protected:
 	bool visit(MemberAccess const& _node) override;
 	void endVisit(IndexAccess const& _node) override;
 	bool visit(InlineAssembly const& _node) override;
+	void endVisit(Break const&) override {}
+	void endVisit(Continue const&) override {}
 
 	/// Do not visit subtree if node is a RationalNumber.
 	/// Symbolic _expr is the rational literal.

libsolidity/formal/SymbolicTypes.cpp

@@ -295,7 +295,6 @@ Expression zeroValue(solidity::TypePointer const& _type)
 			auto mappingType = dynamic_cast<MappingType const*>(_type);
 			solAssert(mappingType, "");
 			return Expression::const_array(Expression(mappingType), zeroValue(mappingType->valueType()));
-
 		}
 		solAssert(false, "");
 	}

libsolidity/formal/Z3CHCInterface.cpp

@@ -41,6 +41,7 @@ Z3CHCInterface::Z3CHCInterface():
 	// These are useful for solving problems with arrays and loops.
 	// Use quantified lemma generalizer.
 	p.set("fp.spacer.q3.use_qgen", true);
+	p.set("fp.spacer.mbqi", false);
 	// Ground pobs by using values from a model.
 	p.set("fp.spacer.ground_pobs", false);
 	m_solver.set(p);
@@ -100,7 +101,7 @@ pair<CheckResult, vector<string>> Z3CHCInterface::query(Expression const& _expr)
 		}
 		// TODO retrieve model / invariants
 	}
-	catch (z3::exception const& _e)
+	catch (z3::exception const&)
 	{
 		result = CheckResult::ERROR;
 		values.clear();

test/libsolidity/smtCheckerTests/invariants/loop_array.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract Simple {
+	uint[] a;
+	function f(uint n) public {
+		uint i;
+		while (i < n)
+		{
+			a[i] = i;
+			++i;
+		}
+		require(n > 1);
+		// Assertion is safe but current solver version cannot solve it.
+		// Keep test for next solver release.
+		assert(a[n-1] > a[n-2]);
+	}
+}
+// ----
+// Warning: (273-296): Assertion violation happens here

test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract Simple {
+	uint[] a;
+	function f(uint n) public {
+		uint i;
+		for (i = 0; i < n; ++i)
+			a[i] = i;
+		require(n > 1);
+		// Assertion is safe but current solver version cannot solve it.
+		// Keep test for next solver release.
+		assert(a[n-1] > a[n-2]);
+	}
+}
+// ----
+// Warning: (267-290): Assertion violation happens here

test/libsolidity/smtCheckerTests/invariants/loop_basic.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract Simple {
+	function f(uint x) public pure {
+		uint y;
+		require(x > 0);
+		while (y < x)
+			++y;
+		assert(y == x);
+	}
+}

test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract Simple {
+	function f(uint x) public pure {
+		uint y;
+		for (y = 0; y < x; ++y) {}
+		assert(y == x);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/invariants/loop_nested.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract Simple {
+	function f() public pure {
+		uint x = 10;
+		uint y;
+		while (y < x)
+		{
+			++y;
+			x = 0;
+			while (x < 10)
+				++x;
+			assert(x == 10);
+		}
+		assert(y == x);
+	}
+}

test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract Simple {
+	function f() public pure {
+		uint x;
+		uint y;
+		for (x = 10; y < x; ++y)
+		{
+			for (x = 0; x < 10; ++x) {}
+			assert(x == 10);
+		}
+		assert(y == x);
+	}
+}

test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol

@@ -15,4 +15,3 @@ contract C
 }
 // ----
 // Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (269-282): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol

@@ -8,10 +8,12 @@ contract C
 			// Overflows due to resetting x.
 			x = x + 1;
 		}
-		// The assertion is true but x is touched and reset.
+		// Assertion is safe but current solver version cannot solve it.
+		// Keep test for next solver release.
 		assert(x > 0);
 	}
 }
 // ----
+// Warning: (296-309): Error trying to invoke SMT solver.
 // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (244-257): Assertion violation happens here
+// Warning: (296-309): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_6.sol

@@ -10,4 +10,3 @@ contract C {
     }
 }
 // ----
-// Warning: (213-226): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol

@@ -18,5 +18,4 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning: (265-285): Assertion violation happens here
 // Warning: (312-331): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol

@@ -18,6 +18,5 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning: (266-286): Assertion violation happens here
 // Warning: (290-309): Assertion violation happens here
 // Warning: (313-332): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol

@@ -15,4 +15,3 @@ contract C {
 }
 // ----
 // Warning: (115-121): Unused local variable.
-// Warning: (356-370): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1.sol

@@ -14,4 +14,3 @@ contract C
 	}
 }
 // ----
-// Warning: (177-190): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1_break.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 10);
+		while (x < 10) {
+			if (b)
+				++x;
+			else {
+				x = 20;
+				break;
+			}
+		}
+		// Assertion is safe but break is unsupported for now
+		// so knowledge is erased.
+		assert(x >= 10);
+	}
+}
+// ----
+// Warning: (274-289): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1_break_fail.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 10);
+		while (x < 10) {
+			if (b)
+				++x;
+			else {
+				break;
+			}
+		}
+		// Fails because the loop might break.
+		assert(x >= 10);
+	}
+}
+// ----
+// Warning: (218-233): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1_continue.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 100);
+		while (x < 10) {
+			if (b) {
+				x = 15;
+				continue;
+			}
+			else
+				x = 20;
+
+		}
+		// Should be safe, but fails due to continue being unsupported
+		// and erasing all knowledge.
+		assert(x >= 15);
+	}
+}
+// ----
+// Warning: (294-309): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1_continue_fail.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 100);
+		while (x < 10) {
+			if (b) {
+				x = 15;
+				continue;
+			}
+			else
+				x = 20;
+
+		}
+		// Fails due to the if.
+		assert(x >= 17);
+	}
+}
+// ----
+// Warning: (223-238): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_1_infinite.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, bool b) public pure {
+		require(x < 100);
+		while (x < 10) {
+			if (b)
+				x = x + 1;
+			else
+				x = 0;
+		}
+		// CHC proves it safe because
+		// 1- if it doesn't go in the loop in the first place, x >= 10
+		// 2- if it goes in the loop and b == true, x increases until >= 10
+		// 3- if it goes in the loop and b == false, it's an infinite loop, therefore
+		//    the assertion and the error are unreachable.
+		assert(x > 0);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/loops/while_2.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x) public pure {
+		x = 2;
+		while (x > 1) {
+			if (x > 10)
+				x = 2;
+			else
+				--x;
+		}
+		assert(x < 2);
+	}
+}

test/libsolidity/smtCheckerTests/loops/while_2_break.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint x = 0;
+		while (x == 0) {
+			++x;
+			break;
+			++x;
+		}
+		// Assertion is safe but break is unsupported for now
+		// so knowledge is erased.
+		assert(x == 1);
+	}
+}
+// ----
+// Warning: (128-131): Unreachable code.
+// Warning: (224-238): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		while (x == 0) {
+			++x;
+			break;
+			++x;
+		}
+		assert(x == 2);
+	}
+}
+// ----
+// Warning: (120-123): Unreachable code.
+// Warning: (131-145): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_2_fail.sol

@@ -12,4 +12,3 @@ contract C {
 	}
 }
 // ----
-// Warning: (158-172): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol

@@ -13,11 +13,13 @@ contract LoopFor2 {
 			c[i] = b[i];
 			++i;
 		}
+		// Fails due to aliasing, since both b and c are
+		// memory references of same type.
 		assert(b[0] == c[0]);
 		assert(a[0] == 900);
 		assert(b[0] == 900);
 	}
 }
 // ----
-// Warning: (274-294): Assertion violation happens here
-// Warning: (321-340): Assertion violation happens here
+// Warning: (362-382): Assertion violation happens here
+// Warning: (409-428): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol

@@ -20,5 +20,4 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning: (265-285): Assertion violation happens here
 // Warning: (312-331): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol

@@ -20,6 +20,5 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning: (266-286): Assertion violation happens here
 // Warning: (290-309): Assertion violation happens here
 // Warning: (313-332): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol

@@ -8,4 +8,3 @@ contract C {
     }
 }
 // ----
-// Warning: (199-213): Assertion violation happens here

test/libsolidity/smtCheckerTestsJSON/multi.json

@@ -4,7 +4,6 @@
 		"smtlib2responses":
 		{
 			"0x047d0c67d7e03c5ac96ca227d1e19ba63257f4ab19cef30029413219ec8963af": "sat\n((|EVALEXPR_0| 0))\n",
-			"0x21d5b49d1416d788fe34b1d2a10a99ea92b007e17a977604afd7b2ff01a055cd": "unsat\n",
 			"0xada7569fb01a9b3e2823517ed40dcc99b11fb1e433e6e3ec8a8713f6f95753d3": "sat\n((|EVALEXPR_0| 1))\n"
 		}
 	}