diff --git a/.circleci/config.yml b/.circleci/config.yml
index fff6e6b67..0224ac93b 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -9,22 +9,23 @@ version: 2.1
 parameters:
   ubuntu-1804-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1804-3
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:19f613d2ac47fedff654dacef984d8a64726c4d67ae8f2667a85ee7d97ac4c1c"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1804-4
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:79ccaf5a294a3c4f480b2cd69c6d845540c12435e64d732e8536f8f99ad35f03"
   ubuntu-2004-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-3
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:aeedbe7390a7383815f0cf0f8a1b8bf84dc5e334a3b0043ebcdf8b1bdbe80a81"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-4
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:aca1372dcc5edadd3db13ff1aa6807727d79e08082a48eb7cc05444c1b516ace"
   ubuntu-2004-clang-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-3
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:2593c15689dee5b5bdfff96a36c8c68a468cd3b147c41f75b820b8fabc257be9"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-4
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:0954edfb48a7efa6922b4d6adf536a2fc483ca34ad62f95ec54c33a616a66974"
   ubuntu-1604-clang-ossfuzz-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-5
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:65901cd8b64b5959bc4c907df47bb7be3d3b00c9ae8948c75aad7d4c57875cf0"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-6
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:990ed3aaac3fcb87ca9b63a021a91ed89dfd165b341aa7b5c6457cdbe132dfb3"
   emscripten-docker-image:
     type: string
+    # solbuildpackpusher/solidity-buildpack-deps:emscripten-2
     default: "solbuildpackpusher/solidity-buildpack-deps@sha256:23dad3b34deae8107c8551804ef299f6a89c23ed506e8118fac151e2bdc9018c"
 
 orbs:
@@ -828,7 +829,7 @@ jobs:
           name: External GnosisSafe compilation
           command: |
             export COMPILE_ONLY=1
-            test/externalTests/gnosis.sh /tmp/workspace/soljson.js || test/externalTests/gnosis.sh /tmp/workspace/soljson.js
+            test/externalTests/gnosis.sh /tmp/workspace/soljson.js
 
   t_ems_test_ext_gnosis:
     docker:
@@ -859,7 +860,7 @@ jobs:
           name: External Zeppelin compilation
           command: |
             export COMPILE_ONLY=1
-            test/externalTests/zeppelin.sh /tmp/workspace/soljson.js || test/externalTests/zeppelin.sh /tmp/workspace/soljson.js
+            test/externalTests/zeppelin.sh /tmp/workspace/soljson.js
 
   t_ems_test_ext_zeppelin:
     docker:
@@ -894,7 +895,7 @@ jobs:
           name: External ColonyNetworks compilation
           command: |
             export COMPILE_ONLY=1
-            test/externalTests/colony.sh /tmp/workspace/soljson.js || test/externalTests/colony.sh /tmp/workspace/soljson.js
+            test/externalTests/colony.sh /tmp/workspace/soljson.js
 
   t_ems_test_ext_colony:
     docker:
@@ -916,6 +917,25 @@ jobs:
       - run: *gitter_notify_failure
       - run: *gitter_notify_success
 
+  t_ems_compile_ext_ens:
+    docker:
+      - image: circleci/node:10
+    environment:
+      TERM: xterm
+    steps:
+      - checkout
+      - attach_workspace:
+          at: /tmp/workspace
+      - run:
+          name: Install test dependencies
+          command: |
+            sudo apt-get -qy install lsof
+      - run:
+          name: External Ens compilation
+          command: |
+            export COMPILE_ONLY=1
+            test/externalTests/ens.sh /tmp/workspace/soljson.js
+
   b_win: &b_win
     executor:
       name: win/default
@@ -1100,6 +1120,7 @@ workflows:
       - t_ems_compile_ext_colony: *workflow_emscripten
       - t_ems_compile_ext_gnosis: *workflow_emscripten
       - t_ems_compile_ext_zeppelin: *workflow_emscripten
+      - t_ems_compile_ext_ens: *workflow_emscripten
 
       # Windows build and tests
       - b_win: *workflow_trigger_on_tags
diff --git a/.circleci/osx_install_dependencies.sh b/.circleci/osx_install_dependencies.sh
index 4041685b4..9050b05a0 100755
--- a/.circleci/osx_install_dependencies.sh
+++ b/.circleci/osx_install_dependencies.sh
@@ -57,7 +57,7 @@ then
   rm -f evmone-0.4.0-darwin-x86_64.tar.gz
 
   # hera
-  wget https://github.com/ewasm/hera/releases/download/v0.3.0/hera-0.3.0-darwin-x86_64.tar.gz
-  tar xzpf hera-0.3.0-darwin-x86_64.tar.gz -C /usr/local
-  rm -f hera-0.3.0-darwin-x86_64.tar.gz
+  wget https://github.com/ewasm/hera/releases/download/v0.3.2/hera-0.3.2-darwin-x86_64.tar.gz
+  tar xzpf hera-0.3.2-darwin-x86_64.tar.gz -C /usr/local
+  rm -f hera-0.3.2-darwin-x86_64.tar.gz
 fi
diff --git a/Changelog.md b/Changelog.md
index 7c0756e4f..ebb171632 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -33,7 +33,9 @@ AST Changes:
 
 Language Features:
  * Code generator: Support copying dynamically encoded structs from calldata to memory.
+ * Code generator: Support copying of nested arrays from calldata to memory.
  * The fallback function can now also have a single ``calldata`` argument (equaling ``msg.data``) and return ``bytes memory`` (which will not be ABI-encoded but returned as-is).
+ * Wasm backend: Add ``i32.select`` and ``i64.select`` instructions.
 
 Compiler Features:
  * Code Generator: Avoid memory allocation for default value if it is not used.
diff --git a/docs/types/reference-types.rst b/docs/types/reference-types.rst
index cedd2fd2a..b6a2bd3fb 100644
--- a/docs/types/reference-types.rst
+++ b/docs/types/reference-types.rst
@@ -549,3 +549,8 @@ members of the local variable actually write to the state.
 Of course, you can also directly access the members of the struct without
 assigning it to a local variable, as in
 ``campaigns[campaignID].amount = 0``.
+
+.. note::
+    Until Solidity 0.7.0, memory-structs containing members of storage-only types (e.g. mappings)
+    were allowed and assignments like ``campaigns[campaignID] = Campaign(beneficiary, goal, 0, 0)``
+    in the example above would work and just silently skip those members.
\ No newline at end of file
diff --git a/libsolidity/codegen/CompilerUtils.cpp b/libsolidity/codegen/CompilerUtils.cpp
index ca6441d0e..639641a2c 100644
--- a/libsolidity/codegen/CompilerUtils.cpp
+++ b/libsolidity/codegen/CompilerUtils.cpp
@@ -941,8 +941,8 @@ void CompilerUtils::convertType(
 	case Type::Category::Array:
 	{
 		solAssert(targetTypeCategory == stackTypeCategory, "");
-		ArrayType const& typeOnStack = dynamic_cast<ArrayType const&>(_typeOnStack);
-		ArrayType const& targetType = dynamic_cast<ArrayType const&>(_targetType);
+		auto const& typeOnStack = dynamic_cast<ArrayType const&>(_typeOnStack);
+		auto const& targetType = dynamic_cast<ArrayType const&>(_targetType);
 		switch (targetType.location())
 		{
 		case DataLocation::Storage:
@@ -958,65 +958,77 @@ void CompilerUtils::convertType(
 			// Copy the array to a free position in memory, unless it is already in memory.
 			if (typeOnStack.location() != DataLocation::Memory)
 			{
-				// stack: <source ref> (variably sized)
-				unsigned stackSize = typeOnStack.sizeOnStack();
-				ArrayUtils(m_context).retrieveLength(typeOnStack);
+				if (
+					typeOnStack.dataStoredIn(DataLocation::CallData) &&
+					typeOnStack.baseType()->isDynamicallyEncoded()
+				)
+				{
+					solAssert(m_context.useABICoderV2(), "");
+					// stack: offset length(optional in case of dynamically sized array)
+					solAssert(typeOnStack.sizeOnStack() == (typeOnStack.isDynamicallySized() ? 2 : 1), "");
+					if (typeOnStack.isDynamicallySized())
+						m_context << Instruction::SWAP1;
 
-				// allocate memory
-				// stack: <source ref> (variably sized) <length>
-				m_context << Instruction::DUP1;
-				ArrayUtils(m_context).convertLengthToSize(targetType, true);
-				// stack: <source ref> (variably sized) <length> <size>
-				if (targetType.isDynamicallySized())
-					m_context << u256(0x20) << Instruction::ADD;
-				allocateMemory();
-				// stack: <source ref> (variably sized) <length> <mem start>
-				m_context << Instruction::DUP1;
-				moveIntoStack(2 + stackSize);
-				if (targetType.isDynamicallySized())
-				{
-					m_context << Instruction::DUP2;
-					storeInMemoryDynamic(*TypeProvider::uint256());
-				}
-				// stack: <mem start> <source ref> (variably sized) <length> <mem data pos>
-				if (targetType.baseType()->isValueType())
-				{
-					copyToStackTop(2 + stackSize, stackSize);
-					ArrayUtils(m_context).copyArrayToMemory(typeOnStack);
+					m_context.callYulFunction(
+						m_context.utilFunctions().conversionFunction(typeOnStack, targetType),
+						typeOnStack.isDynamicallySized() ? 2 : 1,
+						1
+					);
 				}
 				else
 				{
-					if (auto baseType = dynamic_cast<ArrayType const*>(typeOnStack.baseType()))
-						solUnimplementedAssert(
-							typeOnStack.location() != DataLocation::CallData ||
-							!typeOnStack.isDynamicallyEncoded() ||
-							!baseType->isDynamicallySized(),
-							"Copying nested dynamic calldata arrays to memory is not implemented in the old code generator."
-						);
+					// stack: <source ref> (variably sized)
+					unsigned stackSize = typeOnStack.sizeOnStack();
+					ArrayUtils(m_context).retrieveLength(typeOnStack);
 
-					m_context << u256(0) << Instruction::SWAP1;
-					// stack: <mem start> <source ref> (variably sized) <length> <counter> <mem data pos>
-					auto repeat = m_context.newTag();
-					m_context << repeat;
-					m_context << Instruction::DUP3 << Instruction::DUP3;
-					m_context << Instruction::LT << Instruction::ISZERO;
-					auto loopEnd = m_context.appendConditionalJump();
-					copyToStackTop(3 + stackSize, stackSize);
-					copyToStackTop(2 + stackSize, 1);
-					ArrayUtils(m_context).accessIndex(typeOnStack, false);
-					if (typeOnStack.location() == DataLocation::Storage)
-						StorageItem(m_context, *typeOnStack.baseType()).retrieveValue(SourceLocation(), true);
-					convertType(*typeOnStack.baseType(), *targetType.baseType(), _cleanupNeeded);
-					storeInMemoryDynamic(*targetType.baseType(), true);
-					m_context << Instruction::SWAP1 << u256(1) << Instruction::ADD;
-					m_context << Instruction::SWAP1;
-					m_context.appendJumpTo(repeat);
-					m_context << loopEnd;
-					m_context << Instruction::POP;
+					// allocate memory
+					// stack: <source ref> (variably sized) <length>
+					m_context << Instruction::DUP1;
+					ArrayUtils(m_context).convertLengthToSize(targetType, true);
+					// stack: <source ref> (variably sized) <length> <size>
+					if (targetType.isDynamicallySized())
+						m_context << u256(0x20) << Instruction::ADD;
+					allocateMemory();
+					// stack: <source ref> (variably sized) <length> <mem start>
+					m_context << Instruction::DUP1;
+					moveIntoStack(2 + stackSize);
+					if (targetType.isDynamicallySized())
+					{
+						m_context << Instruction::DUP2;
+						storeInMemoryDynamic(*TypeProvider::uint256());
+					}
+					// stack: <mem start> <source ref> (variably sized) <length> <mem data pos>
+					if (targetType.baseType()->isValueType())
+					{
+						copyToStackTop(2 + stackSize, stackSize);
+						ArrayUtils(m_context).copyArrayToMemory(typeOnStack);
+					}
+					else
+					{
+						m_context << u256(0) << Instruction::SWAP1;
+						// stack: <mem start> <source ref> (variably sized) <length> <counter> <mem data pos>
+						auto repeat = m_context.newTag();
+						m_context << repeat;
+						m_context << Instruction::DUP3 << Instruction::DUP3;
+						m_context << Instruction::LT << Instruction::ISZERO;
+						auto loopEnd = m_context.appendConditionalJump();
+						copyToStackTop(3 + stackSize, stackSize);
+						copyToStackTop(2 + stackSize, 1);
+						ArrayUtils(m_context).accessIndex(typeOnStack, false);
+						if (typeOnStack.location() == DataLocation::Storage)
+							StorageItem(m_context, *typeOnStack.baseType()).retrieveValue(SourceLocation(), true);
+						convertType(*typeOnStack.baseType(), *targetType.baseType(), _cleanupNeeded);
+						storeInMemoryDynamic(*targetType.baseType(), true);
+						m_context << Instruction::SWAP1 << u256(1) << Instruction::ADD;
+						m_context << Instruction::SWAP1;
+						m_context.appendJumpTo(repeat);
+						m_context << loopEnd;
+						m_context << Instruction::POP;
+					}
+					// stack: <mem start> <source ref> (variably sized) <length> <mem data pos updated>
+					popStackSlots(2 + stackSize);
+					// Stack: <mem start>
 				}
-				// stack: <mem start> <source ref> (variably sized) <length> <mem data pos updated>
-				popStackSlots(2 + stackSize);
-				// Stack: <mem start>
 			}
 			break;
 		}
diff --git a/libsolidity/codegen/YulUtilFunctions.cpp b/libsolidity/codegen/YulUtilFunctions.cpp
index 5ce5d27a5..62e759632 100644
--- a/libsolidity/codegen/YulUtilFunctions.cpp
+++ b/libsolidity/codegen/YulUtilFunctions.cpp
@@ -1098,10 +1098,9 @@ string YulUtilFunctions::extractByteArrayLengthFunction()
 	});
 }
 
-std::string YulUtilFunctions::resizeDynamicArrayFunction(ArrayType const& _type)
+std::string YulUtilFunctions::resizeArrayFunction(ArrayType const& _type)
 {
 	solAssert(_type.location() == DataLocation::Storage, "");
-	solAssert(_type.isDynamicallySized(), "");
 	solUnimplementedAssert(_type.baseType()->storageBytes() <= 32, "...");
 
 	if (_type.isByteArray())
@@ -1117,8 +1116,10 @@ std::string YulUtilFunctions::resizeDynamicArrayFunction(ArrayType const& _type)
 
 				let oldLen := <fetchLength>(array)
 
-				// Store new length
-				sstore(array, newLen)
+				<?isDynamic>
+					// Store new length
+					sstore(array, newLen)
+				</isDynamic>
 
 				// Size was reduced, clear end of array
 				if lt(newLen, oldLen) {
@@ -1139,6 +1140,7 @@ std::string YulUtilFunctions::resizeDynamicArrayFunction(ArrayType const& _type)
 			("functionName", functionName)
 			("panic", panicFunction(PanicCode::ResourceError))
 			("fetchLength", arrayLengthFunction(_type))
+			("isDynamic", _type.isDynamicallySized())
 			("convertToSize", arrayConvertLengthToSize(_type))
 			("dataPosition", arrayDataAreaFunction(_type))
 			("clearStorageRange", clearStorageRangeFunction(*_type.baseType()))
@@ -1523,7 +1525,7 @@ string YulUtilFunctions::clearStorageArrayFunction(ArrayType const& _type)
 		)")
 		("functionName", functionName)
 		("dynamic", _type.isDynamicallySized())
-		("resizeArray", _type.isDynamicallySized() ? resizeDynamicArrayFunction(_type) : "")
+		("resizeArray", _type.isDynamicallySized() ? resizeArrayFunction(_type) : "")
 		(
 			"clearRange",
 			clearStorageRangeFunction(
@@ -1595,6 +1597,9 @@ string YulUtilFunctions::copyArrayToStorageFunction(ArrayType const& _fromType,
 		*_fromType.copyForLocation(_toType.location(), _toType.isPointer()) == dynamic_cast<ReferenceType const&>(_toType),
 		""
 	);
+	if (!_toType.isDynamicallySized())
+		solAssert(!_fromType.isDynamicallySized() && _fromType.length() <= _toType.length(), "");
+
 	if (_fromType.isByteArray())
 		return copyByteArrayToStorageFunction(_fromType, _toType);
 	if (_fromType.dataStoredIn(DataLocation::Storage) && _toType.baseType()->isValueType())
@@ -1606,9 +1611,8 @@ string YulUtilFunctions::copyArrayToStorageFunction(ArrayType const& _fromType,
 			function <functionName>(slot, value<?isFromDynamicCalldata>, len</isFromDynamicCalldata>) {
 				<?fromStorage> if eq(slot, value) { leave } </fromStorage>
 				let length := <arrayLength>(value<?isFromDynamicCalldata>, len</isFromDynamicCalldata>)
-				<?isToDynamic>
-					<resizeArray>(slot, length)
-				</isToDynamic>
+
+				<resizeArray>(slot, length)
 
 				let srcPtr := <srcDataLocation>(value)
 
@@ -1662,7 +1666,6 @@ string YulUtilFunctions::copyArrayToStorageFunction(ArrayType const& _fromType,
 		bool fromMemory = _fromType.dataStoredIn(DataLocation::Memory);
 		templ("fromMemory", fromMemory);
 		templ("fromCalldata", fromCalldata);
-		templ("isToDynamic", _toType.isDynamicallySized());
 		templ("srcDataLocation", arrayDataAreaFunction(_fromType));
 		if (fromCalldata)
 		{
@@ -1671,8 +1674,7 @@ string YulUtilFunctions::copyArrayToStorageFunction(ArrayType const& _fromType,
 			if (_fromType.baseType()->isDynamicallyEncoded())
 				templ("accessCalldataTail", accessCalldataTailFunction(*_fromType.baseType()));
 		}
-		if (_toType.isDynamicallySized())
-			templ("resizeArray", resizeDynamicArrayFunction(_toType));
+		templ("resizeArray", resizeArrayFunction(_toType));
 		templ("arrayLength",arrayLengthFunction(_fromType));
 		templ("isValueType", _fromType.baseType()->isValueType());
 		templ("dstDataLocation", arrayDataAreaFunction(_toType));
@@ -1791,6 +1793,8 @@ string YulUtilFunctions::copyValueArrayStorageToStorageFunction(ArrayType const&
 	solAssert(_fromType.dataStoredIn(DataLocation::Storage) && _toType.baseType()->isValueType(), "");
 	solAssert(_toType.dataStoredIn(DataLocation::Storage), "");
 
+	solUnimplementedAssert(_fromType.storageStride() == _toType.storageStride(), "");
+
 	string functionName = "copy_array_to_storage_from_" + _fromType.identifier() + "_to_" + _toType.identifier();
 	return m_functionCollector.createFunction(functionName, [&](){
 		Whiskers templ(R"(
@@ -1799,9 +1803,7 @@ string YulUtilFunctions::copyValueArrayStorageToStorageFunction(ArrayType const&
 				let length := <arrayLength>(src)
 				// Make sure array length is sane
 				if gt(length, 0xffffffffffffffff) { <panic>() }
-				<?isToDynamic>
-					<resizeArray>(dst, length)
-				</isToDynamic>
+				<resizeArray>(dst, length)
 
 				let srcPtr := <srcDataLocation>(src)
 
@@ -1821,9 +1823,7 @@ string YulUtilFunctions::copyValueArrayStorageToStorageFunction(ArrayType const&
 		if (_fromType.dataStoredIn(DataLocation::Storage))
 			solAssert(!_fromType.isValueType(), "");
 		templ("functionName", functionName);
-		templ("isToDynamic", _toType.isDynamicallySized());
-		if (_toType.isDynamicallySized())
-			templ("resizeArray", resizeDynamicArrayFunction(_toType));
+		templ("resizeArray", resizeArrayFunction(_toType));
 		templ("arrayLength",arrayLengthFunction(_fromType));
 		templ("panic", panicFunction(PanicCode::ResourceError));
 		templ("srcDataLocation", arrayDataAreaFunction(_fromType));
diff --git a/libsolidity/codegen/YulUtilFunctions.h b/libsolidity/codegen/YulUtilFunctions.h
index 6ce30a452..3b38ba8cd 100644
--- a/libsolidity/codegen/YulUtilFunctions.h
+++ b/libsolidity/codegen/YulUtilFunctions.h
@@ -194,8 +194,9 @@ public:
 	std::string extractByteArrayLengthFunction();
 
 	/// @returns the name of a function that resizes a storage array
+	/// for statically sized arrays, it will just clean-up elements of array starting from newLen until the end
 	/// signature: (array, newLen)
-	std::string resizeDynamicArrayFunction(ArrayType const& _type);
+	std::string resizeArrayFunction(ArrayType const& _type);
 
 	/// @returns the name of a function that reduces the size of a storage array by one element
 	/// signature: (array)
diff --git a/libsolidity/codegen/ir/IRGenerator.cpp b/libsolidity/codegen/ir/IRGenerator.cpp
index c518c7763..c9487c646 100644
--- a/libsolidity/codegen/ir/IRGenerator.cpp
+++ b/libsolidity/codegen/ir/IRGenerator.cpp
@@ -249,6 +249,7 @@ string IRGenerator::generateFunction(FunctionDefinition const& _function)
 {
 	string functionName = IRNames::function(_function);
 	return m_context.functionCollector().createFunction(functionName, [&]() {
+		solUnimplementedAssert(_function.modifiers().empty(), "Modifiers not implemented yet.");
 		Whiskers t(R"(
 			function <functionName>(<params>)<?+retParams> -> <retParams></+retParams> {
 				<initReturnVariables>
@@ -521,8 +522,16 @@ void IRGenerator::generateImplicitConstructors(ContractDefinition const& _contra
 			)");
 			vector<string> params;
 			if (contract->constructor())
+			{
+				for (auto const& modifierInvocation: contract->constructor()->modifiers())
+					// This can be ContractDefinition too for super arguments. That is supported.
+					solUnimplementedAssert(
+						!dynamic_cast<ModifierDefinition const*>(modifierInvocation->name().annotation().referencedDeclaration),
+						"Modifiers not implemented yet."
+					);
 				for (ASTPointer<VariableDeclaration> const& varDecl: contract->constructor()->parameters())
 					params += m_context.addLocalVariable(*varDecl).stackSlots();
+			}
 			t("params", joinHumanReadable(params));
 			vector<string> baseParams = listAllParams(baseConstructorParams);
 			t("baseParams", joinHumanReadable(baseParams));
diff --git a/libsolidity/codegen/ir/IRGeneratorForStatements.cpp b/libsolidity/codegen/ir/IRGeneratorForStatements.cpp
index 6cd5f3c30..8b2b8e65b 100644
--- a/libsolidity/codegen/ir/IRGeneratorForStatements.cpp
+++ b/libsolidity/codegen/ir/IRGeneratorForStatements.cpp
@@ -712,10 +712,16 @@ void IRGeneratorForStatements::endVisit(UnaryOperation const& _unaryOperation)
 		else
 			solUnimplementedAssert(false, "Unary operator not yet implemented");
 	}
+	else if (resultType.category() == Type::Category::FixedBytes)
+	{
+		solAssert(op == Token::BitNot, "Only bitwise negation is allowed for FixedBytes");
+		solAssert(resultType == type(_unaryOperation.subExpression()), "Result type doesn't match!");
+		appendSimpleUnaryOperation(_unaryOperation, _unaryOperation.subExpression());
+	}
 	else if (resultType.category() == Type::Category::Bool)
 	{
 		solAssert(
-			_unaryOperation.getOperator() != Token::BitNot,
+			op != Token::BitNot,
 			"Bitwise Negation can't be done on bool!"
 		);
 
@@ -1794,6 +1800,11 @@ void IRGeneratorForStatements::endVisit(MemberAccess const& _memberAccess)
 					", " <<
 					offset <<
 					")\n";
+			else if (
+				dynamic_cast<ArrayType const*>(_memberAccess.annotation().type) ||
+				dynamic_cast<StructType const*>(_memberAccess.annotation().type)
+			)
+				define(_memberAccess) << offset << "\n";
 			else
 				define(_memberAccess) <<
 					m_utils.readFromCalldata(*_memberAccess.annotation().type) <<
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index ec10b44de..de80dd996 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -162,6 +162,7 @@ void BMC::endVisit(FunctionDefinition const& _function)
 		smtutil::Expression constraints = m_context.assertions();
 		checkVerificationTargets(constraints);
 		m_verificationTargets.clear();
+		m_pathConditions.clear();
 	}
 
 	SMTEncoder::endVisit(_function);
@@ -184,7 +185,26 @@ bool BMC::visit(IfStatement const& _node)
 		);
 	m_context.popSolver();
 
-	SMTEncoder::visit(_node);
+	_node.condition().accept(*this);
+	auto conditionExpr = expr(_node.condition());
+	// visit true branch
+	auto [indicesEndTrue, trueEndPathCondition] = visitBranch(&_node.trueStatement(), conditionExpr);
+	auto touchedVars = touchedVariables(_node.trueStatement());
+
+	// visit false branch
+	decltype(indicesEndTrue) indicesEndFalse;
+	auto falseEndPathCondition = currentPathConditions() && !conditionExpr;
+	if (_node.falseStatement())
+	{
+		std::tie(indicesEndFalse, falseEndPathCondition) = visitBranch(_node.falseStatement(), !conditionExpr);
+		touchedVars += touchedVariables(*_node.falseStatement());
+	}
+	else
+		indicesEndFalse = copyVariableIndices();
+
+	// merge the information from branches
+	setPathCondition(trueEndPathCondition || falseEndPathCondition);
+	mergeVariables(touchedVars, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
 
 	return false;
 }
@@ -224,7 +244,7 @@ bool BMC::visit(WhileStatement const& _node)
 	decltype(indicesBeforeLoop) indicesAfterLoop;
 	if (_node.isDoWhile())
 	{
-		indicesAfterLoop = visitBranch(&_node.body());
+		indicesAfterLoop = visitBranch(&_node.body()).first;
 		// TODO the assertions generated in the body should still be active in the condition
 		_node.condition().accept(*this);
 		if (isRootFunction())
@@ -244,7 +264,7 @@ bool BMC::visit(WhileStatement const& _node)
 				&_node.condition()
 			);
 
-		indicesAfterLoop = visitBranch(&_node.body(), expr(_node.condition()));
+		indicesAfterLoop = visitBranch(&_node.body(), expr(_node.condition())).first;
 	}
 
 	// We reset the execution to before the loop
@@ -406,6 +426,12 @@ void BMC::endVisit(FunctionCall const& _funCall)
 	}
 }
 
+void BMC::endVisit(Return const& _return)
+{
+	SMTEncoder::endVisit(_return);
+	setPathCondition(smtutil::Expression(false));
+}
+
 /// Visitor helpers.
 
 void BMC::visitAssert(FunctionCall const& _funCall)
@@ -467,7 +493,9 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 		// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
 		// is that there we don't have `_funCall`.
 		pushCallStack({funDef, &_funCall});
+		pushPathCondition(currentPathConditions());
 		funDef->accept(*this);
+		popPathCondition();
 	}
 
 	createReturnedExpressions(_funCall);
@@ -968,3 +996,14 @@ smtutil::CheckResult BMC::checkSatisfiable()
 	return checkSatisfiableAndGenerateModel({}).first;
 }
 
+void BMC::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value)
+{
+	auto oldVar = _symVar.currentValue();
+	auto newVar = _symVar.increaseIndex();
+	m_context.addAssertion(smtutil::Expression::ite(
+		currentPathConditions(),
+		newVar == _value,
+		newVar == oldVar
+	));
+}
+
diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h
index d55ce7666..3bdd0caa9 100644
--- a/libsolidity/formal/BMC.h
+++ b/libsolidity/formal/BMC.h
@@ -90,6 +90,7 @@ private:
 	bool visit(ForStatement const& _node) override;
 	void endVisit(UnaryOperation const& _node) override;
 	void endVisit(FunctionCall const& _node) override;
+	void endVisit(Return const& _node) override;
 	//@}
 
 	/// Visitor helpers.
@@ -97,6 +98,7 @@ private:
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
 	void visitAddMulMod(FunctionCall const& _funCall) override;
+	void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value) override;
 	/// Visits the FunctionDefinition of the called function
 	/// if available and inlines the return value.
 	void inlineFunctionCall(FunctionCall const& _funCall);
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index ae5c92845..d977e16f3 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -155,8 +155,10 @@ void SMTEncoder::visitFunctionOrModifier()
 
 	if (m_modifierDepthStack.back() == static_cast<int>(function.modifiers().size()))
 	{
+		pushPathCondition(currentPathConditions());
 		if (function.isImplemented())
 			function.body().accept(*this);
+		popPathCondition();
 	}
 	else
 	{
@@ -193,6 +195,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
 	initializeFunctionCallParameters(*_definition, args);
 
 	pushCallStack({_definition, _invocation});
+	pushPathCondition(currentPathConditions());
 	if (auto modifier = dynamic_cast<ModifierDefinition const*>(_definition))
 	{
 		if (modifier->isImplemented())
@@ -205,6 +208,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
 			function->accept(*this);
 		// Functions are popped from the callstack in endVisit(FunctionDefinition)
 	}
+	popPathCondition();
 }
 
 void SMTEncoder::inlineConstructorHierarchy(ContractDefinition const& _contract)
@@ -288,26 +292,6 @@ bool SMTEncoder::visit(TryCatchClause const& _clause)
 	return false;
 }
 
-bool SMTEncoder::visit(IfStatement const& _node)
-{
-	_node.condition().accept(*this);
-
-	auto indicesEndTrue = visitBranch(&_node.trueStatement(), expr(_node.condition()));
-	auto touchedVars = touchedVariables(_node.trueStatement());
-	decltype(indicesEndTrue) indicesEndFalse;
-	if (_node.falseStatement())
-	{
-		indicesEndFalse = visitBranch(_node.falseStatement(), !expr(_node.condition()));
-		touchedVars += touchedVariables(*_node.falseStatement());
-	}
-	else
-		indicesEndFalse = copyVariableIndices();
-
-	mergeVariables(touchedVars, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
-
-	return false;
-}
-
 void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
 {
 	if (_varDecl.declarations().size() != 1)
@@ -598,10 +582,10 @@ bool SMTEncoder::visit(Conditional const& _op)
 {
 	_op.condition().accept(*this);
 
-	auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition()));
+	auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition())).first;
 	auto touchedVars = touchedVariables(_op.trueExpression());
 
-	auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition()));
+	auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition())).first;
 	touchedVars += touchedVariables(_op.falseExpression());
 
 	mergeVariables(touchedVars, expr(_op.condition()), indicesEndTrue, indicesEndFalse);
@@ -1749,13 +1733,13 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op)
 		_op.leftExpression().accept(*this);
 		if (_op.getOperator() == Token::And)
 		{
-			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression()));
+			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first;
 			mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 			defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
 		}
 		else
 		{
-			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression()));
+			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first;
 			mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 			defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
 		}
@@ -1969,22 +1953,29 @@ void SMTEncoder::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression
 	m_context.addAssertion(_symVar.increaseIndex() == _value);
 }
 
-SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression _condition)
+pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
+	ASTNode const* _statement,
+	smtutil::Expression _condition
+)
 {
 	return visitBranch(_statement, &_condition);
 }
 
-SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition)
+pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
+	ASTNode const* _statement,
+	smtutil::Expression const* _condition
+)
 {
 	auto indicesBeforeBranch = copyVariableIndices();
 	if (_condition)
 		pushPathCondition(*_condition);
 	_statement->accept(*this);
+	auto pathConditionOnExit = currentPathConditions();
 	if (_condition)
 		popPathCondition();
 	auto indicesAfterBranch = copyVariableIndices();
 	resetVariableIndices(indicesBeforeBranch);
-	return indicesAfterBranch;
+	return {indicesAfterBranch, pathConditionOnExit};
 }
 
 void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smtutil::Expression> const& _callArgs)
@@ -2240,6 +2231,14 @@ void SMTEncoder::pushPathCondition(smtutil::Expression const& _e)
 	m_pathConditions.push_back(currentPathConditions() && _e);
 }
 
+void SMTEncoder::setPathCondition(smtutil::Expression const& _e)
+{
+	if (m_pathConditions.empty())
+		m_pathConditions.push_back(_e);
+	else
+		m_pathConditions.back() = _e;
+}
+
 smtutil::Expression SMTEncoder::currentPathConditions()
 {
 	if (m_pathConditions.empty())
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 8dffc2682..4c26cb4c8 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -89,7 +89,7 @@ protected:
 	bool visit(FunctionDefinition const& _node) override;
 	void endVisit(FunctionDefinition const& _node) override;
 	bool visit(PlaceholderStatement const& _node) override;
-	bool visit(IfStatement const& _node) override;
+	bool visit(IfStatement const&) override { return false; }
 	bool visit(WhileStatement const&) override { return false; }
 	bool visit(ForStatement const&) override { return false; }
 	void endVisit(VariableDeclarationStatement const& _node) override;
@@ -197,7 +197,7 @@ protected:
 
 	/// Handles the actual assertion of the new value to the encoding context.
 	/// Other assignment methods should use this one in the end.
-	void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value);
+	virtual void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value);
 
 	void assignment(VariableDeclaration const& _variable, Expression const& _value);
 	/// Handles assignments to variables of different types.
@@ -219,9 +219,10 @@ protected:
 
 	/// Visits the branch given by the statement, pushes and pops the current path conditions.
 	/// @param _condition if present, asserts that this condition is true within the branch.
-	/// @returns the variable indices after visiting the branch.
-	VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition = nullptr);
-	VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression _condition);
+	/// @returns the variable indices after visiting the branch and the expression representing
+	/// the path condition at the end of the branch.
+	std::pair<VariableIndices, smtutil::Expression> visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition = nullptr);
+	std::pair<VariableIndices, smtutil::Expression> visitBranch(ASTNode const* _statement, smtutil::Expression _condition);
 
 	using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
 
@@ -263,6 +264,8 @@ protected:
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smtutil::Expression _value);
 
+	/// Overwrites the current path condition
+	void setPathCondition(smtutil::Expression const& _e);
 	/// Adds a new path condition
 	void pushPathCondition(smtutil::Expression const& _e);
 	/// Remove the last path condition
diff --git a/libyul/backends/wasm/BinaryTransform.cpp b/libyul/backends/wasm/BinaryTransform.cpp
index a36742750..df700527e 100644
--- a/libyul/backends/wasm/BinaryTransform.cpp
+++ b/libyul/backends/wasm/BinaryTransform.cpp
@@ -156,6 +156,8 @@ Opcode constOpcodeFor(ValueType _type)
 }
 
 static map<string, uint8_t> const builtins = {
+	{"i32.select", 0x1b},
+	{"i64.select", 0x1b},
 	{"i32.load", 0x28},
 	{"i64.load", 0x29},
 	{"i32.load8_s", 0x2c},
diff --git a/libyul/backends/wasm/WasmDialect.cpp b/libyul/backends/wasm/WasmDialect.cpp
index 1c7755d6a..1e77e1d47 100644
--- a/libyul/backends/wasm/WasmDialect.cpp
+++ b/libyul/backends/wasm/WasmDialect.cpp
@@ -120,6 +120,10 @@ WasmDialect::WasmDialect()
 	addFunction("i32.drop", {i32}, {});
 	addFunction("i64.drop", {i64}, {});
 
+	// Select is also overloaded.
+	addFunction("i32.select", {i32, i32, i32}, {i32});
+	addFunction("i64.select", {i64, i64, i32}, {i64});
+
 	addFunction("nop", {}, {});
 	addFunction("unreachable", {}, {}, false);
 	m_functions["unreachable"_yulstring].sideEffects.storage = SideEffects::None;
diff --git a/libyul/backends/wasm/polyfill/Arithmetic.yul b/libyul/backends/wasm/polyfill/Arithmetic.yul
index 4a0e32bf3..7a4a80f5f 100644
--- a/libyul/backends/wasm/polyfill/Arithmetic.yul
+++ b/libyul/backends/wasm/polyfill/Arithmetic.yul
@@ -90,9 +90,9 @@ function mul_64x64_128(x, y) -> hi, lo {
 // value split into four 64 bit values.
 function mul_128x128_256(x1, x2, y1, y2) -> r1, r2, r3, r4 {
 	let ah, al := mul_64x64_128(x1, y1)
-	let     bh, bl := mul_64x64_128(x1, y2)
-	let     ch, cl := mul_64x64_128(x2, y1)
-	let         dh, dl := mul_64x64_128(x2, y2)
+	let bh, bl := mul_64x64_128(x1, y2)
+	let ch, cl := mul_64x64_128(x2, y1)
+	let dh, dl := mul_64x64_128(x2, y2)
 	r4 := dl
 	let carry1, carry2
 	let t1, t2
diff --git a/libyul/backends/wasm/polyfill/Comparison.yul b/libyul/backends/wasm/polyfill/Comparison.yul
index 6f08c5b18..dc052a145 100644
--- a/libyul/backends/wasm/polyfill/Comparison.yul
+++ b/libyul/backends/wasm/polyfill/Comparison.yul
@@ -35,24 +35,23 @@ function iszero512(x1, x2, x3, x4, x5, x6, x7, x8) -> r:i32 {
 }
 
 function eq(x1, x2, x3, x4, y1, y2, y3, y4) -> r1, r2, r3, r4 {
-	if i64.eq(x1, y1) {
-		if i64.eq(x2, y2) {
-			if i64.eq(x3, y3) {
-				if i64.eq(x4, y4) {
-					r4 := 1
-				}
-			}
-		}
-	}
+	r4 := i64.extend_i32_u(
+		i32.and(
+			i64.eq(x1, y1),
+			i32.and(
+				i64.eq(x2, y2),
+				i32.and(
+					i64.eq(x3, y3),
+					i64.eq(x4, y4)
+				)
+			)
+		)
+	)
 }
 
 // returns 0 if a == b, -1 if a < b and 1 if a > b
 function cmp(a, b) -> r:i32 {
-	switch i64.lt_u(a, b)
-	case 1:i32 { r := 0xffffffff:i32 }
-	default {
-		r := i64.ne(a, b)
-	}
+	r := i32.select(0xffffffff:i32, i64.ne(a, b), i64.lt_u(a, b))
 }
 
 function lt_320x320_64(x1, x2, x3, x4, x5, y1, y2, y3, y4, y5) -> z:i32 {
diff --git a/libyul/optimiser/CommonSubexpressionEliminator.cpp b/libyul/optimiser/CommonSubexpressionEliminator.cpp
index 2f80e7bc4..6a739618c 100644
--- a/libyul/optimiser/CommonSubexpressionEliminator.cpp
+++ b/libyul/optimiser/CommonSubexpressionEliminator.cpp
@@ -103,9 +103,9 @@ void CommonSubexpressionEliminator::visit(Expression& _e)
 		for (auto const& [variable, value]: m_value)
 		{
 			assertThrow(value.value, OptimizerException, "");
-			assertThrow(inScope(variable), OptimizerException, "");
 			if (SyntacticallyEqual{}(_e, *value.value))
 			{
+				assertThrow(inScope(variable), OptimizerException, "");
 				_e = Identifier{locationOf(_e), variable};
 				break;
 			}
diff --git a/libyul/optimiser/DataFlowAnalyzer.cpp b/libyul/optimiser/DataFlowAnalyzer.cpp
index 6755500b3..97cdd2062 100644
--- a/libyul/optimiser/DataFlowAnalyzer.cpp
+++ b/libyul/optimiser/DataFlowAnalyzer.cpp
@@ -82,7 +82,7 @@ void DataFlowAnalyzer::operator()(Assignment& _assignment)
 	assertThrow(_assignment.value, OptimizerException, "");
 	clearKnowledgeIfInvalidated(*_assignment.value);
 	visit(*_assignment.value);
-	handleAssignment(names, _assignment.value.get());
+	handleAssignment(names, _assignment.value.get(), false);
 }
 
 void DataFlowAnalyzer::operator()(VariableDeclaration& _varDecl)
@@ -98,7 +98,7 @@ void DataFlowAnalyzer::operator()(VariableDeclaration& _varDecl)
 		visit(*_varDecl.value);
 	}
 
-	handleAssignment(names, _varDecl.value.get());
+	handleAssignment(names, _varDecl.value.get(), true);
 }
 
 void DataFlowAnalyzer::operator()(If& _if)
@@ -161,7 +161,7 @@ void DataFlowAnalyzer::operator()(FunctionDefinition& _fun)
 	for (auto const& var: _fun.returnVariables)
 	{
 		m_variableScopes.back().variables.emplace(var.name);
-		handleAssignment({var.name}, nullptr);
+		handleAssignment({var.name}, nullptr, true);
 	}
 	ASTModifier::operator()(_fun);
 
@@ -220,9 +220,10 @@ void DataFlowAnalyzer::operator()(Block& _block)
 	assertThrow(numScopes == m_variableScopes.size(), OptimizerException, "");
 }
 
-void DataFlowAnalyzer::handleAssignment(set<YulString> const& _variables, Expression* _value)
+void DataFlowAnalyzer::handleAssignment(set<YulString> const& _variables, Expression* _value, bool _isDeclaration)
 {
-	clearValues(_variables);
+	if (!_isDeclaration)
+		clearValues(_variables);
 
 	MovableChecker movableChecker{m_dialect, &m_functionSideEffects};
 	if (_value)
@@ -244,14 +245,17 @@ void DataFlowAnalyzer::handleAssignment(set<YulString> const& _variables, Expres
 	for (auto const& name: _variables)
 	{
 		m_references.set(name, referencedVariables);
-		// assignment to slot denoted by "name"
-		m_storage.eraseKey(name);
-		// assignment to slot contents denoted by "name"
-		m_storage.eraseValue(name);
-		// assignment to slot denoted by "name"
-		m_memory.eraseKey(name);
-		// assignment to slot contents denoted by "name"
-		m_memory.eraseValue(name);
+		if (!_isDeclaration)
+		{
+			// assignment to slot denoted by "name"
+			m_storage.eraseKey(name);
+			// assignment to slot contents denoted by "name"
+			m_storage.eraseValue(name);
+			// assignment to slot denoted by "name"
+			m_memory.eraseKey(name);
+			// assignment to slot contents denoted by "name"
+			m_memory.eraseValue(name);
+		}
 	}
 
 	if (_value && _variables.size() == 1)
diff --git a/libyul/optimiser/DataFlowAnalyzer.h b/libyul/optimiser/DataFlowAnalyzer.h
index 237b48597..e5d868246 100644
--- a/libyul/optimiser/DataFlowAnalyzer.h
+++ b/libyul/optimiser/DataFlowAnalyzer.h
@@ -107,7 +107,7 @@ public:
 
 protected:
 	/// Registers the assignment.
-	void handleAssignment(std::set<YulString> const& _names, Expression* _value);
+	void handleAssignment(std::set<YulString> const& _names, Expression* _value, bool _isDeclaration);
 
 	/// Creates a new inner scope.
 	void pushScope(bool _functionScope);
diff --git a/libyul/optimiser/Suite.cpp b/libyul/optimiser/Suite.cpp
index f07a16c83..af9c93715 100644
--- a/libyul/optimiser/Suite.cpp
+++ b/libyul/optimiser/Suite.cpp
@@ -364,6 +364,9 @@ void OptimiserSuite::runSequenceUntilStable(
 	size_t maxRounds
 )
 {
+	if (_steps.empty())
+		return;
+
 	size_t codeSize = 0;
 	for (size_t rounds = 0; rounds < maxRounds; ++rounds)
 	{
diff --git a/scripts/ci/docker_upgrade.sh b/scripts/ci/docker_upgrade.sh
index 16d622230..29e80354a 100755
--- a/scripts/ci/docker_upgrade.sh
+++ b/scripts/ci/docker_upgrade.sh
@@ -61,5 +61,5 @@ docker push "${DOCKER_IMAGE_ID}-${VERSION}"
 
 REPO_DIGEST=$(docker inspect --format='{{.RepoDigests}}' "${DOCKER_IMAGE_ID}-${VERSION}")
 
-echo "::set-env name=DOCKER_IMAGE::${DOCKER_IMAGE_ID}-${VERSION}"
-echo "::set-env name=DOCKER_REPO_DIGEST::${REPO_DIGEST}"
+echo "DOCKER_IMAGE=${DOCKER_IMAGE_ID}-${VERSION}" >> "$GITHUB_ENV"
+echo "DOCKER_REPO_DIGEST=${REPO_DIGEST}" >> "$GITHUB_ENV"
diff --git a/scripts/docker/buildpack-deps/Dockerfile.ubuntu1604.clang.ossfuzz b/scripts/docker/buildpack-deps/Dockerfile.ubuntu1604.clang.ossfuzz
index 7cdf26cb1..787b33c03 100644
--- a/scripts/docker/buildpack-deps/Dockerfile.ubuntu1604.clang.ossfuzz
+++ b/scripts/docker/buildpack-deps/Dockerfile.ubuntu1604.clang.ossfuzz
@@ -22,7 +22,7 @@
 # (c) 2016-2019 solidity contributors.
 #------------------------------------------------------------------------------
 FROM gcr.io/oss-fuzz-base/base-clang as base
-LABEL version="5"
+LABEL version="6"
 
 ARG DEBIAN_FRONTEND=noninteractive
 
@@ -104,7 +104,7 @@ RUN set -ex; \
 # HERA
 RUN set -ex; \
 	cd /usr/src; \
-	git clone --branch="v0.3.0" --recurse-submodules https://github.com/ewasm/hera.git; \
+	git clone --branch="v0.3.2" --depth 1 --recurse-submodules https://github.com/ewasm/hera.git; \
 	cd hera; \
 	mkdir build; \
 	cd build; \
diff --git a/scripts/docker/buildpack-deps/Dockerfile.ubuntu1804 b/scripts/docker/buildpack-deps/Dockerfile.ubuntu1804
index 65750a62d..ca6eed20e 100644
--- a/scripts/docker/buildpack-deps/Dockerfile.ubuntu1804
+++ b/scripts/docker/buildpack-deps/Dockerfile.ubuntu1804
@@ -22,7 +22,7 @@
 # (c) 2016-2019 solidity contributors.
 #------------------------------------------------------------------------------
 FROM buildpack-deps:bionic AS base
-LABEL version="3"
+LABEL version="4"
 
 ARG DEBIAN_FRONTEND=noninteractive
 
@@ -84,20 +84,20 @@ RUN set -ex; \
 	EVMONE_VERSION="$EVMONE_MAJOR.$EVMONE_MINOR.$EVMONE_MICRO"; \
 	TGZFILE="evmone-$EVMONE_VERSION-linux-x86_64.tar.gz"; \
 	wget https://github.com/ethereum/evmone/releases/download/v$EVMONE_VERSION/$TGZFILE; \
-	sha256sum $TGZFILE; \
+	sha256sum $TGZFILE | grep ${EVMONE_HASH}; \
 	tar xzpf $TGZFILE -C /usr; \
 	rm -f $TGZFILE;
 
 # HERA
-ARG HERA_HASH="622663cb3bc1fa07213c6e1fe8070c5c259096e75039a46d014b2a3448b5cf44"
+ARG HERA_HASH="1a0b3cf626910c969f0ac86b7a731969a2e5b8254bc4e626b8f3a60471481f03"
 ARG HERA_MAJOR="0"
 ARG HERA_MINOR="3"
-ARG HERA_MICRO="0"
+ARG HERA_MICRO="2"
 RUN set -ex; \
 	HERA_VERSION="$HERA_MAJOR.$HERA_MINOR.$HERA_MICRO"; \
 	TGZFILE="hera-$HERA_VERSION-linux-x86_64.tar.gz"; \
 	wget https://github.com/ewasm/hera/releases/download/v$HERA_VERSION/$TGZFILE; \
-	sha256sum $TGZFILE; \
+	sha256sum $TGZFILE | grep ${HERA_HASH}; \
 	tar xzpf $TGZFILE -C /usr; \
 	rm -f $TGZFILE;
 
diff --git a/scripts/docker/buildpack-deps/Dockerfile.ubuntu2004 b/scripts/docker/buildpack-deps/Dockerfile.ubuntu2004
index 6614ff6e7..505f4b585 100644
--- a/scripts/docker/buildpack-deps/Dockerfile.ubuntu2004
+++ b/scripts/docker/buildpack-deps/Dockerfile.ubuntu2004
@@ -22,7 +22,7 @@
 # (c) 2016-2019 solidity contributors.
 #------------------------------------------------------------------------------
 FROM buildpack-deps:focal AS base
-LABEL version="3"
+LABEL version="4"
 
 ARG DEBIAN_FRONTEND=noninteractive
 
@@ -60,7 +60,7 @@ RUN set -ex; \
 # HERA
 RUN set -ex; \
 	cd /usr/src; \
-	git clone --branch="v0.3.0" --recurse-submodules https://github.com/ewasm/hera.git; \
+	git clone --branch="v0.3.2" --depth 1 --recurse-submodules https://github.com/ewasm/hera.git; \
 	cd hera; \
 	mkdir build; \
 	cd build; \
diff --git a/scripts/docker/buildpack-deps/Dockerfile.ubuntu2004.clang b/scripts/docker/buildpack-deps/Dockerfile.ubuntu2004.clang
index 88314b5a6..4968c148c 100644
--- a/scripts/docker/buildpack-deps/Dockerfile.ubuntu2004.clang
+++ b/scripts/docker/buildpack-deps/Dockerfile.ubuntu2004.clang
@@ -22,7 +22,7 @@
 # (c) 2016-2019 solidity contributors.
 #------------------------------------------------------------------------------
 FROM buildpack-deps:focal AS base
-LABEL version="3"
+LABEL version="4"
 
 ARG DEBIAN_FRONTEND=noninteractive
 
@@ -62,7 +62,7 @@ RUN set -ex; \
 # HERA
 RUN set -ex; \
 	cd /usr/src; \
-	git clone --branch="v0.3.0" --recurse-submodules https://github.com/ewasm/hera.git; \
+	git clone --branch="v0.3.2" --depth 1 --recurse-submodules https://github.com/ewasm/hera.git; \
 	cd hera; \
 	mkdir build; \
 	cd build; \
diff --git a/test/Common.h b/test/Common.h
index a665d563f..e745ac6ac 100644
--- a/test/Common.h
+++ b/test/Common.h
@@ -34,17 +34,17 @@ namespace solidity::test
 static constexpr auto evmoneFilename = "evmone.dll";
 static constexpr auto evmoneDownloadLink = "https://github.com/ethereum/evmone/releases/download/v0.4.1/evmone-0.4.1-windows-amd64.zip";
 static constexpr auto heraFilename = "hera.dll";
-static constexpr auto heraDownloadLink = "https://github.com/ewasm/hera/archive/v0.3.0.tar.gz";
+static constexpr auto heraDownloadLink = "https://github.com/ewasm/hera/archive/v0.3.2.tar.gz";
 #elif defined(__APPLE__)
 static constexpr auto evmoneFilename = "libevmone.dylib";
 static constexpr auto evmoneDownloadLink = "https://github.com/ethereum/evmone/releases/download/v0.4.1/evmone-0.4.1-darwin-x86_64.tar.gz";
 static constexpr auto heraFilename = "libhera.dylib";
-static constexpr auto heraDownloadLink = "https://github.com/ewasm/hera/releases/download/v0.3.0/hera-0.3.0-darwin-x86_64.tar.gz";
+static constexpr auto heraDownloadLink = "https://github.com/ewasm/hera/releases/download/v0.3.2/hera-0.3.2-darwin-x86_64.tar.gz";
 #else
 static constexpr auto evmoneFilename = "libevmone.so";
 static constexpr auto evmoneDownloadLink = "https://github.com/ethereum/evmone/releases/download/v0.4.1/evmone-0.4.1-linux-x86_64.tar.gz";
 static constexpr auto heraFilename = "libhera.so";
-static constexpr auto heraDownloadLink = "https://github.com/ewasm/hera/releases/download/v0.3.0/hera-0.3.0-linux-x86_64.tar.gz";
+static constexpr auto heraDownloadLink = "https://github.com/ewasm/hera/releases/download/v0.3.2/hera-0.3.2-linux-x86_64.tar.gz";
 #endif
 
 struct ConfigException : public util::Exception {};
diff --git a/test/cmdlineTests/evm_to_wasm_break/output b/test/cmdlineTests/evm_to_wasm_break/output
index 8346f3c42..2a70119d9 100644
--- a/test/cmdlineTests/evm_to_wasm_break/output
+++ b/test/cmdlineTests/evm_to_wasm_break/output
@@ -31,10 +31,9 @@ object "object" {
             let x_6 := x_2
             let x_7 := x_3
             let _2 := 1
-            let _3 := i64.or(_1, _1)
-            let _4:i32 := i32.eqz(i32.eqz(i64.eqz(i64.or(_3, i64.or(_1, _2)))))
+            let _3:i32 := i32.eqz(i32.eqz(i64.eqz(i64.or(i64.or(_1, _1), i64.or(_1, _2)))))
             for { }
-            i32.eqz(_4)
+            i32.eqz(_3)
             {
                 let x_8, x_9, x_10, x_11 := add(x_4, x_5, x_6, x_7, _1, _1, _1, _2)
                 x_4 := x_8
@@ -43,10 +42,12 @@ object "object" {
                 x_7 := x_11
             }
             {
-                let _5, _6, _7, _8 := iszero_197_919_1528(_1, _1, _1, lt_199(x_4, x_5, x_6, x_7, _1, _1, _1, 10))
-                if i32.eqz(i64.eqz(i64.or(i64.or(_5, _6), i64.or(_7, _8)))) { break }
-                if i32.eqz(i64.eqz(i64.or(_3, i64.or(_1, eq(x_4, x_5, x_6, x_7, _1, _1, _1, 2))))) { break }
-                if i32.eqz(i64.eqz(i64.or(_3, i64.or(_1, eq(x_4, x_5, x_6, x_7, _1, _1, _1, 4))))) { continue }
+                let _4, _5, _6, _7 := iszero_200_872_1499(_1, _1, _1, lt_202(x_4, x_5, x_6, x_7, _1, _1, _1, 10))
+                if i32.eqz(i64.eqz(i64.or(i64.or(_4, _5), i64.or(_6, _7)))) { break }
+                let _8, _9, _10, _11 := eq_201_873_1500(x_4, x_5, x_6, x_7, _1, _1, _1, 2)
+                if i32.eqz(i64.eqz(i64.or(i64.or(_8, _9), i64.or(_10, _11)))) { break }
+                let _12, _13, _14, _15 := eq_201_873_1500(x_4, x_5, x_6, x_7, _1, _1, _1, 4)
+                if i32.eqz(i64.eqz(i64.or(i64.or(_12, _13), i64.or(_14, _15)))) { continue }
             }
             sstore(_1, _1, _1, _1, x_4, x_5, x_6, x_7)
         }
@@ -67,34 +68,23 @@ object "object" {
             let r1_1, carry_2 := add_carry(x1, y1, carry_1)
             r1 := r1_1
         }
-        function iszero_197_919_1528(x1, x2, x3, x4) -> r1, r2, r3, r4
+        function iszero_200_872_1499(x1, x2, x3, x4) -> r1, r2, r3, r4
         {
             r4 := i64.extend_i32_u(i64.eqz(i64.or(i64.or(x1, x2), i64.or(x3, x4))))
         }
-        function eq(x1, x2, x3, x4, y1, y2, y3, y4) -> r4
+        function eq_201_873_1500(x1, x2, x3, x4, y1, y2, y3, y4) -> r1, r2, r3, r4
         {
-            if i64.eq(x1, y1)
-            {
-                if i64.eq(x2, y2)
-                {
-                    if i64.eq(x3, y3) { if i64.eq(x4, y4) { r4 := 1 } }
-                }
-            }
+            r4 := i64.extend_i32_u(i32.and(i64.eq(x1, y1), i32.and(i64.eq(x2, y2), i32.and(i64.eq(x3, y3), i64.eq(x4, y4)))))
         }
-        function cmp(a, b) -> r:i32
-        {
-            switch i64.lt_u(a, b)
-            case 1:i32 { r := 0xffffffff:i32 }
-            default { r := i64.ne(a, b) }
-        }
-        function lt_199(x1, x2, x3, x4, y1, y2, y3, y4) -> z4
+        function lt_202(x1, x2, x3, x4, y1, y2, y3, y4) -> z4
         {
             let z:i32 := false
-            switch cmp(x1, y1)
+            let _1:i32 := 0xffffffff:i32
+            switch i32.select(_1, i64.ne(x1, y1), i64.lt_u(x1, y1))
             case 0:i32 {
-                switch cmp(x2, y2)
+                switch i32.select(_1, i64.ne(x2, y2), i64.lt_u(x2, y2))
                 case 0:i32 {
-                    switch cmp(x3, y3)
+                    switch i32.select(_1, i64.ne(x3, y3), i64.lt_u(x3, y3))
                     case 0:i32 { z := i64.lt_u(x4, y4) }
                     case 1:i32 { z := 0:i32 }
                     default { z := 1:i32 }
@@ -178,7 +168,7 @@ object "object" {
 
 
 Binary representation:
-0061736d0100000001540c6000006000017f60017e017e60027e7e017f60037e7e7e017e60047e7e7e7e017e60047e7e7e7e017f60087e7e7e7e7e7e7e7e0060087e7e7e7e7e7e7e7e017e60057f7e7e7e7e0060027f7f0060037f7f7f00025e0408657468657265756d0c73746f7261676553746f7265000a08657468657265756d06726576657274000a08657468657265756d0f67657443616c6c4461746153697a65000108657468657265756d0c63616c6c44617461436f7079000b030f0e000408050803080602020205090705030100010610037e0142000b7e0142000b7e0142000b071102066d656d6f72790200046d61696e00040aa1090ea302030b7e017f087e02404200210002402000200020002000100f21012300210223012103230221040b20012105200221062003210720042108420121092000200084210a200a200020098484504545210b02400340200b45450d01024002402000200020002005200620072008200020002000420a100a1007210c2300210d2301210e2302210f0b200c200d84200e200f8484504504400c030b200a20002005200620072008200020002000420210088484504504400c030b200a20002005200620072008200020002000420410088484504504400c010b0b024020052006200720082000200020002009100621102300211123012112230221130b201021052011210620122107201321080c000b0b2000200020002000200520062007200810110b0b2901037e0240200020017c2105200520027c21032005200054200320055472ad21040b2004240020030b6c010b7e0240200320077c210c200c42007c210b024020022006200c200354200b200c5472ad1005210d2300210e0b200d210a024020012005200e1005210f230021100b200f2109024020002004201010052111230021120b201121080b20092400200a2401200b240220080b2401047e0240200020018420022003848450ad21070b20052400200624012007240220040b2d01017e024020002004510440200120055104402002200651044020032007510440420121080b0b0b0b0b20080b2701027f024002402000200154210320034101460440417f210205200020015221020b0b0b20020b8a0102017e047f0240410021090240200020041009210a200a41004604400240200120051009210b200b41004604400240200220061009210c200c41004604402003200754210905200c41014604404100210905410121090b0b0b05200b41014604404100210905410121090b0b0b05200a41014604404100210905410121090b0b0b2009ad21080b20080b2901017f024042002000200184200284520440000b42002003422088520440000b2003a721040b20040b1f01017e024020004208864280fe0383200042088842ff01838421010b20010b1e01027e02402000100c421086210220022000421088100c8421010b20010b1e01027e02402000100d422086210220022000422088100d8421010b20010bfc0105047e017f017e087f047e024010022108420021092009200920092009100b210a2000200120022003100b210b2009200920094220100b210c200b417f200c6b4b04404100410010010b2008200b6b210d200b20084b04404100210d0b4100210e200d200e4b0440200a200b200d10030b200c200d4b0440200c200d6b210f200a200d6a2110200e2111024003402011200f49450d010240201020116a200e3a00000b201141016a21110c000b0b0b200e290000100e2112200e41086a290000100e2113200e41106a290000100e2114200e41186a290000100e2115201221042013210520142106201521070b20052400200624012007240220040b3200024020002001100e370000200041086a2002100e370000200041106a2003100e370000200041186a2004100e3700000b0b230002404100200020012002200310104120200420052006200710104100412010000b0b
+0061736d01000000014e0b6000006000017f60017e017e60037e7e7e017e60047e7e7e7e017e60047e7e7e7e017f60087e7e7e7e7e7e7e7e0060087e7e7e7e7e7e7e7e017e60057f7e7e7e7e0060027f7f0060037f7f7f00025e0408657468657265756d0c73746f7261676553746f7265000908657468657265756d06726576657274000908657468657265756d0f67657443616c6c4461746153697a65000108657468657265756d0c63616c6c44617461436f7079000a030e0d0003070407070502020204080605030100010610037e0142000b7e0142000b7e0142000b071102066d656d6f72790200046d61696e00040abc090dcb02030a7e017f107e02404200210002402000200020002000100e21012300210223012103230221040b20012105200221062003210720042108420121092000200084200020098484504545210a02400340200a45450d01024002402000200020002005200620072008200020002000420a10091007210b2300210c2301210d2302210e0b200b200c84200d200e8484504504400c030b0240200520062007200820002000200042021008210f2300211023012111230221120b200f201084201120128484504504400c030b024020052006200720082000200020004204100821132300211423012115230221160b2013201484201520168484504504400c010b0b0240200520062007200820002000200020091006211723002118230121192302211a0b201721052018210620192107201a21080c000b0b2000200020002000200520062007200810100b0b2901037e0240200020017c2105200520027c21032005200054200320055472ad21040b2004240020030b6c010b7e0240200320077c210c200c42007c210b024020022006200c200354200b200c5472ad1005210d2300210e0b200d210a024020012005200e1005210f230021100b200f2109024020002004201010052111230021120b201121080b20092400200a2401200b240220080b2401047e0240200020018420022003848450ad21070b20052400200624012007240220040b2f01047e02402000200451200120055120022006512003200751717171ad210b0b20092400200a2401200b240220080ba30102017e057f024041002109417f210a0240200a200020045220002004541b210b200b41004604400240200a200120055220012005541b210c200c41004604400240200a200220065220022006541b210d200d41004604402003200754210905200d41014604404100210905410121090b0b0b05200c41014604404100210905410121090b0b0b05200b41014604404100210905410121090b0b0b2009ad21080b20080b2901017f024042002000200184200284520440000b42002003422088520440000b2003a721040b20040b1f01017e024020004208864280fe0383200042088842ff01838421010b20010b1e01027e02402000100b421086210220022000421088100b8421010b20010b1e01027e02402000100c422086210220022000422088100c8421010b20010bfc0105047e017f017e087f047e024010022108420021092009200920092009100a210a2000200120022003100a210b2009200920094220100a210c200b417f200c6b4b04404100410010010b2008200b6b210d200b20084b04404100210d0b4100210e200d200e4b0440200a200b200d10030b200c200d4b0440200c200d6b210f200a200d6a2110200e2111024003402011200f49450d010240201020116a200e3a00000b201141016a21110c000b0b0b200e290000100d2112200e41086a290000100d2113200e41106a290000100d2114200e41186a290000100d2115201221042013210520142106201521070b20052400200624012007240220040b3200024020002001100d370000200041086a2002100d370000200041106a2003100d370000200041186a2004100d3700000b0b2300024041002000200120022003100f41202004200520062007100f4100412010000b0b
 
 Text representation:
 (module
@@ -203,12 +193,19 @@ Text representation:
     (local $x_6 i64)
     (local $x_7 i64)
     (local $_2 i64)
-    (local $_3 i64)
-    (local $_4 i32)
+    (local $_3 i32)
+    (local $_4 i64)
     (local $_5 i64)
     (local $_6 i64)
     (local $_7 i64)
     (local $_8 i64)
+    (local $_9 i64)
+    (local $_10 i64)
+    (local $_11 i64)
+    (local $_12 i64)
+    (local $_13 i64)
+    (local $_14 i64)
+    (local $_15 i64)
     (local $x_8 i64)
     (local $x_9 i64)
     (local $x_10 i64)
@@ -227,26 +224,39 @@ Text representation:
         (local.set $x_6 (local.get $x_2))
         (local.set $x_7 (local.get $x_3))
         (local.set $_2 (i64.const 1))
-        (local.set $_3 (i64.or (local.get $_1) (local.get $_1)))
-        (local.set $_4 (i32.eqz (i32.eqz (i64.eqz (i64.or (local.get $_3) (i64.or (local.get $_1) (local.get $_2)))))))
+        (local.set $_3 (i32.eqz (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_1) (local.get $_1)) (i64.or (local.get $_1) (local.get $_2)))))))
         (block $label__3
             (loop $label__5
-                (br_if $label__3 (i32.eqz (i32.eqz (local.get $_4))))
+                (br_if $label__3 (i32.eqz (i32.eqz (local.get $_3))))
                 (block $label__4
                     (block
-                        (local.set $_5 (call $iszero_197_919_1528 (local.get $_1) (local.get $_1) (local.get $_1) (call $lt_199 (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 10))))
-                        (local.set $_6 (global.get $global_))
-                        (local.set $_7 (global.get $global__1))
-                        (local.set $_8 (global.get $global__2))
+                        (local.set $_4 (call $iszero_200_872_1499 (local.get $_1) (local.get $_1) (local.get $_1) (call $lt_202 (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 10))))
+                        (local.set $_5 (global.get $global_))
+                        (local.set $_6 (global.get $global__1))
+                        (local.set $_7 (global.get $global__2))
 
                     )
-                    (if (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_5) (local.get $_6)) (i64.or (local.get $_7) (local.get $_8))))) (then
+                    (if (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_4) (local.get $_5)) (i64.or (local.get $_6) (local.get $_7))))) (then
                         (br $label__3)
                     ))
-                    (if (i32.eqz (i64.eqz (i64.or (local.get $_3) (i64.or (local.get $_1) (call $eq (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 2)))))) (then
+                    (block
+                        (local.set $_8 (call $eq_201_873_1500 (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 2)))
+                        (local.set $_9 (global.get $global_))
+                        (local.set $_10 (global.get $global__1))
+                        (local.set $_11 (global.get $global__2))
+
+                    )
+                    (if (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_8) (local.get $_9)) (i64.or (local.get $_10) (local.get $_11))))) (then
                         (br $label__3)
                     ))
-                    (if (i32.eqz (i64.eqz (i64.or (local.get $_3) (i64.or (local.get $_1) (call $eq (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 4)))))) (then
+                    (block
+                        (local.set $_12 (call $eq_201_873_1500 (local.get $x_4) (local.get $x_5) (local.get $x_6) (local.get $x_7) (local.get $_1) (local.get $_1) (local.get $_1) (i64.const 4)))
+                        (local.set $_13 (global.get $global_))
+                        (local.set $_14 (global.get $global__1))
+                        (local.set $_15 (global.get $global__2))
+
+                    )
+                    (if (i32.eqz (i64.eqz (i64.or (i64.or (local.get $_12) (local.get $_13)) (i64.or (local.get $_14) (local.get $_15))))) (then
                         (br $label__4)
                     ))
 
@@ -338,7 +348,7 @@ Text representation:
     (local.get $r1)
 )
 
-(func $iszero_197_919_1528
+(func $iszero_200_872_1499
     (param $x1 i64)
     (param $x2 i64)
     (param $x3 i64)
@@ -358,7 +368,7 @@ Text representation:
     (local.get $r1)
 )
 
-(func $eq
+(func $eq_201_873_1500
     (param $x1 i64)
     (param $x2 i64)
     (param $x3 i64)
@@ -368,44 +378,21 @@ Text representation:
     (param $y3 i64)
     (param $y4 i64)
     (result i64)
+    (local $r1 i64)
+    (local $r2 i64)
+    (local $r3 i64)
     (local $r4 i64)
     (block $label__9
-        (if (i64.eq (local.get $x1) (local.get $y1)) (then
-            (if (i64.eq (local.get $x2) (local.get $y2)) (then
-                (if (i64.eq (local.get $x3) (local.get $y3)) (then
-                    (if (i64.eq (local.get $x4) (local.get $y4)) (then
-                        (local.set $r4 (i64.const 1))
-                    ))
-                ))
-            ))
-        ))
+        (local.set $r4 (i64.extend_i32_u (i32.and (i64.eq (local.get $x1) (local.get $y1)) (i32.and (i64.eq (local.get $x2) (local.get $y2)) (i32.and (i64.eq (local.get $x3) (local.get $y3)) (i64.eq (local.get $x4) (local.get $y4)))))))
 
     )
-    (local.get $r4)
+    (global.set $global_ (local.get $r2))
+    (global.set $global__1 (local.get $r3))
+    (global.set $global__2 (local.get $r4))
+    (local.get $r1)
 )
 
-(func $cmp
-    (param $a i64)
-    (param $b i64)
-    (result i32)
-    (local $r i32)
-    (local $condition i32)
-    (block $label__10
-        (block
-            (local.set $condition (i64.lt_u (local.get $a) (local.get $b)))
-            (if (i32.eq (local.get $condition) (i32.const 1)) (then
-                (local.set $r (i32.const 4294967295))
-            )(else
-                (local.set $r (i64.ne (local.get $a) (local.get $b)))
-            ))
-
-        )
-
-    )
-    (local.get $r)
-)
-
-(func $lt_199
+(func $lt_202
     (param $x1 i64)
     (param $x2 i64)
     (param $x3 i64)
@@ -417,23 +404,25 @@ Text representation:
     (result i64)
     (local $z4 i64)
     (local $z i32)
+    (local $_1 i32)
+    (local $condition i32)
+    (local $condition_11 i32)
     (local $condition_12 i32)
-    (local $condition_13 i32)
-    (local $condition_14 i32)
-    (block $label__11
+    (block $label__10
         (local.set $z (i32.const 0))
+        (local.set $_1 (i32.const 4294967295))
         (block
-            (local.set $condition_12 (call $cmp (local.get $x1) (local.get $y1)))
-            (if (i32.eq (local.get $condition_12) (i32.const 0)) (then
+            (local.set $condition (i32.select (local.get $_1) (i64.ne (local.get $x1) (local.get $y1)) (i64.lt_u (local.get $x1) (local.get $y1))))
+            (if (i32.eq (local.get $condition) (i32.const 0)) (then
                 (block
-                    (local.set $condition_13 (call $cmp (local.get $x2) (local.get $y2)))
-                    (if (i32.eq (local.get $condition_13) (i32.const 0)) (then
+                    (local.set $condition_11 (i32.select (local.get $_1) (i64.ne (local.get $x2) (local.get $y2)) (i64.lt_u (local.get $x2) (local.get $y2))))
+                    (if (i32.eq (local.get $condition_11) (i32.const 0)) (then
                         (block
-                            (local.set $condition_14 (call $cmp (local.get $x3) (local.get $y3)))
-                            (if (i32.eq (local.get $condition_14) (i32.const 0)) (then
+                            (local.set $condition_12 (i32.select (local.get $_1) (i64.ne (local.get $x3) (local.get $y3)) (i64.lt_u (local.get $x3) (local.get $y3))))
+                            (if (i32.eq (local.get $condition_12) (i32.const 0)) (then
                                 (local.set $z (i64.lt_u (local.get $x4) (local.get $y4)))
                             )(else
-                                (if (i32.eq (local.get $condition_14) (i32.const 1)) (then
+                                (if (i32.eq (local.get $condition_12) (i32.const 1)) (then
                                     (local.set $z (i32.const 0))
                                 )(else
                                     (local.set $z (i32.const 1))
@@ -442,7 +431,7 @@ Text representation:
 
                         )
                     )(else
-                        (if (i32.eq (local.get $condition_13) (i32.const 1)) (then
+                        (if (i32.eq (local.get $condition_11) (i32.const 1)) (then
                             (local.set $z (i32.const 0))
                         )(else
                             (local.set $z (i32.const 1))
@@ -451,7 +440,7 @@ Text representation:
 
                 )
             )(else
-                (if (i32.eq (local.get $condition_12) (i32.const 1)) (then
+                (if (i32.eq (local.get $condition) (i32.const 1)) (then
                     (local.set $z (i32.const 0))
                 )(else
                     (local.set $z (i32.const 1))
@@ -472,7 +461,7 @@ Text representation:
     (param $x4 i64)
     (result i32)
     (local $v i32)
-    (block $label__15
+    (block $label__13
         (if (i64.ne (i64.const 0) (i64.or (i64.or (local.get $x1) (local.get $x2)) (local.get $x3))) (then
             (unreachable)))
         (if (i64.ne (i64.const 0) (i64.shr_u (local.get $x4) (i64.const 32))) (then
@@ -487,7 +476,7 @@ Text representation:
     (param $x i64)
     (result i64)
     (local $y i64)
-    (block $label__16
+    (block $label__14
         (local.set $y (i64.or (i64.and (i64.shl (local.get $x) (i64.const 8)) (i64.const 65280)) (i64.and (i64.shr_u (local.get $x) (i64.const 8)) (i64.const 255))))
 
     )
@@ -499,7 +488,7 @@ Text representation:
     (result i64)
     (local $y i64)
     (local $hi i64)
-    (block $label__17
+    (block $label__15
         (local.set $hi (i64.shl (call $bswap16 (local.get $x)) (i64.const 16)))
         (local.set $y (i64.or (local.get $hi) (call $bswap16 (i64.shr_u (local.get $x) (i64.const 16)))))
 
@@ -512,7 +501,7 @@ Text representation:
     (result i64)
     (local $y i64)
     (local $hi i64)
-    (block $label__18
+    (block $label__16
         (local.set $hi (i64.shl (call $bswap32 (local.get $x)) (i64.const 32)))
         (local.set $y (i64.or (local.get $hi) (call $bswap32 (i64.shr_u (local.get $x) (i64.const 32)))))
 
@@ -544,7 +533,7 @@ Text representation:
     (local $z2_1 i64)
     (local $z3_1 i64)
     (local $z4_1 i64)
-    (block $label__19
+    (block $label__17
         (local.set $cds (call $eth.getCallDataSize))
         (local.set $_1 (i64.const 0))
         (local.set $destination (call $u256_to_i32 (local.get $_1) (local.get $_1) (local.get $_1) (local.get $_1)))
@@ -563,14 +552,14 @@ Text representation:
             (local.set $_3 (i32.sub (local.get $requested_size) (local.get $available_size)))
             (local.set $_4 (i32.add (local.get $destination) (local.get $available_size)))
             (local.set $i (local.get $_2))
-            (block $label__20
-                (loop $label__22
-                    (br_if $label__20 (i32.eqz (i32.lt_u (local.get $i) (local.get $_3))))
-                    (block $label__21
+            (block $label__18
+                (loop $label__20
+                    (br_if $label__18 (i32.eqz (i32.lt_u (local.get $i) (local.get $_3))))
+                    (block $label__19
                         (i32.store8 (i32.add (local.get $_4) (local.get $i)) (local.get $_2))
                     )
                     (local.set $i (i32.add (local.get $i) (i32.const 1)))
-                    (br $label__22)
+                    (br $label__20)
                 )
 
             )
@@ -597,7 +586,7 @@ Text representation:
     (param $y2 i64)
     (param $y3 i64)
     (param $y4 i64)
-    (block $label__23
+    (block $label__21
         (i64.store (local.get $pos) (call $bswap64 (local.get $y1)))
         (i64.store (i32.add (local.get $pos) (i32.const 8)) (call $bswap64 (local.get $y2)))
         (i64.store (i32.add (local.get $pos) (i32.const 16)) (call $bswap64 (local.get $y3)))
@@ -614,7 +603,7 @@ Text representation:
     (param $y2 i64)
     (param $y3 i64)
     (param $y4 i64)
-    (block $label__24
+    (block $label__22
         (call $mstore_internal (i32.const 0) (local.get $x1) (local.get $x2) (local.get $x3) (local.get $x4))
         (call $mstore_internal (i32.const 32) (local.get $y1) (local.get $y2) (local.get $y3) (local.get $y4))
         (call $eth.storageStore (i32.const 0) (i32.const 32))
diff --git a/test/cmdlineTests/standard_model_checker_engine_bmc/output.json b/test/cmdlineTests/standard_model_checker_engine_bmc/output.json
index 63a21eb4e..8840c2477 100644
--- a/test/cmdlineTests/standard_model_checker_engine_bmc/output.json
+++ b/test/cmdlineTests/standard_model_checker_engine_bmc/output.json
@@ -1,4 +1,4 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x8b2c3058077c75f8fff85d2d387198b91b4e591448624f4bef0ab6c7b87d5ec1":"(set-option :produce-models true)
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x238aade411d63d50406236089e28f3770d51f95888222fdb838f930911e0f763":"(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -15,7 +15,7 @@
 (declare-fun |expr_9_0| () Int)
 (declare-fun |expr_10_1| () Bool)
 
-(assert (and (and true (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (= expr_9_0 0) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))) (not expr_10_1)))
+(assert (and (and (and true true) (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (= expr_9_0 0) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))) (not expr_10_1)))
 (declare-const |EVALEXPR_0| Int)
 (assert (= |EVALEXPR_0| x_4_0))
 (check-sat)
diff --git a/test/cmdlineTests/standard_model_checker_timeout_all/output.json b/test/cmdlineTests/standard_model_checker_timeout_all/output.json
index e055cb70b..1f9d232fe 100644
--- a/test/cmdlineTests/standard_model_checker_timeout_all/output.json
+++ b/test/cmdlineTests/standard_model_checker_timeout_all/output.json
@@ -1,4 +1,4 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x0ab92bf00d2546a23d94ff3a406d009299b43650e321d35e02531726df040b9d":"(set-option :produce-models true)
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x0d6f843ef6990bfad1918be96d1aad42b5d7ca87a171d0ac34009e0d4b6e8e03":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -26,9 +26,9 @@
 (declare-fun |expr_21_0| () Int)
 (declare-fun |expr_22_1| () Bool)
 
-(assert (and (and true (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1))
+(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1))
 (check-sat)
-","0x34467f46a484d40c850f05c3b05b0817a859573bc546982aeab4a17f9259fb5b":"(set-option :produce-models true)
+","0x3091365cefd5a713eea87735305ab53c75303343ebf74b77d3578ae0b73c64a2":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -49,9 +49,99 @@
 (declare-fun |expr_13_0| () Int)
 (declare-fun |expr_14_1| () Bool)
 
-(assert (and (and true (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1)))
+(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1)))
 (check-sat)
-","0x3dd3d755e279cd0bf414fd3fd9830517ee2397e3931ec76a9fd970b5eec46384":"(set-option :produce-models true)
+","0x6b268fc2d87ebda3f3b3b93c8d0b2b5374fd3bd33387113b9ee138a85c142dae":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_15_0| () Int)
+(declare-fun |r_div_mod_15_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+(declare-fun |expr_26_0| () Int)
+(declare-fun |expr_27_0| () Int)
+(declare-fun |d_div_mod_16_0| () Int)
+(declare-fun |r_div_mod_16_0| () Int)
+(declare-fun |expr_28_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1))
+(check-sat)
+","0xa81ce8317a79fc74d85d9edfe56caf9b0274a7da4556bfb418652051e0bfa679":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1))
+(check-sat)
+","0xaec7aba847ba235b585e4c7e6ec8d8eee964e76bd40a02e00af3354acede95d8":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_15_0| () Int)
+(declare-fun |r_div_mod_15_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1)))
+(check-sat)
+","0xe6aad7b5a7ba681908e47e11921c93815f9a4cdd90ef82dd79a60fcac94492c9":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -102,7 +192,7 @@
 (declare-fun |expr_45_0| () Int)
 (declare-fun |expr_46_1| () Bool)
 
-(assert (and (and true (and (= expr_46_1 (= expr_44_1 expr_45_0)) (and (= expr_45_0 0) (and (= expr_44_1 (ite (= expr_43_0 0) 0 r_div_mod_18_0)) (and (and (<= 0 r_div_mod_18_0) (or (= expr_43_0 0) (< r_div_mod_18_0 expr_43_0))) (and (= (+ (* d_div_mod_18_0 expr_43_0) r_div_mod_18_0) expr_42_0) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (= r_34_1 expr_39_1) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_17_0)) (and (and (<= 0 r_div_mod_17_0) (or (= expr_38_0 0) (< r_div_mod_17_0 expr_38_0))) (and (= (+ (* d_div_mod_17_0 expr_38_0) r_div_mod_17_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies true expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))))))))))))))))))) (not expr_46_1)))
+(assert (and (and (and true true) (and (= expr_46_1 (= expr_44_1 expr_45_0)) (and (= expr_45_0 0) (and (= expr_44_1 (ite (= expr_43_0 0) 0 r_div_mod_18_0)) (and (and (<= 0 r_div_mod_18_0) (or (= expr_43_0 0) (< r_div_mod_18_0 expr_43_0))) (and (= (+ (* d_div_mod_18_0 expr_43_0) r_div_mod_18_0) expr_42_0) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (ite (and true true) (= r_34_1 expr_39_1) (= r_34_1 r_34_0)) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_17_0)) (and (and (<= 0 r_div_mod_17_0) (or (= expr_38_0 0) (< r_div_mod_17_0 expr_38_0))) (and (= (+ (* d_div_mod_17_0 expr_38_0) r_div_mod_17_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))))))))))))))))))) (not expr_46_1)))
 (declare-const |EVALEXPR_0| Int)
 (assert (= |EVALEXPR_0| x_4_0))
 (declare-const |EVALEXPR_1| Int)
@@ -113,7 +203,7 @@
 (assert (= |EVALEXPR_3| r_34_1))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| ))
-","0x4b82600501b4619c19bf57eb8d3cdb69f1c0d2a807d5908f1503d07e65ce2fd6":"(set-option :produce-models true)
+","0xf877f10b1dc480ae2403c9376947f543da579bf3aff7dfaa2f946e300b81d305":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -148,97 +238,7 @@
 (declare-fun |expr_29_0| () Int)
 (declare-fun |expr_30_1| () Bool)
 
-(assert (and (and true (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1))
-(check-sat)
-","0x5d4ad2f9c711b9e187dba2577e849272617d56d0ba3d46427baa3c11804a9143":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(set-logic ALL)
-(declare-fun |error_0| () Int)
-(declare-fun |this_0| () Int)
-(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
-(declare-fun |state_0| () |state_type|)
-(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
-(declare-fun |tx_0| () |tx_type|)
-(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
-(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
-(declare-fun |crypto_0| () |crypto_type|)
-(declare-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_15_0| () Int)
-(declare-fun |r_div_mod_15_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-
-(assert (and (and true (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1)))
-(check-sat)
-","0xd63dd6c8c7f21f7200de074c7131ab703fcb783425bc609ee7541efc2fc320bf":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(set-logic ALL)
-(declare-fun |error_0| () Int)
-(declare-fun |this_0| () Int)
-(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
-(declare-fun |state_0| () |state_type|)
-(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
-(declare-fun |tx_0| () |tx_type|)
-(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
-(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
-(declare-fun |crypto_0| () |crypto_type|)
-(declare-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_15_0| () Int)
-(declare-fun |r_div_mod_15_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-(declare-fun |expr_26_0| () Int)
-(declare-fun |expr_27_0| () Int)
-(declare-fun |d_div_mod_16_0| () Int)
-(declare-fun |r_div_mod_16_0| () Int)
-(declare-fun |expr_28_1| () Int)
-(declare-fun |expr_29_0| () Int)
-(declare-fun |expr_30_1| () Bool)
-
-(assert (and (and true (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1)))
-(check-sat)
-","0xee7d96e23195f6aeb74a805122639dcd6a8932788ceeae3cba711aba9050a0b7":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(set-logic ALL)
-(declare-fun |error_0| () Int)
-(declare-fun |this_0| () Int)
-(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
-(declare-fun |state_0| () |state_type|)
-(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
-(declare-fun |tx_0| () |tx_type|)
-(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
-(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
-(declare-fun |crypto_0| () |crypto_type|)
-(declare-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-
-(assert (and (and true (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1))
+(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1)))
 (check-sat)
 "}},"errors":[{"component":"general","errorCode":"6328","formattedMessage":"A:6:85: Warning: CHC: Assertion violation might happen here.
 require(k > 0); require(x % k == 0); require(y % k == 0); uint r = mulmod(x, y, k); assert(r % k == 0);}}
diff --git a/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json b/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json
index b1db514d4..e59ff2f82 100644
--- a/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json
+++ b/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json
@@ -1,78 +1,4 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x0f5149c7799751d1575c0946ca73f9a1a9dbc6c432db3c5e13625bd301d7fd37":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(set-logic ALL)
-(declare-fun |error_0| () Int)
-(declare-fun |this_0| () Int)
-(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
-(declare-fun |state_0| () |state_type|)
-(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
-(declare-fun |tx_0| () |tx_type|)
-(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
-(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
-(declare-fun |crypto_0| () |crypto_type|)
-(declare-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-(declare-fun |expr_26_0| () Int)
-(declare-fun |expr_27_0| () Int)
-(declare-fun |d_div_mod_1_0| () Int)
-(declare-fun |r_div_mod_1_0| () Int)
-(declare-fun |expr_28_1| () Int)
-(declare-fun |expr_29_0| () Int)
-(declare-fun |expr_30_1| () Bool)
-
-(assert (and (and true (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1))
-(check-sat)
-","0x11444b207b7d8827f8b7503cad8aed1426a8727290a070d1eed04a55e85e2f14":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(set-logic ALL)
-(declare-fun |error_0| () Int)
-(declare-fun |this_0| () Int)
-(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
-(declare-fun |state_0| () |state_type|)
-(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
-(declare-fun |tx_0| () |tx_type|)
-(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
-(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
-(declare-fun |crypto_0| () |crypto_type|)
-(declare-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-(declare-fun |expr_26_0| () Int)
-(declare-fun |expr_27_0| () Int)
-(declare-fun |d_div_mod_1_0| () Int)
-(declare-fun |r_div_mod_1_0| () Int)
-(declare-fun |expr_28_1| () Int)
-(declare-fun |expr_29_0| () Int)
-(declare-fun |expr_30_1| () Bool)
-
-(assert (and (and true (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1)))
-(check-sat)
-","0x317d72a016f7a5ff016cda82e96601cfac3a0498f393852410c7ce335d4896c8":"(set-option :produce-models true)
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x0e2ec6d70e3de7ac14f07c9bbb08f9436e3b832ae8456d340e4d4a8b8712c7f5":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -123,280 +49,7 @@
 (declare-fun |expr_45_0| () Int)
 (declare-fun |expr_46_1| () Bool)
 
-(assert (and (and true (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (= r_34_1 expr_39_1) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_2_0)) (and (and (<= 0 r_div_mod_2_0) (or (= expr_38_0 0) (< r_div_mod_2_0 expr_38_0))) (and (= (+ (* d_div_mod_2_0 expr_38_0) r_div_mod_2_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies true expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))))))))))))))))))) (= expr_43_0 0)))
-(declare-const |EVALEXPR_0| Int)
-(assert (= |EVALEXPR_0| x_4_0))
-(declare-const |EVALEXPR_1| Int)
-(assert (= |EVALEXPR_1| y_6_0))
-(declare-const |EVALEXPR_2| Int)
-(assert (= |EVALEXPR_2| k_8_0))
-(declare-const |EVALEXPR_3| Int)
-(assert (= |EVALEXPR_3| r_34_1))
-(declare-const |EVALEXPR_4| Int)
-(assert (= |EVALEXPR_4| expr_43_0))
-(check-sat)
-(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0x34467f46a484d40c850f05c3b05b0817a859573bc546982aeab4a17f9259fb5b":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(set-logic ALL)
-(declare-fun |error_0| () Int)
-(declare-fun |this_0| () Int)
-(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
-(declare-fun |state_0| () |state_type|)
-(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
-(declare-fun |tx_0| () |tx_type|)
-(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
-(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
-(declare-fun |crypto_0| () |crypto_type|)
-(declare-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-
-(assert (and (and true (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1)))
-(check-sat)
-","0x46b3448dbd021b48635faf7ba42511a38684819cde3808197301d93fa7b482ea":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(set-logic ALL)
-(declare-fun |error_0| () Int)
-(declare-fun |this_0| () Int)
-(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
-(declare-fun |state_0| () |state_type|)
-(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
-(declare-fun |tx_0| () |tx_type|)
-(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
-(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
-(declare-fun |crypto_0| () |crypto_type|)
-(declare-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-
-(assert (and (and true (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1)))
-(check-sat)
-","0x6929232f73f56b073cf47977f8ce4ce5c728e02e72812041b60b544333443c3c":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(set-logic ALL)
-(declare-fun |error_0| () Int)
-(declare-fun |this_0| () Int)
-(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
-(declare-fun |state_0| () |state_type|)
-(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
-(declare-fun |tx_0| () |tx_type|)
-(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
-(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
-(declare-fun |crypto_0| () |crypto_type|)
-(declare-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-(declare-fun |expr_26_0| () Int)
-(declare-fun |expr_27_0| () Int)
-(declare-fun |d_div_mod_1_0| () Int)
-(declare-fun |r_div_mod_1_0| () Int)
-(declare-fun |expr_28_1| () Int)
-(declare-fun |expr_29_0| () Int)
-(declare-fun |expr_30_1| () Bool)
-(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
-(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
-(declare-fun |expr_36_0| () Int)
-(declare-fun |expr_37_0| () Int)
-(declare-fun |expr_38_0| () Int)
-(declare-fun |d_div_mod_2_0| () Int)
-(declare-fun |r_div_mod_2_0| () Int)
-(declare-fun |expr_39_1| () Int)
-(declare-fun |r_34_1| () Int)
-(declare-fun |expr_42_0| () Int)
-(declare-fun |expr_43_0| () Int)
-(declare-fun |d_div_mod_3_0| () Int)
-(declare-fun |r_div_mod_3_0| () Int)
-(declare-fun |expr_44_1| () Int)
-(declare-fun |expr_45_0| () Int)
-(declare-fun |expr_46_1| () Bool)
-
-(assert (and (and true (and (= expr_46_1 (= expr_44_1 expr_45_0)) (and (= expr_45_0 0) (and (= expr_44_1 (ite (= expr_43_0 0) 0 r_div_mod_3_0)) (and (and (<= 0 r_div_mod_3_0) (or (= expr_43_0 0) (< r_div_mod_3_0 expr_43_0))) (and (= (+ (* d_div_mod_3_0 expr_43_0) r_div_mod_3_0) expr_42_0) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (= r_34_1 expr_39_1) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_2_0)) (and (and (<= 0 r_div_mod_2_0) (or (= expr_38_0 0) (< r_div_mod_2_0 expr_38_0))) (and (= (+ (* d_div_mod_2_0 expr_38_0) r_div_mod_2_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies true expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))))))))))))))))))) (not expr_46_1)))
-(declare-const |EVALEXPR_0| Int)
-(assert (= |EVALEXPR_0| x_4_0))
-(declare-const |EVALEXPR_1| Int)
-(assert (= |EVALEXPR_1| y_6_0))
-(declare-const |EVALEXPR_2| Int)
-(assert (= |EVALEXPR_2| k_8_0))
-(declare-const |EVALEXPR_3| Int)
-(assert (= |EVALEXPR_3| r_34_1))
-(check-sat)
-(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| ))
-","0x7d43d079635c11d55bba40ba4b7f9c9beeef336e19e5612f020ab7547affbf54":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(set-logic ALL)
-(declare-fun |error_0| () Int)
-(declare-fun |this_0| () Int)
-(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
-(declare-fun |state_0| () |state_type|)
-(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
-(declare-fun |tx_0| () |tx_type|)
-(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
-(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
-(declare-fun |crypto_0| () |crypto_type|)
-(declare-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-
-(assert (and (and true (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1))
-(check-sat)
-","0x94d4c42b833aeec4b7c67fb46410594966e252d7ca8bf44e5687142a078842b2":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(set-logic ALL)
-(declare-fun |error_0| () Int)
-(declare-fun |this_0| () Int)
-(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
-(declare-fun |state_0| () |state_type|)
-(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
-(declare-fun |tx_0| () |tx_type|)
-(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
-(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
-(declare-fun |crypto_0| () |crypto_type|)
-(declare-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-(declare-fun |expr_26_0| () Int)
-(declare-fun |expr_27_0| () Int)
-(declare-fun |d_div_mod_1_0| () Int)
-(declare-fun |r_div_mod_1_0| () Int)
-(declare-fun |expr_28_1| () Int)
-(declare-fun |expr_29_0| () Int)
-(declare-fun |expr_30_1| () Bool)
-(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
-(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
-(declare-fun |expr_36_0| () Int)
-(declare-fun |expr_37_0| () Int)
-(declare-fun |expr_38_0| () Int)
-(declare-fun |d_div_mod_2_0| () Int)
-(declare-fun |r_div_mod_2_0| () Int)
-(declare-fun |expr_39_1| () Int)
-(declare-fun |r_34_1| () Int)
-(declare-fun |expr_42_0| () Int)
-(declare-fun |expr_43_0| () Int)
-(declare-fun |d_div_mod_3_0| () Int)
-(declare-fun |r_div_mod_3_0| () Int)
-(declare-fun |expr_44_1| () Int)
-(declare-fun |expr_45_0| () Int)
-(declare-fun |expr_46_1| () Bool)
-
-(assert (and (and true (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies true expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))))))))))))) (= expr_38_0 0)))
-(declare-const |EVALEXPR_0| Int)
-(assert (= |EVALEXPR_0| x_4_0))
-(declare-const |EVALEXPR_1| Int)
-(assert (= |EVALEXPR_1| y_6_0))
-(declare-const |EVALEXPR_2| Int)
-(assert (= |EVALEXPR_2| k_8_0))
-(declare-const |EVALEXPR_3| Int)
-(assert (= |EVALEXPR_3| r_34_0))
-(declare-const |EVALEXPR_4| Int)
-(assert (= |EVALEXPR_4| expr_38_0))
-(check-sat)
-(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0x9ccee337d79bf0618f658506fca4179eacaee0de28aebc060fce24a9a2cb21fc":"(set-option :produce-models true)
-(set-option :timeout 1000)
-(set-logic ALL)
-(declare-fun |error_0| () Int)
-(declare-fun |this_0| () Int)
-(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
-(declare-fun |state_0| () |state_type|)
-(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
-(declare-fun |tx_0| () |tx_type|)
-(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
-(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
-(declare-fun |crypto_0| () |crypto_type|)
-(declare-fun |x_4_0| () Int)
-(declare-fun |y_6_0| () Int)
-(declare-fun |k_8_0| () Int)
-(declare-fun |r_34_0| () Int)
-(declare-fun |expr_12_0| () Int)
-(declare-fun |expr_13_0| () Int)
-(declare-fun |expr_14_1| () Bool)
-(declare-fun |expr_18_0| () Int)
-(declare-fun |expr_19_0| () Int)
-(declare-fun |d_div_mod_0_0| () Int)
-(declare-fun |r_div_mod_0_0| () Int)
-(declare-fun |expr_20_1| () Int)
-(declare-fun |expr_21_0| () Int)
-(declare-fun |expr_22_1| () Bool)
-(declare-fun |expr_26_0| () Int)
-(declare-fun |expr_27_0| () Int)
-(declare-fun |d_div_mod_1_0| () Int)
-(declare-fun |r_div_mod_1_0| () Int)
-(declare-fun |expr_28_1| () Int)
-(declare-fun |expr_29_0| () Int)
-(declare-fun |expr_30_1| () Bool)
-(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
-(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
-(declare-fun |expr_36_0| () Int)
-(declare-fun |expr_37_0| () Int)
-(declare-fun |expr_38_0| () Int)
-(declare-fun |d_div_mod_2_0| () Int)
-(declare-fun |r_div_mod_2_0| () Int)
-(declare-fun |expr_39_1| () Int)
-(declare-fun |r_34_1| () Int)
-(declare-fun |expr_42_0| () Int)
-(declare-fun |expr_43_0| () Int)
-(declare-fun |d_div_mod_3_0| () Int)
-(declare-fun |r_div_mod_3_0| () Int)
-(declare-fun |expr_44_1| () Int)
-(declare-fun |expr_45_0| () Int)
-(declare-fun |expr_46_1| () Bool)
-
-(assert (and (and true (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies true expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))) (= expr_27_0 0)))
+(assert (and (and (and true true) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))) (= expr_27_0 0)))
 (declare-const |EVALEXPR_0| Int)
 (assert (= |EVALEXPR_0| x_4_0))
 (declare-const |EVALEXPR_1| Int)
@@ -409,7 +62,30 @@
 (assert (= |EVALEXPR_4| expr_27_0))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0xc087609e1dc5e5b58588a60985e4e04dbb5b602e92873c2123a018895f5f9e1a":"(set-option :produce-models true)
+","0x3091365cefd5a713eea87735305ab53c75303343ebf74b77d3578ae0b73c64a2":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1)))
+(check-sat)
+","0x46c0f34a4da6b31138e9238be92256a3c472a5a24c88371ef680f78e0c520cb6":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -460,7 +136,205 @@
 (declare-fun |expr_45_0| () Int)
 (declare-fun |expr_46_1| () Bool)
 
-(assert (and (and true (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies true expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))) (= expr_19_0 0)))
+(assert (and (and (and true true) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))))))))))))) (= expr_38_0 0)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| x_4_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| y_6_0))
+(declare-const |EVALEXPR_2| Int)
+(assert (= |EVALEXPR_2| k_8_0))
+(declare-const |EVALEXPR_3| Int)
+(assert (= |EVALEXPR_3| r_34_0))
+(declare-const |EVALEXPR_4| Int)
+(assert (= |EVALEXPR_4| expr_38_0))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
+","0x6378f27de46d517b5bafe774eab66c12cb656dbd031cb5e710f07b1bfd6c5f79":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1)))
+(check-sat)
+","0x7db419e89d4bb9fbaa4bda7fd522223a515177ff577a6d381e7f2b7f4612582b":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1))
+(check-sat)
+","0x7de8eaf2518b47eec1afadbebacdfa7d93a1878e0f1b6eef91b8a80f1246937e":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+(declare-fun |expr_26_0| () Int)
+(declare-fun |expr_27_0| () Int)
+(declare-fun |d_div_mod_1_0| () Int)
+(declare-fun |r_div_mod_1_0| () Int)
+(declare-fun |expr_28_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1)))
+(check-sat)
+","0x8c4f3faef8ad4a2fe9935f16ec93e2df20f5a3831be51c13afe060774658141c":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+(declare-fun |expr_26_0| () Int)
+(declare-fun |expr_27_0| () Int)
+(declare-fun |d_div_mod_1_0| () Int)
+(declare-fun |r_div_mod_1_0| () Int)
+(declare-fun |expr_28_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1))
+(check-sat)
+","0xa4666c5d197afd69bd82af703fb694c1d3cdd8926ab480fc42e69231134d9265":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+(declare-fun |expr_26_0| () Int)
+(declare-fun |expr_27_0| () Int)
+(declare-fun |d_div_mod_1_0| () Int)
+(declare-fun |r_div_mod_1_0| () Int)
+(declare-fun |expr_28_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_1| () Bool)
+(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
+(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |expr_37_0| () Int)
+(declare-fun |expr_38_0| () Int)
+(declare-fun |d_div_mod_2_0| () Int)
+(declare-fun |r_div_mod_2_0| () Int)
+(declare-fun |expr_39_1| () Int)
+(declare-fun |r_34_1| () Int)
+(declare-fun |expr_42_0| () Int)
+(declare-fun |expr_43_0| () Int)
+(declare-fun |d_div_mod_3_0| () Int)
+(declare-fun |r_div_mod_3_0| () Int)
+(declare-fun |expr_44_1| () Int)
+(declare-fun |expr_45_0| () Int)
+(declare-fun |expr_46_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))) (= expr_19_0 0)))
 (declare-const |EVALEXPR_0| Int)
 (assert (= |EVALEXPR_0| x_4_0))
 (declare-const |EVALEXPR_1| Int)
@@ -473,7 +347,7 @@
 (assert (= |EVALEXPR_4| expr_19_0))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0xee7d96e23195f6aeb74a805122639dcd6a8932788ceeae3cba711aba9050a0b7":"(set-option :produce-models true)
+","0xa81ce8317a79fc74d85d9edfe56caf9b0274a7da4556bfb418652051e0bfa679":"(set-option :produce-models true)
 (set-option :timeout 1000)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
@@ -494,8 +368,134 @@
 (declare-fun |expr_13_0| () Int)
 (declare-fun |expr_14_1| () Bool)
 
-(assert (and (and true (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1))
+(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1))
 (check-sat)
+","0xa96a68b7853fcc0a10dd525c3ff838e3bfac425b104c44b240623f7a35aee6f1":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+(declare-fun |expr_26_0| () Int)
+(declare-fun |expr_27_0| () Int)
+(declare-fun |d_div_mod_1_0| () Int)
+(declare-fun |r_div_mod_1_0| () Int)
+(declare-fun |expr_28_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_1| () Bool)
+(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
+(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |expr_37_0| () Int)
+(declare-fun |expr_38_0| () Int)
+(declare-fun |d_div_mod_2_0| () Int)
+(declare-fun |r_div_mod_2_0| () Int)
+(declare-fun |expr_39_1| () Int)
+(declare-fun |r_34_1| () Int)
+(declare-fun |expr_42_0| () Int)
+(declare-fun |expr_43_0| () Int)
+(declare-fun |d_div_mod_3_0| () Int)
+(declare-fun |r_div_mod_3_0| () Int)
+(declare-fun |expr_44_1| () Int)
+(declare-fun |expr_45_0| () Int)
+(declare-fun |expr_46_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_46_1 (= expr_44_1 expr_45_0)) (and (= expr_45_0 0) (and (= expr_44_1 (ite (= expr_43_0 0) 0 r_div_mod_3_0)) (and (and (<= 0 r_div_mod_3_0) (or (= expr_43_0 0) (< r_div_mod_3_0 expr_43_0))) (and (= (+ (* d_div_mod_3_0 expr_43_0) r_div_mod_3_0) expr_42_0) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (ite (and true true) (= r_34_1 expr_39_1) (= r_34_1 r_34_0)) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_2_0)) (and (and (<= 0 r_div_mod_2_0) (or (= expr_38_0 0) (< r_div_mod_2_0 expr_38_0))) (and (= (+ (* d_div_mod_2_0 expr_38_0) r_div_mod_2_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))))))))))))))))))) (not expr_46_1)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| x_4_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| y_6_0))
+(declare-const |EVALEXPR_2| Int)
+(assert (= |EVALEXPR_2| k_8_0))
+(declare-const |EVALEXPR_3| Int)
+(assert (= |EVALEXPR_3| r_34_1))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| ))
+","0xcc1de975d2f5e9b3e4ff9b4f46c8248513ac3b755b60f8a630a46d12b4b11f9a":"(set-option :produce-models true)
+(set-option :timeout 1000)
+(set-logic ALL)
+(declare-fun |error_0| () Int)
+(declare-fun |this_0| () Int)
+(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
+(declare-fun |state_0| () |state_type|)
+(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-fun |tx_0| () |tx_type|)
+(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
+(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
+(declare-fun |crypto_0| () |crypto_type|)
+(declare-fun |x_4_0| () Int)
+(declare-fun |y_6_0| () Int)
+(declare-fun |k_8_0| () Int)
+(declare-fun |r_34_0| () Int)
+(declare-fun |expr_12_0| () Int)
+(declare-fun |expr_13_0| () Int)
+(declare-fun |expr_14_1| () Bool)
+(declare-fun |expr_18_0| () Int)
+(declare-fun |expr_19_0| () Int)
+(declare-fun |d_div_mod_0_0| () Int)
+(declare-fun |r_div_mod_0_0| () Int)
+(declare-fun |expr_20_1| () Int)
+(declare-fun |expr_21_0| () Int)
+(declare-fun |expr_22_1| () Bool)
+(declare-fun |expr_26_0| () Int)
+(declare-fun |expr_27_0| () Int)
+(declare-fun |d_div_mod_1_0| () Int)
+(declare-fun |r_div_mod_1_0| () Int)
+(declare-fun |expr_28_1| () Int)
+(declare-fun |expr_29_0| () Int)
+(declare-fun |expr_30_1| () Bool)
+(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
+(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
+(declare-fun |expr_36_0| () Int)
+(declare-fun |expr_37_0| () Int)
+(declare-fun |expr_38_0| () Int)
+(declare-fun |d_div_mod_2_0| () Int)
+(declare-fun |r_div_mod_2_0| () Int)
+(declare-fun |expr_39_1| () Int)
+(declare-fun |r_34_1| () Int)
+(declare-fun |expr_42_0| () Int)
+(declare-fun |expr_43_0| () Int)
+(declare-fun |d_div_mod_3_0| () Int)
+(declare-fun |r_div_mod_3_0| () Int)
+(declare-fun |expr_44_1| () Int)
+(declare-fun |expr_45_0| () Int)
+(declare-fun |expr_46_1| () Bool)
+
+(assert (and (and (and true true) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (ite (and true true) (= r_34_1 expr_39_1) (= r_34_1 r_34_0)) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_2_0)) (and (and (<= 0 r_div_mod_2_0) (or (= expr_38_0 0) (< r_div_mod_2_0 expr_38_0))) (and (= (+ (* d_div_mod_2_0 expr_38_0) r_div_mod_2_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))))))))))))))))))) (= expr_43_0 0)))
+(declare-const |EVALEXPR_0| Int)
+(assert (= |EVALEXPR_0| x_4_0))
+(declare-const |EVALEXPR_1| Int)
+(assert (= |EVALEXPR_1| y_6_0))
+(declare-const |EVALEXPR_2| Int)
+(assert (= |EVALEXPR_2| k_8_0))
+(declare-const |EVALEXPR_3| Int)
+(assert (= |EVALEXPR_3| r_34_1))
+(declare-const |EVALEXPR_4| Int)
+(assert (= |EVALEXPR_4| expr_43_0))
+(check-sat)
+(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
 "}},"errors":[{"component":"general","errorCode":"7812","formattedMessage":"A:6:85: Warning: BMC: Assertion violation might happen here.
 require(k > 0); require(x % k == 0); require(y % k == 0); uint r = mulmod(x, y, k); assert(r % k == 0);}}
                                                                                     ^----------------^
diff --git a/test/externalTests.sh b/test/externalTests.sh
index d7ba829a7..7bf3eb76b 100755
--- a/test/externalTests.sh
+++ b/test/externalTests.sh
@@ -45,6 +45,7 @@ printTask "Running external tests..."
 $REPO_ROOT/externalTests/zeppelin.sh "$SOLJSON"
 $REPO_ROOT/externalTests/gnosis.sh "$SOLJSON"
 $REPO_ROOT/externalTests/colony.sh "$SOLJSON"
+$REPO_ROOT/externalTests/ens.sh "$SOLJSON"
 
 # Disabled temporarily as it needs to be updated to latest Truffle first.
 #test_truffle Gnosis https://github.com/axic/pm-contracts.git solidity-050
diff --git a/test/externalTests/common.sh b/test/externalTests/common.sh
index ebc57b97d..5a9f42ba2 100644
--- a/test/externalTests/common.sh
+++ b/test/externalTests/common.sh
@@ -104,7 +104,7 @@ function replace_version_pragmas
     # Replace fixed-version pragmas (part of Consensys best practice).
     # Include all directories to also cover node dependencies.
     printLog "Replacing fixed-version pragmas..."
-    find . test -name '*.sol' -type f -print0 | xargs -0 sed -i -e 's/pragma solidity [\^0-9\.]*/pragma solidity >=0.0/'
+    find . test -name '*.sol' -type f -print0 | xargs -0 sed -i -E -e 's/pragma solidity [^;]+;/pragma solidity >=0.0;/'
 }
 
 function replace_libsolc_call
diff --git a/test/externalTests/ens.sh b/test/externalTests/ens.sh
new file mode 100755
index 000000000..bdd501703
--- /dev/null
+++ b/test/externalTests/ens.sh
@@ -0,0 +1,44 @@
+#!/usr/bin/env bash
+
+# ------------------------------------------------------------------------------
+# This file is part of solidity.
+#
+# solidity is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# solidity is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with solidity.  If not, see <http://www.gnu.org/licenses/>
+#
+# (c) 2019 solidity contributors.
+#------------------------------------------------------------------------------
+# shellcheck disable=SC1091
+source scripts/common.sh
+# shellcheck disable=SC1091
+source test/externalTests/common.sh
+
+verify_input "$1"
+export SOLJSON="$1"
+
+function install_fn { npm install; }
+function compile_fn { npx truffle compile; }
+function test_fn { npm run test; }
+
+function ens_test
+{
+    export OPTIMIZER_LEVEL=1
+    export CONFIG="truffle-config.js"
+
+    truffle_setup https://github.com/solidity-external-tests/ens.git upgrade-0.8.0
+    run_install install_fn
+
+    truffle_run_test compile_fn test_fn
+}
+
+external_test Ens ens_test
diff --git a/test/libsolidity/SolidityEndToEndTest.cpp b/test/libsolidity/SolidityEndToEndTest.cpp
index cd7dc1710..db45577c8 100644
--- a/test/libsolidity/SolidityEndToEndTest.cpp
+++ b/test/libsolidity/SolidityEndToEndTest.cpp
@@ -4384,30 +4384,6 @@ BOOST_AUTO_TEST_CASE(non_payable_throw)
 	BOOST_CHECK_EQUAL(balanceAt(m_contractAddress), 0);
 }
 
-BOOST_AUTO_TEST_CASE(no_nonpayable_circumvention_by_modifier)
-{
-	char const* sourceCode = R"(
-		contract C {
-			modifier tryCircumvent {
-				if (false) _; // avoid the function, we should still not accept ether
-			}
-			function f() tryCircumvent public returns (uint) {
-				return msgvalue();
-			}
-			function msgvalue() internal returns (uint) {
-				return msg.value;
-			}
-		}
-	)";
-	ALSO_VIA_YUL(
-		DISABLE_EWASM_TESTRUN()
-
-		compileAndRun(sourceCode);
-		ABI_CHECK(callContractFunctionWithValue("f()", 27), encodeArgs());
-		BOOST_CHECK_EQUAL(balanceAt(m_contractAddress), 0);
-	)
-}
-
 BOOST_AUTO_TEST_CASE(mem_resize_is_not_paid_at_call)
 {
 	// This tests that memory resize for return values is not paid during the call, which would
diff --git a/test/libsolidity/semanticTests/array/copying/array_copy_storage_storage_different_base.sol b/test/libsolidity/semanticTests/array/copying/array_copy_storage_storage_different_base.sol
new file mode 100644
index 000000000..e1b6cfeb1
--- /dev/null
+++ b/test/libsolidity/semanticTests/array/copying/array_copy_storage_storage_different_base.sol
@@ -0,0 +1,19 @@
+contract c {
+    uint64[] data1;
+    uint256[] data2;
+
+    function test() public returns (uint256 x, uint256 y) {
+        data2.push(11);
+        data1.push(0);
+        data1.push(1);
+        data1.push(2);
+        data1.push(3);
+        data1.push(4);
+        data2 = data1;
+        assert(data1[0] == data2[0]);
+        x = data2.length;
+        y = data2[4];
+    }
+}
+// ----
+// test() -> 5, 4
diff --git a/test/libsolidity/semanticTests/array/copying/array_copy_storage_storage_dynamic_dynamic.sol b/test/libsolidity/semanticTests/array/copying/array_copy_storage_storage_dynamic_dynamic.sol
new file mode 100644
index 000000000..7815f0a28
--- /dev/null
+++ b/test/libsolidity/semanticTests/array/copying/array_copy_storage_storage_dynamic_dynamic.sol
@@ -0,0 +1,22 @@
+contract c {
+    uint256[] data1;
+    uint256[] data2;
+
+    function test() public returns (uint256 x, uint256 y) {
+        data2.push(11);
+        data1.push(0);
+        data1.push(1);
+        data1.push(2);
+        data1.push(3);
+        data1.push(4);
+        data2 = data1;
+        assert(data1[0] == data2[0]);
+        x = data2.length;
+        y = data2[4];
+    }
+}
+
+// ====
+// compileViaYul: also
+// ----
+// test() -> 5, 4
diff --git a/test/libsolidity/semanticTests/array/copying/array_copy_storage_storage_static_static.sol b/test/libsolidity/semanticTests/array/copying/array_copy_storage_storage_static_static.sol
index 71601d477..98642c9e1 100644
--- a/test/libsolidity/semanticTests/array/copying/array_copy_storage_storage_static_static.sol
+++ b/test/libsolidity/semanticTests/array/copying/array_copy_storage_storage_static_static.sol
@@ -13,5 +13,7 @@ contract c {
     }
 }
 
+// ====
+// compileViaYul: also
 // ----
 // test() -> 8, 0
diff --git a/test/libsolidity/semanticTests/array/copying/array_nested_calldata_to_memory.sol b/test/libsolidity/semanticTests/array/copying/array_nested_calldata_to_memory.sol
index dbafccf9c..7da4fc4ed 100644
--- a/test/libsolidity/semanticTests/array/copying/array_nested_calldata_to_memory.sol
+++ b/test/libsolidity/semanticTests/array/copying/array_nested_calldata_to_memory.sol
@@ -30,7 +30,7 @@ contract c {
     }
 }
 // ====
-// compileViaYul: true
+// compileViaYul: also
 // ----
 // test1(uint256[][]): 0x20, 2, 0x40, 0x40, 2, 23, 42 -> 2, 65
 // test2(uint256[][2]): 0x20, 0x40, 0x40, 2, 23, 42 -> 2, 65
diff --git a/test/libsolidity/semanticTests/array/copying/array_of_structs_containing_arrays_calldata_to_memory.sol b/test/libsolidity/semanticTests/array/copying/array_of_structs_containing_arrays_calldata_to_memory.sol
index 13e05c4ee..6ec4c5471 100644
--- a/test/libsolidity/semanticTests/array/copying/array_of_structs_containing_arrays_calldata_to_memory.sol
+++ b/test/libsolidity/semanticTests/array/copying/array_of_structs_containing_arrays_calldata_to_memory.sol
@@ -18,6 +18,6 @@ contract C {
     }
 }
 // ====
-// compileViaYul: true
+// compileViaYul: also
 // ----
 // f((uint256[])[]): 0x20, 3, 0x60, 0x60, 0x60, 0x20, 3, 1, 2, 3 -> 3, 1
\ No newline at end of file
diff --git a/test/libsolidity/semanticTests/array/copying/calldata_2d_bytes_to_memory.sol b/test/libsolidity/semanticTests/array/copying/calldata_2d_bytes_to_memory.sol
new file mode 100644
index 000000000..1687fb54a
--- /dev/null
+++ b/test/libsolidity/semanticTests/array/copying/calldata_2d_bytes_to_memory.sol
@@ -0,0 +1,14 @@
+pragma abicoder v2;
+
+contract C {
+    function g(bytes[2] memory m) internal returns (bytes memory) {
+        return m[0];
+    }
+    function f(bytes[2] calldata c) external returns (bytes memory) {
+        return g(c);
+    }
+}
+// ====
+// compileViaYul: also
+// ----
+// f(bytes[2]): 0x20, 0x40, 0x40, 2, "ab" -> 0x20, 2, "ab"
diff --git a/test/libsolidity/semanticTests/array/copying/calldata_2d_bytes_to_memory_2.sol b/test/libsolidity/semanticTests/array/copying/calldata_2d_bytes_to_memory_2.sol
new file mode 100644
index 000000000..f87aa6bd1
--- /dev/null
+++ b/test/libsolidity/semanticTests/array/copying/calldata_2d_bytes_to_memory_2.sol
@@ -0,0 +1,18 @@
+pragma abicoder v2;
+
+contract C {
+    function g(bytes[2] memory m) internal {
+        assert(m[0].length > 1);
+        assert(m[1].length > 1);
+        assert(m[0][0] == m[1][0]);
+        assert(m[0][1] == m[1][1]);
+    }
+    function f(bytes[2] calldata c) external {
+        g(c);
+    }
+}
+// ====
+// compileViaYul: also
+// ----
+// f(bytes[2]): 0x20, 0x40, 0x40, 2, "ab" ->
+// f(bytes[2]): 0x20, 0x40, 0x40, 1, "a" -> FAILURE
diff --git a/test/libsolidity/semanticTests/array/copying/calldata_nested_array_copy_to_memory.sol b/test/libsolidity/semanticTests/array/copying/calldata_nested_array_copy_to_memory.sol
new file mode 100644
index 000000000..bfcd5ead4
--- /dev/null
+++ b/test/libsolidity/semanticTests/array/copying/calldata_nested_array_copy_to_memory.sol
@@ -0,0 +1,14 @@
+pragma abicoder v2;
+
+contract Test {
+    struct shouldBug {
+        uint256[][2] deadly;
+    }
+    function killer(uint256[][2] calldata weapon) pure external returns (shouldBug memory) {
+        return shouldBug(weapon);
+    }
+}
+// ====
+// compileViaYul: also
+// ----
+// killer(uint256[][2]): 0x20, 0x40, 0x40, 2, 1, 2 -> 0x20, 0x20, 0x40, 0xa0, 2, 1, 2, 2, 1, 2
diff --git a/test/libsolidity/semanticTests/inlineAssembly/inline_assembly_in_modifiers.sol b/test/libsolidity/semanticTests/inlineAssembly/inline_assembly_in_modifiers.sol
index 2eb723181..70f19479a 100644
--- a/test/libsolidity/semanticTests/inlineAssembly/inline_assembly_in_modifiers.sol
+++ b/test/libsolidity/semanticTests/inlineAssembly/inline_assembly_in_modifiers.sol
@@ -11,10 +11,23 @@ contract C {
     function f() public m returns (bool) {
         return true;
     }
+
+    modifier n {
+        uint256 a = 1;
+        assembly {
+            a := 2
+        }
+        if (a != 2)
+            _;
+        revert();
+    }
+
+    function g() public n returns (bool) {
+        // This statement should never execute.
+        return true;
+    }
 }
 
-// ====
-// compileViaYul: also
-// compileToEwasm: also
 // ----
 // f() -> true
+// g() -> FAILURE
diff --git a/test/libsolidity/semanticTests/modifiers/break_in_modifier.sol b/test/libsolidity/semanticTests/modifiers/break_in_modifier.sol
index 23f03a822..67fc0e6be 100644
--- a/test/libsolidity/semanticTests/modifiers/break_in_modifier.sol
+++ b/test/libsolidity/semanticTests/modifiers/break_in_modifier.sol
@@ -3,7 +3,8 @@ contract C {
     modifier run() {
         for (uint256 i = 0; i < 10; i++) {
             _;
-            break;
+            if (i == 1)
+                break;
         }
     }
 
@@ -13,10 +14,7 @@ contract C {
         x = t;
     }
 }
-// ====
-// compileViaYul: also
-// compileToEwasm: also
 // ----
 // x() -> 0
 // f() ->
-// x() -> 1
+// x() -> 2
diff --git a/test/libsolidity/semanticTests/modifiers/stacked_return_with_modifiers.sol b/test/libsolidity/semanticTests/modifiers/stacked_return_with_modifiers.sol
index 23f03a822..616a2183c 100644
--- a/test/libsolidity/semanticTests/modifiers/stacked_return_with_modifiers.sol
+++ b/test/libsolidity/semanticTests/modifiers/stacked_return_with_modifiers.sol
@@ -1,22 +1,21 @@
 contract C {
     uint256 public x;
-    modifier run() {
+    modifier m() {
         for (uint256 i = 0; i < 10; i++) {
             _;
-            break;
+            ++x;
+            return;
         }
     }
 
-    function f() public run {
-        uint256 k = x;
-        uint256 t = k + 1;
-        x = t;
+    function f() public m m m returns (uint) {
+        for (uint256 i = 0; i < 10; i++) {
+            ++x;
+            return 42;
+        }
     }
 }
-// ====
-// compileViaYul: also
-// compileToEwasm: also
 // ----
 // x() -> 0
-// f() ->
-// x() -> 1
+// f() -> 42
+// x() -> 4
diff --git a/test/libsolidity/semanticTests/payable/no_nonpayable_circumvention_by_modifier.sol b/test/libsolidity/semanticTests/payable/no_nonpayable_circumvention_by_modifier.sol
new file mode 100644
index 000000000..cefb8f3b7
--- /dev/null
+++ b/test/libsolidity/semanticTests/payable/no_nonpayable_circumvention_by_modifier.sol
@@ -0,0 +1,18 @@
+contract C {
+    modifier tryCircumvent {
+        if (false) _; // avoid the function, we should still not accept ether
+    }
+    function f() tryCircumvent public returns (uint) {
+        return msgvalue();
+    }
+    function msgvalue() internal returns (uint) {
+        return msg.value;
+    }
+    // TODO: remove this helper function once isoltest supports balance checking
+    function balance() external returns (uint) {
+        return address(this).balance;
+    }
+}
+// ----
+// f(), 27 wei -> FAILURE
+// balance() -> 0
diff --git a/test/libsolidity/semanticTests/structs/calldata/calldata_struct_array_member.sol b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_array_member.sol
index c15aaaf50..0439aeff5 100644
--- a/test/libsolidity/semanticTests/structs/calldata/calldata_struct_array_member.sol
+++ b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_array_member.sol
@@ -1,4 +1,4 @@
-pragma abicoder               v2;
+pragma abicoder v2;
 
 
 contract C {
@@ -19,6 +19,7 @@ contract C {
         c = s.c;
     }
 }
-
+// ====
+// compileViaYul: also
 // ----
 // f((uint256,uint256[2],uint256)): 42, 1, 2, 23 -> 42, 1, 2, 23
diff --git a/test/libsolidity/semanticTests/structs/calldata/calldata_struct_array_member_dynamic.sol b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_array_member_dynamic.sol
new file mode 100644
index 000000000..bac400295
--- /dev/null
+++ b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_array_member_dynamic.sol
@@ -0,0 +1,24 @@
+pragma abicoder v2;
+
+contract C {
+    struct S {
+        uint32 a;
+        uint256[] b;
+        uint64 c;
+    }
+
+    function f(S calldata s)
+        external
+        pure
+        returns (uint32 a, uint256 b0, uint256 b1, uint64 c)
+    {
+        a = s.a;
+        b0 = s.b[0];
+        b1 = s.b[1];
+        c = s.c;
+    }
+}
+// ====
+// compileViaYul: also
+// ----
+// f((uint32,uint256[],uint64)): 0x20, 42, 0x60, 23, 2, 1, 2 -> 42, 1, 2, 23
diff --git a/test/libsolidity/semanticTests/structs/calldata/calldata_struct_struct_member.sol b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_struct_member.sol
new file mode 100644
index 000000000..fede46d6a
--- /dev/null
+++ b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_struct_member.sol
@@ -0,0 +1,28 @@
+pragma abicoder v2;
+
+contract C {
+    struct S {
+        uint64 a;
+        uint64 b;
+    }
+    struct S1 {
+        uint256 a;
+        S s;
+        uint256 c;
+    }
+
+    function f(S1 calldata s1)
+        external
+        pure
+        returns (uint256 a, uint64 b0, uint64 b1, uint256 c)
+    {
+        a = s1.a;
+        b0 = s1.s.a;
+        b1 = s1.s.b;
+        c = s1.c;
+    }
+}
+// ====
+// compileViaYul: also
+// ----
+// f((uint256,(uint64, uint64),uint256)): 42, 1, 2, 23 -> 42, 1, 2, 23
diff --git a/test/libsolidity/semanticTests/structs/calldata/calldata_struct_struct_member_dynamic.sol b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_struct_member_dynamic.sol
new file mode 100644
index 000000000..64baab7c8
--- /dev/null
+++ b/test/libsolidity/semanticTests/structs/calldata/calldata_struct_struct_member_dynamic.sol
@@ -0,0 +1,28 @@
+pragma abicoder v2;
+
+contract C {
+    struct S {
+        uint64 a;
+        bytes b;
+    }
+    struct S1 {
+        uint256 a;
+        S s;
+        uint256 c;
+    }
+
+    function f(S1 calldata s1)
+        external
+        pure
+        returns (uint256 a, uint64 b0, byte b1, uint256 c)
+    {
+        a = s1.a;
+        b0 = s1.s.a;
+        b1 = s1.s.b[0];
+        c = s1.c;
+    }
+}
+// ====
+// compileViaYul: also
+// ----
+// f((uint256,(uint64, bytes),uint256)): 0x20, 42, 0x60, 23, 1, 0x40, 2, "ab" -> 42, 1, "a", 23
diff --git a/test/libsolidity/semanticTests/various/iszero_bnot_correct.sol b/test/libsolidity/semanticTests/various/iszero_bnot_correct.sol
index 743825d60..e957fbc8e 100644
--- a/test/libsolidity/semanticTests/various/iszero_bnot_correct.sol
+++ b/test/libsolidity/semanticTests/various/iszero_bnot_correct.sol
@@ -15,5 +15,7 @@ contract C {
     }
 }
 
+// ====
+// compileViaYul: also
 // ----
 // f() -> true
diff --git a/test/libsolidity/semanticTests/various/nested_calldata_struct.sol b/test/libsolidity/semanticTests/various/nested_calldata_struct.sol
index dde91c719..6a05524f5 100644
--- a/test/libsolidity/semanticTests/various/nested_calldata_struct.sol
+++ b/test/libsolidity/semanticTests/various/nested_calldata_struct.sol
@@ -22,5 +22,7 @@ contract C {
     }
 }
 
+// ====
+// compileViaYul: also
 // ----
 // f((uint256,uint256,(uint256,uint256),uint256)): 1, 2, 3, 4, 5 -> 1, 2, 3, 4, 5
diff --git a/test/libsolidity/semanticTests/viaYul/unary_fixedbytes.sol b/test/libsolidity/semanticTests/viaYul/unary_fixedbytes.sol
new file mode 100644
index 000000000..3f4d586e6
--- /dev/null
+++ b/test/libsolidity/semanticTests/viaYul/unary_fixedbytes.sol
@@ -0,0 +1,87 @@
+contract C {
+	function conv(bytes25 a) public pure returns (bytes32) {
+		// truncating and widening
+		return ~bytes32(bytes16(~a));
+	}
+
+	function upcast(bytes25 a) public pure returns (bytes32) {
+		// implicit widening is allowed
+		return ~a;
+	}
+
+	function downcast(bytes25 a) public pure returns (bytes12) {
+		// truncating cast must be explicit
+		return bytes12(~a);
+	}
+
+	function r_b32() public pure returns (bytes32) {
+		return ~bytes32(hex"ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00");
+	}
+	function r_b25() public pure returns (bytes25) {
+		return ~bytes25(hex"ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff");
+	}
+	function r_b16() public pure returns (bytes16) {
+		return ~bytes16(hex"ff00ff00ff00ff00ff00ff00ff00ff00");
+	}
+	function r_b8() public pure returns (bytes8) {
+		return ~bytes8(hex"ff00ff00ff00ff00");
+	}
+	function r_b4() public pure returns (bytes4) {
+		return ~bytes4(hex"ff00ff00");
+	}
+	function r_b1() public pure returns (bytes1) {
+		return ~bytes1(hex"55");
+	}
+	function r_b() public pure returns (byte) {
+		return ~byte(hex"55");
+	}
+
+	function a_b32() public pure returns (bytes32) {
+		bytes32 r = ~bytes32(hex"ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00");
+		return r;
+	}
+	function a_b25() public pure returns (bytes25) {
+		bytes25 r = ~bytes25(hex"ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff");
+		return r;
+	}
+	function a_b16() public pure returns (bytes16) {
+		bytes16 r =  ~bytes16(hex"ff00ff00ff00ff00ff00ff00ff00ff00");
+		return r;
+	}
+	function a_b8() public pure returns (bytes8) {
+		bytes8 r =  ~bytes8(hex"ff00ff00ff00ff00");
+		return r;
+	}
+	function a_b4() public pure returns (bytes4) {
+		bytes4 r =  ~bytes4(hex"ff00ff00");
+		return r;
+	}
+	function a_b1() public pure returns (byte) {
+		bytes1 r =  ~bytes1(hex"55");
+		return r;
+	}
+	function a_b() public pure returns (byte) {
+		byte r =  ~byte(hex"55");
+		return r;
+	}
+}
+// ====
+// compileViaYul: also
+// ----
+// conv(bytes25): left(0xff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff) -> 0xff00ff00ff00ff00ff00ff00ff00ff00ffffffffffffffffffffffffffffffff
+// upcast(bytes25): left(0xff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff) -> 0xff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff0000000000000000
+// downcast(bytes25): left(0xff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff) -> 0xff00ff00ff00ff00ff00ff0000000000000000000000000000000000000000
+// r_b32() -> 0xff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff
+// r_b25() -> 0xff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff0000000000000000
+// r_b16() -> 0xff00ff00ff00ff00ff00ff00ff00ff00000000000000000000000000000000
+// r_b8() -> 0xff00ff00ff00ff000000000000000000000000000000000000000000000000
+// r_b4() -> 0xff00ff00000000000000000000000000000000000000000000000000000000
+// r_b1() -> 0xaa00000000000000000000000000000000000000000000000000000000000000
+// r_b() -> 0xaa00000000000000000000000000000000000000000000000000000000000000
+// a_b32() -> 0xff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff
+// a_b25() -> 0xff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff0000000000000000
+// a_b16() -> 0xff00ff00ff00ff00ff00ff00ff00ff00000000000000000000000000000000
+// a_b8() -> 0xff00ff00ff00ff000000000000000000000000000000000000000000000000
+// a_b4() -> 0xff00ff00000000000000000000000000000000000000000000000000000000
+// a_b1() -> 0xaa00000000000000000000000000000000000000000000000000000000000000
+// a_b() -> 0xaa00000000000000000000000000000000000000000000000000000000000000
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers.sol
new file mode 100644
index 000000000..fb87df2b5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers.sol
@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	uint x;
+
+	modifier check() {
+		require(x == 0);
+		_;
+		assert(x == 1); // should fail;
+		assert(x == 0); // should hold;
+	}
+
+	modifier inc() {
+		if (x == 0) {
+			return;
+		}
+		x = x + 1;
+		_;
+	}
+
+	function test() check inc public {
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (103-117): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers_2.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers_2.sol
new file mode 100644
index 000000000..47e3a27ef
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/branches_in_modifiers_2.sol
@@ -0,0 +1,45 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+    uint x;
+
+    function reset_if_overflow() internal postinc {
+        if (x < 10)
+            return;
+        x = 0;
+    }
+
+    modifier postinc() {
+        if (x == 0) {
+            return;
+        }
+        _;
+        x = x + 1;
+    }
+
+    function test() public {
+        if (x == 0) {
+            reset_if_overflow();
+            assert(x == 1); // should fail;
+            assert(x == 0); // should hold;
+            return;
+        }
+        if (x < 10) {
+            uint oldx = x;
+            reset_if_overflow();
+            assert(oldx + 1 == x); // should hold;
+            assert(oldx == x);     // should fail;
+            return;
+        }
+        reset_if_overflow();
+        assert(x == 1); // should hold;
+        assert(x == 0); // should fail;
+    }
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (384-398): BMC: Assertion violation happens here.
+// Warning 4661: (635-652): BMC: Assertion violation happens here.
+// Warning 4661: (781-795): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol
new file mode 100644
index 000000000..6d960112a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol
@@ -0,0 +1,43 @@
+pragma experimental SMTChecker;
+
+contract A {
+	int x;
+	constructor (int a) { x = a;}
+}
+
+contract B is A {
+	int y;
+	constructor(int a) A(-a) {
+		if (a > 0) {
+			y = 2;
+			return;
+		}
+		else {
+			y = 3;
+		}
+		y = 4; // overwrites the else branch
+	}
+}
+
+contract C is B {
+	constructor(int a) B(a) {
+		assert(y != 3); // should hold
+		assert(y == 4); // should fail
+		if (a > 0) {
+			assert(x < 0 && y == 2); // should hold
+			assert(x < 0 && y == 4); // should fail
+		}
+		else {
+			assert(x >= 0 && y == 4); // should hold
+			assert(x >= 0 && y == 2); // should fail
+			assert(x > 0); // should fail
+		}
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (330-344): BMC: Assertion violation happens here.
+// Warning 4661: (422-445): BMC: Assertion violation happens here.
+// Warning 4661: (522-546): BMC: Assertion violation happens here.
+// Warning 4661: (566-579): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_chain_alternate.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_chain_alternate.sol
new file mode 100644
index 000000000..511cfbb60
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_chain_alternate.sol
@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x = 1;
+}
+
+contract B is A {
+	constructor(int a) {
+		if (a > 0) {
+			x = 2;
+			return;
+		}
+		x = 3;
+	}
+}
+
+abstract contract C is B {
+}
+
+contract D is C {
+	constructor(int a) B(a) {
+		assert(a > 0 || x == 3); // should hold
+		assert(a <= 0 || x == 2); // should hold
+		assert(x == 1); // should fail
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (319-333): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_diamond.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_diamond.sol
new file mode 100644
index 000000000..c962d1003
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init_diamond.sol
@@ -0,0 +1,72 @@
+pragma experimental SMTChecker;
+
+contract A {
+	int x;
+}
+
+contract B is A {
+	int y;
+	constructor (int a) {
+		if (a >= 0) {
+			y = 1;
+			return;
+		}
+		x = 1;
+		y = 2;
+	}
+}
+
+contract C is A {
+	int z;
+	constructor (int a) {
+		if (a >= 0) {
+			z = 1;
+			return;
+		}
+		x = -1;
+		z = 2;
+	}
+}
+
+contract D1 is B, C {
+	constructor() B(1) C(1) {
+		assert(x == 0); // should hold
+		assert(x == 1); // should fail
+		assert(x == -1); // should fail
+	}
+}
+
+contract D2 is B, C {
+	constructor() B(1) C(-1) {
+		assert(x == 0); // should fail
+		assert(x == 1); // should fail
+		assert(x == -1); // should hold (constructor of C is executed AFTER constructor of B)
+	}
+}
+
+contract D3 is B, C {
+	constructor() B(-1) C(1) {
+		assert(x == 0); // should fail
+		assert(x == 1); // should hold
+		assert(x == -1); // should fail
+	}
+}
+
+contract D4 is B, C {
+	constructor() B(-1) C(-1) {
+		assert(x == 0); // should fail
+		assert(x == 1); // should fail
+		assert(x == -1); // should hold (constructor of C is executed AFTER constructor of B)
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (370-384): BMC: Assertion violation happens here.
+// Warning 4661: (403-418): BMC: Assertion violation happens here.
+// Warning 4661: (493-507): BMC: Assertion violation happens here.
+// Warning 4661: (526-540): BMC: Assertion violation happens here.
+// Warning 4661: (703-717): BMC: Assertion violation happens here.
+// Warning 4661: (769-784): BMC: Assertion violation happens here.
+// Warning 4661: (860-874): BMC: Assertion violation happens here.
+// Warning 4661: (893-907): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructors.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructors.sol
new file mode 100644
index 000000000..9ed5ddcbf
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructors.sol
@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+
+contract B {
+	int x;
+	constructor(int b) {
+		if (b > 0) {
+			x = 1;
+			return;
+		}
+		else {
+			x = 2;
+			return;
+		}
+		x = 3; // dead code
+	}
+}
+
+contract C is B {
+	constructor(int a) B(a) {
+		assert(a > 0 || x == 2); // should hold
+		assert(a <= 0 || x == 1); // should hold
+		assert(x == 3); // should fail
+		assert(x == 2); // should fail
+		assert(x == 1); // should fail
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 5740: (152-157): Unreachable code.
+// Warning 4661: (310-324): BMC: Assertion violation happens here.
+// Warning 4661: (343-357): BMC: Assertion violation happens here.
+// Warning 4661: (376-390): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/nested_if.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/nested_if.sol
new file mode 100644
index 000000000..c941c6421
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/nested_if.sol
@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	function test(uint256 a, uint256 b) public pure {
+		assert(nested_if(a,b) != 42); // should hold
+		assert(nested_if(a,b) == 1);  // should fail
+	}
+
+	function nested_if(uint256 a, uint256 b) internal pure returns (uint256) {
+		if (a < 5) {
+			if (b > 1) {
+				return 0;
+			}
+		}
+		if (a == 2 && b == 2) {
+			return 42; // unreachable
+		}
+		else {
+			return 1;
+		}
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (147-174): BMC: Assertion violation happens here.
+// Warning 6838: (332-348): BMC: Condition is always false.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/return_in_both_branches.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/return_in_both_branches.sol
new file mode 100644
index 000000000..0ad554c31
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/return_in_both_branches.sol
@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	function test() public pure {
+		assert(branches(0) == 0);
+		assert(branches(1) == 42);
+	}
+
+	function branches(uint256 a) internal pure returns (uint256) {
+		if (a == 0) {
+			return 0;
+		}
+		else {
+			return 42;
+		}
+		return 1; // dead code
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 5740: (265-273): Unreachable code.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if.sol
new file mode 100644
index 000000000..783a28543
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function test(uint256 a, uint256 b) public pure returns (uint256) {
+		if (a == 0) {
+			return 0;
+		}
+		return b / a; // This division is safe because of the early return in if-block.
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if2.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if2.sol
new file mode 100644
index 000000000..d614edb55
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if2.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	function test(uint256 a) public pure {
+		assert(simple_if(a) == 1); // should fail for a == 0
+	}
+
+	function simple_if(uint256 a) internal pure returns (uint256) {
+		if (a == 0) {
+			return 0;
+		}
+		return 1;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (89-114): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_array.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_array.sol
new file mode 100644
index 000000000..70cc1ed38
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_array.sol
@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	uint[] a;
+
+	constructor () {
+		a.push();
+		a.push();
+	}
+
+	function check() public {
+		require(a.length >= 2);
+		require(a[1] == 0);
+		conditional_store();
+		assert(a[1] == 1); // should fail;
+		assert(a[1] == 0); // should hold;
+	}
+
+	function conditional_store() internal {
+		if (a[1] == 0) {
+			return;
+		}
+		a[1] = 1;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (205-222): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_state_var.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_state_var.sol
new file mode 100644
index 000000000..5acc7fcbe
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_state_var.sol
@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	uint x;
+
+	function check() public {
+		require(x == 0);
+		conditional_increment();
+		assert(x == 1); // should fail;
+		assert(x == 0); // should hold;
+	}
+
+	function conditional_increment() internal {
+		if (x == 0) {
+			return;
+		}
+		x = 1;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (132-146): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct.sol
new file mode 100644
index 000000000..de3cfda1b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct.sol
@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	struct S {
+		uint x;
+	}
+	S s;
+
+	function check() public {
+		require(s.x == 0);
+		conditional_increment();
+		assert(s.x == 1); // should fail;
+		assert(s.x == 0); // should hold;
+	}
+
+	function conditional_increment() internal {
+		if (s.x == 0) {
+			return;
+		}
+		s.x = 1;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (156-172): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct_2.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct_2.sol
new file mode 100644
index 000000000..d709be0c7
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_struct_2.sol
@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	struct S {
+		uint x;
+	}
+	S s;
+
+	function check() public {
+		require(s.x == 0);
+		conditional_increment();
+		assert(s.x == 1); // should fail;
+		assert(s.x == 0); // should hold;
+	}
+
+	function conditional_increment() internal {
+		if (s.x == 0) {
+			return;
+		}
+		s = S(1);
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (156-172): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_tuple.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_tuple.sol
new file mode 100644
index 000000000..e1e6b323c
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/simple_if_tuple.sol
@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	uint x;
+	uint y;
+
+	function check() public {
+		require(x == 0);
+		require(y == 0);
+		conditional_increment();
+		assert(x == 0); // should fail;
+		assert(x == 1); // should fail;
+		assert(x == 2); // should hold;
+	}
+
+	function conditional_increment() internal {
+		if (x == 0) {
+			(x,y) = (2,2);
+			return;
+		}
+		(x,y) = (1,1);
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (160-174): BMC: Assertion violation happens here.
+// Warning 4661: (194-208): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/triple_nested_if.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/triple_nested_if.sol
new file mode 100644
index 000000000..38a5c852b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/triple_nested_if.sol
@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+    uint a;
+    uint b;
+    uint c;
+
+	function test() public view {
+		if (a == 0) {
+			if (b == 0) {
+				if (c == 0) {
+					return;
+				}
+			}
+		}
+		assert(a != 0 || b != 0 || c != 0);
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
diff --git a/test/libsolidity/smtCheckerTests/operators/division_6.sol b/test/libsolidity/smtCheckerTests/operators/division_6.sol
index 4dfd728c1..5672a9784 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_6.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_6.sol
@@ -1,14 +1,14 @@
 pragma experimental SMTChecker;
 contract C {
-	function mul(uint256 a, uint256 b) internal pure returns (uint256) {
+	function mul(uint256 a, uint256 b) public pure returns (uint256) {
 		if (a == 0) {
 			return 0;
 		}
-		// TODO remove when SMTChecker sees that this code is the `else` of the `return`.
-		require(a != 0);
 		uint256 c = a * b;
 		require(c / a == b);
 		return c;
 	}
 }
 // ----
+// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4281: (177-182): CHC: Division by zero happens here.
diff --git a/test/libsolidity/syntaxTests/array/invalidCopy/storage_to_storage_different_base.sol b/test/libsolidity/syntaxTests/array/invalidCopy/storage_to_storage_different_base.sol
new file mode 100644
index 000000000..b9f158697
--- /dev/null
+++ b/test/libsolidity/syntaxTests/array/invalidCopy/storage_to_storage_different_base.sol
@@ -0,0 +1,9 @@
+contract C {
+    byte[32] data1;
+    bytes2[10] data2;
+    function f() external {
+        data1 = data2;
+    }
+}
+// ----
+// TypeError 7407: (99-104): Type bytes2[10] storage ref is not implicitly convertible to expected type bytes1[32] storage ref.
diff --git a/test/libsolidity/syntaxTests/array/invalidCopy/storage_to_storage_different_base_2.sol b/test/libsolidity/syntaxTests/array/invalidCopy/storage_to_storage_different_base_2.sol
new file mode 100644
index 000000000..dabeb18e0
--- /dev/null
+++ b/test/libsolidity/syntaxTests/array/invalidCopy/storage_to_storage_different_base_2.sol
@@ -0,0 +1,9 @@
+contract C {
+    uint64[32] data1;
+    uint256[10] data2;
+    function f() external {
+        data1 = data2;
+    }
+}
+// ----
+// TypeError 7407: (102-107): Type uint256[10] storage ref is not implicitly convertible to expected type uint64[32] storage ref.
diff --git a/test/libsolidity/syntaxTests/array/invalidCopy/storage_to_storage_dynamic_to_static.sol b/test/libsolidity/syntaxTests/array/invalidCopy/storage_to_storage_dynamic_to_static.sol
new file mode 100644
index 000000000..1b3733a0b
--- /dev/null
+++ b/test/libsolidity/syntaxTests/array/invalidCopy/storage_to_storage_dynamic_to_static.sol
@@ -0,0 +1,9 @@
+contract C {
+    uint256[10] data1;
+    uint256[] data2;
+    function f() external {
+        data1 = data2;
+    }
+}
+// ----
+// TypeError 7407: (101-106): Type uint256[] storage ref is not implicitly convertible to expected type uint256[10] storage ref.
diff --git a/test/libsolidity/syntaxTests/array/invalidCopy/storage_to_storage_static_longer_to_shorter.sol b/test/libsolidity/syntaxTests/array/invalidCopy/storage_to_storage_static_longer_to_shorter.sol
new file mode 100644
index 000000000..95185d317
--- /dev/null
+++ b/test/libsolidity/syntaxTests/array/invalidCopy/storage_to_storage_static_longer_to_shorter.sol
@@ -0,0 +1,9 @@
+contract C {
+    uint256[10] data1;
+    uint256[18] data2;
+    function f() external {
+        data1 = data2;
+    }
+}
+// ----
+// TypeError 7407: (103-108): Type uint256[18] storage ref is not implicitly convertible to expected type uint256[10] storage ref.
diff --git a/test/libsolidity/syntaxTests/array/nested_calldata_memory.sol b/test/libsolidity/syntaxTests/array/nested_calldata_memory.sol
index 25be459a9..fb2ab2d94 100644
--- a/test/libsolidity/syntaxTests/array/nested_calldata_memory.sol
+++ b/test/libsolidity/syntaxTests/array/nested_calldata_memory.sol
@@ -10,4 +10,3 @@ contract Test {
 }
 
 // ----
-// UnimplementedFeatureError: Copying nested dynamic calldata arrays to memory is not implemented in the old code generator.
diff --git a/test/libsolidity/syntaxTests/array/nested_calldata_memory2.sol b/test/libsolidity/syntaxTests/array/nested_calldata_memory2.sol
index 2aed58103..ad09877c4 100644
--- a/test/libsolidity/syntaxTests/array/nested_calldata_memory2.sol
+++ b/test/libsolidity/syntaxTests/array/nested_calldata_memory2.sol
@@ -10,4 +10,3 @@ contract Test {
 }
 
 // ----
-// UnimplementedFeatureError: Copying nested dynamic calldata arrays to memory is not implemented in the old code generator.
diff --git a/test/libsolidity/syntaxTests/array/nested_calldata_memory3.sol b/test/libsolidity/syntaxTests/array/nested_calldata_memory3.sol
index 94008ae59..d7f0133fc 100644
--- a/test/libsolidity/syntaxTests/array/nested_calldata_memory3.sol
+++ b/test/libsolidity/syntaxTests/array/nested_calldata_memory3.sol
@@ -10,4 +10,3 @@ contract Test {
 }
 
 // ----
-// UnimplementedFeatureError: Copying nested dynamic calldata arrays to memory is not implemented in the old code generator.
diff --git a/test/libsolidity/syntaxTests/types/bytesNN_bitnot.sol b/test/libsolidity/syntaxTests/types/bytesNN_bitnot.sol
new file mode 100644
index 000000000..b926beeb1
--- /dev/null
+++ b/test/libsolidity/syntaxTests/types/bytesNN_bitnot.sol
@@ -0,0 +1,5 @@
+contract C {
+  bytes32 b32 = ~bytes32(hex"ff");
+  bytes32 b25 = ~bytes25(hex"ff");
+  bytes25 b8 = ~bytes8(hex"ff");
+}
diff --git a/test/libsolidity/syntaxTests/types/hex_literal_bitnot.sol b/test/libsolidity/syntaxTests/types/hex_literal_bitnot.sol
new file mode 100644
index 000000000..5fbfa919a
--- /dev/null
+++ b/test/libsolidity/syntaxTests/types/hex_literal_bitnot.sol
@@ -0,0 +1,5 @@
+contract C {
+    bytes32 b = ~hex"00ff11";
+}
+// ----
+// TypeError 4907: (29-41): Unary operator ~ cannot be applied to type literal_string hex"00ff11"
diff --git a/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp b/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp
index 10c8af230..7d50e1527 100644
--- a/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp
+++ b/test/tools/yulInterpreter/EwasmBuiltinInterpreter.cpp
@@ -154,6 +154,20 @@ u256 EwasmBuiltinInterpreter::evalBuiltin(
 	}
 	else if (fun == "i32.drop" || fun == "i64.drop" || fun == "nop")
 		return {};
+	else if (fun == "i32.select")
+	{
+		if ((arg.at(2) & 0xffffffff) == 0)
+			return arg.at(1);
+		else
+			return arg.at(0);
+	}
+	else if (fun == "i64.select")
+	{
+		if ((arg.at(2) & 0xffffffffffffffff) == 0)
+			return arg.at(1);
+		else
+			return arg.at(0);
+	}
 	else if (fun == "i32.wrap_i64")
 		return arg.at(0) & uint32_t(-1);
 	else if (fun == "i64.extend_i32_u")