4 files changed, 69 insertions, 22 deletions
diff --git a/libsolidity/codegen/ABIFunctions.cpp b/libsolidity/codegen/ABIFunctions.cpp
index 6648be06..00f59065 100644
--- a/libsolidity/codegen/ABIFunctions.cpp
+++ b/libsolidity/codegen/ABIFunctions.cpp
@@ -120,7 +120,7 @@ string ABIFunctions::tupleDecoder(TypePointers const& _types, bool _fromMemory)
 
 		Whiskers templ(R"(
 			function <functionName>(headStart, dataEnd) -> <valueReturnParams> {
-				switch slt(sub(dataEnd, headStart), <minimumSize>) case 1 { revert(0, 0) }
+				if slt(sub(dataEnd, headStart), <minimumSize>) { revert(0, 0) }
 				<decodeElements>
 			}
 		)");
@@ -151,7 +151,7 @@ string ABIFunctions::tupleDecoder(TypePointers const& _types, bool _fromMemory)
 				R"(
 				{
 					let offset := <load>(add(headStart, <pos>))
-					switch gt(offset, 0xffffffffffffffff) case 1 { revert(0, 0) }
+					if gt(offset, 0xffffffffffffffff) { revert(0, 0) }
 					<values> := <abiDecode>(add(headStart, offset), dataEnd)
 				}
 				)" :
@@ -1134,7 +1134,7 @@ string ABIFunctions::abiDecodingFunctionArray(ArrayType const& _type, bool _from
 			R"(
 				// <readableTypeName>
 				function <functionName>(offset, end) -> array {
-					switch slt(add(offset, 0x1f), end) case 0 { revert(0, 0) }
+					if iszero(slt(add(offset, 0x1f), end)) { revert(0, 0) }
 					let length := <retrieveLength>
 					array := <allocate>(<allocationSize>(length))
 					let dst := array
@@ -1169,7 +1169,7 @@ string ABIFunctions::abiDecodingFunctionArray(ArrayType const& _type, bool _from
 		else
 		{
 			string baseEncodedSize = toCompactHexWithPrefix(_type.baseType()->calldataEncodedSize());
-			templ("staticBoundsCheck", "switch gt(add(src, mul(length, " + baseEncodedSize + ")), end) case 1 { revert(0, 0) }");
+			templ("staticBoundsCheck", "if gt(add(src, mul(length, " + baseEncodedSize + ")), end) { revert(0, 0) }");
 			templ("retrieveElementPos", "src");
 			templ("baseEncodedSize", baseEncodedSize);
 		}
@@ -1197,11 +1197,11 @@ string ABIFunctions::abiDecodingFunctionCalldataArray(ArrayType const& _type)
 			templ = R"(
 				// <readableTypeName>
 				function <functionName>(offset, end) -> arrayPos, length {
-					switch slt(add(offset, 0x1f), end) case 0 { revert(0, 0) }
+					if iszero(slt(add(offset, 0x1f), end)) { revert(0, 0) }
 					length := calldataload(offset)
-					switch gt(length, 0xffffffffffffffff) case 1 { revert(0, 0) }
+					if gt(length, 0xffffffffffffffff) { revert(0, 0) }
 					arrayPos := add(offset, 0x20)
-					switch gt(add(arrayPos, mul(<length>, <baseEncodedSize>)), end) case 1 { revert(0, 0) }
+					if gt(add(arrayPos, mul(<length>, <baseEncodedSize>)), end) { revert(0, 0) }
 				}
 			)";
 		else
@@ -1209,7 +1209,7 @@ string ABIFunctions::abiDecodingFunctionCalldataArray(ArrayType const& _type)
 				// <readableTypeName>
 				function <functionName>(offset, end) -> arrayPos {
 					arrayPos := offset
-					switch gt(add(arrayPos, mul(<length>, <baseEncodedSize>)), end) case 1 { revert(0, 0) }
+					if gt(add(arrayPos, mul(<length>, <baseEncodedSize>)), end) { revert(0, 0) }
 				}
 			)";
 		Whiskers w{templ};
@@ -1235,13 +1235,13 @@ string ABIFunctions::abiDecodingFunctionByteArray(ArrayType const& _type, bool _
 		Whiskers templ(
 			R"(
 				function <functionName>(offset, end) -> array {
-					switch slt(add(offset, 0x1f), end) case 0 { revert(0, 0) }
+					if iszero(slt(add(offset, 0x1f), end)) { revert(0, 0) }
 					let length := <load>(offset)
 					array := <allocate>(<allocationSize>(length))
 					mstore(array, length)
 					let src := add(offset, 0x20)
 					let dst := add(array, 0x20)
-					switch gt(add(src, length), end) case 1 { revert(0, 0) }
+					if gt(add(src, length), end) { revert(0, 0) }
 					<copyToMemFun>(src, dst, length)
 				}
 			)"
@@ -1268,7 +1268,7 @@ string ABIFunctions::abiDecodingFunctionStruct(StructType const& _type, bool _fr
 		Whiskers templ(R"(
 			// <readableTypeName>
 			function <functionName>(headStart, end) -> value {
-				switch slt(sub(end, headStart), <minimumSize>) case 1 { revert(0, 0) }
+				if slt(sub(end, headStart), <minimumSize>) { revert(0, 0) }
 				value := <allocate>(<memorySize>)
 				<#members>
 				{
@@ -1296,7 +1296,7 @@ string ABIFunctions::abiDecodingFunctionStruct(StructType const& _type, bool _fr
 				dynamic ?
 				R"(
 					let offset := <load>(add(headStart, <pos>))
-					switch gt(offset, 0xffffffffffffffff) case 1 { revert(0, 0) }
+					if gt(offset, 0xffffffffffffffff) { revert(0, 0) }
 					mstore(add(value, <memoryOffset>), <abiDecode>(add(headStart, offset), end))
 				)" :
 				R"(
@@ -1501,7 +1501,7 @@ string ABIFunctions::arrayAllocationSizeFunction(ArrayType const& _type)
 		Whiskers w(R"(
 			function <functionName>(length) -> size {
 				// Make sure we can allocate memory without overflow
-				switch gt(length, 0xffffffffffffffff) case 1 { revert(0, 0) }
+				if gt(length, 0xffffffffffffffff) { revert(0, 0) }
 				size := <allocationSize>
 				<addLengthSlot>
 			}
@@ -1620,7 +1620,7 @@ string ABIFunctions::allocationFunction()
 				memPtr := mload(<freeMemoryPointer>)
 				let newFreePtr := add(memPtr, size)
 				// protect against overflow
-				switch or(gt(newFreePtr, 0xffffffffffffffff), lt(newFreePtr, memPtr)) case 1 { revert(0, 0) }
+				if or(gt(newFreePtr, 0xffffffffffffffff), lt(newFreePtr, memPtr)) { revert(0, 0) }
 				mstore(<freeMemoryPointer>, newFreePtr)
 			}
 		)")
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index a22e35d6..d4887a3d 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -71,6 +71,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 	m_interface->reset();
 	m_currentSequenceCounter.clear();
 	m_nextFreeSequenceCounter.clear();
+	m_pathConditions.clear();
 	m_conditionalExecutionHappened = false;
 	initializeLocalVariables(_function);
 	return true;
@@ -344,14 +345,14 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 		solAssert(args.size() == 1, "");
 		solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
 		checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
-		m_interface->addAssertion(expr(*args[0]));
+		addPathImpliedExpression(expr(*args[0]));
 	}
 	else if (funType.kind() == FunctionType::Kind::Require)
 	{
 		solAssert(args.size() == 1, "");
 		solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
 		checkBooleanNotConstant(*args[0], "Condition is always $VALUE.");
-		m_interface->addAssertion(expr(*args[0]));
+		addPathImpliedExpression(expr(*args[0]));
 	}
 }
 
@@ -514,11 +515,11 @@ void SMTChecker::visitBranch(Statement const& _statement, smt::Expression const*
 {
 	VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
 
-	m_interface->push();
 	if (_condition)
-		m_interface->addAssertion(*_condition);
+		pushPathCondition(*_condition);
 	_statement.accept(*this);
-	m_interface->pop();
+	if (_condition)
+		popPathCondition();
 
 	m_conditionalExecutionHappened = true;
 	m_currentSequenceCounter = sequenceCountersStart;
@@ -533,7 +534,7 @@ void SMTChecker::checkCondition(
 )
 {
 	m_interface->push();
-	m_interface->addAssertion(_condition);
+	addPathConjoinedExpression(_condition);
 
 	vector<smt::Expression> expressionsToEvaluate;
 	vector<string> expressionNames;
@@ -605,12 +606,12 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
 		return;
 
 	m_interface->push();
-	m_interface->addAssertion(expr(_condition));
+	addPathConjoinedExpression(expr(_condition));
 	auto positiveResult = checkSatisifable();
 	m_interface->pop();
 
 	m_interface->push();
-	m_interface->addAssertion(!expr(_condition));
+	addPathConjoinedExpression(!expr(_condition));
 	auto negatedResult = checkSatisifable();
 	m_interface->pop();
 
@@ -828,3 +829,31 @@ smt::Expression SMTChecker::var(Declaration const& _decl)
 	solAssert(m_variables.count(&_decl), "");
 	return m_variables.at(&_decl);
 }
+
+void SMTChecker::popPathCondition()
+{
+	solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty.");
+	m_pathConditions.pop_back();
+}
+
+void SMTChecker::pushPathCondition(smt::Expression const& _e)
+{
+	m_pathConditions.push_back(currentPathConditions() && _e);
+}
+
+smt::Expression SMTChecker::currentPathConditions()
+{
+	if (m_pathConditions.size() == 0)
+		return smt::Expression(true);
+	return m_pathConditions.back();
+}
+
+void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e)
+{
+	m_interface->addAssertion(currentPathConditions() && _e);
+}
+
+void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
+{
+	m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
+}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index e7481cca..539221cc 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -26,6 +26,7 @@
 
 #include <map>
 #include <string>
+#include <vector>
 
 namespace dev
 {
@@ -145,6 +146,17 @@ private:
 	/// The function takes one argument which is the "sequence number".
 	smt::Expression var(Declaration const& _decl);
 
+	/// Adds a new path condition
+	void pushPathCondition(smt::Expression const& _e);
+	/// Remove the last path condition
+	void popPathCondition();
+	/// Returns the conjunction of all path conditions or True if empty
+	smt::Expression currentPathConditions();
+	/// 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
+	void addPathImpliedExpression(smt::Expression const& _e);
+
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::shared_ptr<VariableUsage> m_variableUsage;
 	bool m_conditionalExecutionHappened = false;
@@ -152,6 +164,7 @@ private:
 	std::map<Declaration const*, int> m_nextFreeSequenceCounter;
 	std::map<Expression const*, smt::Expression> m_expressions;
 	std::map<Declaration const*, smt::Expression> m_variables;
+	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;
 
 	FunctionDefinition const* m_currentFunction = nullptr;
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 74c993e8..88487310 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -72,6 +72,11 @@ public:
 		}, _trueValue.sort);
 	}
 
+	static Expression implies(Expression _a, Expression _b)
+	{
+		return !std::move(_a) || std::move(_b);
+	}
+
 	friend Expression operator!(Expression _a)
 	{
 		return Expression("not", std::move(_a), Sort::Bool);