Merge pull request #13007 from ethereum/develop

Merge develop into breaking.
2023-10-03 13:03:40 +00:00 · 2022-05-11 16:39:24 +02:00 · 2022-05-11 16:39:24 +02:00 · a137d42094
commit a137d42094
parent a433511128 9f6d3deaea
103 changed files with 2338 additions and 840 deletions
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@ -9,20 +9,20 @@ version: 2.1
 parameters:
  ubuntu-2004-docker-image:
    type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-11
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:9928dc357829e475e8729c62a1c2d495dbb41cb9fe4c4b115a5568be8e1ed69e"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-12
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:5087cc068b48787e89887804e632120b3e65bc5c25086bdf7b152be4fe5fc9ba"
  ubuntu-2004-clang-docker-image:
    type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-11
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:72fb9574c90e8ef908dce4c9dd9788ff4de708b504d970cd9146eed8911c313e"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-12
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:7f53f1bc3d89bdfb0725f604efbbec570d80ffa9b731b47a4842f4e286de0355"
  ubuntu-1604-clang-ossfuzz-docker-image:
    type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-16
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:fe54d8e5409827d43edb0dc8ad0d9e4232a675050ceb271c873b73e5ee267938"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-17
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:85b298c763adf5c516238246beb283640eb555e79e7ad6a8e7a6c9ed47ef6324"
  emscripten-docker-image:
    type: string
-    # solbuildpackpusher/solidity-buildpack-deps:emscripten-9
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d51534dfdd05ece86f69ed7beafd68c15b88606da00a4b7fe2873ccfbd0dce24"
+    # solbuildpackpusher/solidity-buildpack-deps:emscripten-10
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:bd23831e0025e35a106005b4ac06cb3618f690bfa2833a5881b573c02d35d9fc"
  evm-version:
    type: string
    default: london
@ -1280,6 +1280,15 @@ jobs:
      - run:
          name: "Run soltest"
          command: .circleci/soltest.ps1
+      - run:
+          name: Install LSP test dependencies
+          command: python -m pip install --user deepdiff colorama
+      - run:
+          name: Inspect lsp.py
+          command: Get-Content ./test/lsp.py
+      - run:
+          name: Executing solc LSP test suite
+          command: python ./test/lsp.py .\build\solc\Release\solc.exe
      - store_test_results: *store_test_results
      - store_artifacts: *artifacts_test_results
      - gitter_notify_failure_unless_pr
--- a/.circleci/osx_install_dependencies.sh
+++ b/.circleci/osx_install_dependencies.sh
@ -61,11 +61,11 @@ then
  ./scripts/install_obsolete_jsoncpp_1_7_4.sh

  # z3
-  z3_version="4.8.14"
+  z3_version="4.8.16"
  z3_dir="z3-${z3_version}-x64-osx-10.16"
  z3_package="${z3_dir}.zip"
  wget "https://github.com/Z3Prover/z3/releases/download/z3-${z3_version}/${z3_package}"
-  validate_checksum "$z3_package" 1341671670e0c4e72da80815128a68975ee90816d50ceaf6bd820f06babe2cfd
+  validate_checksum "$z3_package" 71ed7b6d10c01198187df72cccb8eb6de6d9aa2bf9557b3dd052032524b598a5
  unzip "$z3_package"
  rm "$z3_package"
  cp "${z3_dir}/bin/libz3.a" /usr/local/lib
--- a/.circleci/soltest.sh
+++ b/.circleci/soltest.sh
@ -74,7 +74,7 @@ do
    BOOST_TEST_ARGS_RUN=(
        "--color_output=no"
        "--show_progress=yes"
-        "--logger=JUNIT,error,test_results/$(get_logfile_basename "$run").xml"
+        "--logger=JUNIT,error,test_results/$(get_logfile_basename "$((CPUs * CIRCLE_NODE_INDEX + run))").xml"
        "${BOOST_TEST_ARGS[@]}"
    )
    SOLTEST_ARGS=("--evm-version=$EVM" "${SOLTEST_FLAGS[@]}")
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@ -65,7 +65,7 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens

 include(EthOptions)
 configure_project(TESTS)
-set(LATEST_Z3_VERSION "4.8.14")
+set(LATEST_Z3_VERSION "4.8.16")
 set(MINIMUM_Z3_VERSION "4.8.0")
 find_package(Z3)
 if (${Z3_FOUND})
--- a/Changelog.md
+++ b/Changelog.md
@ -20,11 +20,14 @@ Compiler Features:
 * Assembly-Json: Export: Include source list in `sourceList` field.
 * Commandline Interface: option ``--pretty-json`` works also with the following options: ``--abi``, ``--asm-json``, ``--ast-compact-json``, ``--devdoc``, ``--storage-layout``, ``--userdoc``.
 * SMTChecker: Support ``abi.encodeCall`` taking into account the called selector.
+ * Language Server: Allow full filesystem access to language server.


 Bugfixes:
+ * Type Checker: Properly check restrictions of ``using ... global`` in conjunction with libraries.
 * Assembly-Json: Fix assembly json export to store jump types of operations in `jumpType` field instead of `value`.
 * TypeChecker: Convert parameters of function type to how they would be called for ``abi.encodeCall``.
+* View Pure Checker: Mark ``returndatasize`` and ``returndatacopy`` as view to disallow them in inline assembly blocks in pure functions.



--- a/docs/contracts/functions.rst
+++ b/docs/contracts/functions.rst
@ -318,12 +318,13 @@ will consume more gas than the 2300 gas stipend:
 - Sending Ether

 .. warning::
-    Contracts that receive Ether directly (without a function call, i.e. using ``send`` or ``transfer``)
-    but do not define a receive Ether function or a payable fallback function
-    throw an exception, sending back the Ether (this was different
-    before Solidity v0.4.0). So if you want your contract to receive Ether,
+    When Ether is sent directly to a contract (without a function call, i.e. sender uses ``send`` or ``transfer``)
+    but the receiving contract does not define a receive Ether function or a payable fallback function,
+    an exception will be thrown, sending back the Ether (this was different
+    before Solidity v0.4.0). If you want your contract to receive Ether,
    you have to implement a receive Ether function (using payable fallback functions for receiving Ether is
-    not recommended, since it would not fail on interface confusions).
+    not recommended, since the fallback is invoked and would not fail for interface confusions
+    on the part of the sender).


 .. warning::
--- a/docs/examples/voting.rst
+++ b/docs/examples/voting.rst
@ -109,6 +109,7 @@ of votes.
        function delegate(address to) external {
            // assigns reference
            Voter storage sender = voters[msg.sender];
+            require(sender.weight != 0, "You have no right to vote");
            require(!sender.voted, "You already voted.");

            require(to != msg.sender, "Self-delegation is disallowed.");
@ -132,7 +133,7 @@ of votes.
            // modifies `voters[msg.sender].voted`
            Voter storage delegate_ = voters[to];

-            // Voters cannot delegate to wallets that cannot vote.
+            // Voters cannot delegate to accounts that cannot vote.
            require(delegate_.weight >= 1);
            sender.voted = true;
            sender.delegate = to;
--- a/libevmasm/SemanticInformation.cpp
+++ b/libevmasm/SemanticInformation.cpp
@ -481,6 +481,8 @@ bool SemanticInformation::invalidInPureFunctions(Instruction _instruction)
 	case Instruction::EXTCODESIZE:
 	case Instruction::EXTCODECOPY:
 	case Instruction::EXTCODEHASH:
+	case Instruction::RETURNDATASIZE:
+	case Instruction::RETURNDATACOPY:
 	case Instruction::BLOCKHASH:
 	case Instruction::COINBASE:
 	case Instruction::TIMESTAMP:
--- a/libsolidity/CMakeLists.txt
+++ b/libsolidity/CMakeLists.txt
@ -176,3 +176,4 @@ set(sources

 add_library(solidity ${sources})
 target_link_libraries(solidity PUBLIC yul evmasm langutil smtutil solutil Boost::boost fmt::fmt-header-only)
+
--- a/libsolidity/analysis/TypeChecker.cpp
+++ b/libsolidity/analysis/TypeChecker.cpp
@ -3641,11 +3641,36 @@ void TypeChecker::endVisit(Literal const& _literal)

 void TypeChecker::endVisit(UsingForDirective const& _usingFor)
 {
+	if (_usingFor.global())
+	{
+		if (m_currentContract || !_usingFor.typeName())
+		{
+			solAssert(m_errorReporter.hasErrors());
+			return;
+		}
+		solAssert(_usingFor.typeName()->annotation().type);
+		if (Declaration const* typeDefinition = _usingFor.typeName()->annotation().type->typeDefinition())
+		{
+			if (typeDefinition->scope() != m_currentSourceUnit)
+				m_errorReporter.typeError(
+					4117_error,
+					_usingFor.location(),
+					"Can only use \"global\" with types defined in the same source unit at file level."
+				);
+		}
+		else
+			m_errorReporter.typeError(
+				8841_error,
+				_usingFor.location(),
+				"Can only use \"global\" with user-defined types."
+			);
+	}
+
 	if (!_usingFor.usesBraces())
 	{
 		solAssert(_usingFor.functionsOrLibrary().size() == 1);
 		ContractDefinition const* library = dynamic_cast<ContractDefinition const*>(
-				_usingFor.functionsOrLibrary().front()->annotation().referencedDeclaration
+			_usingFor.functionsOrLibrary().front()->annotation().referencedDeclaration
 		);
 		solAssert(library && library->isLibrary());
 		// No type checking for libraries
@ -3665,28 +3690,6 @@ void TypeChecker::endVisit(UsingForDirective const& _usingFor)
 	);
 	solAssert(normalizedType);

-	if (_usingFor.global())
-	{
-		if (m_currentContract)
-			solAssert(m_errorReporter.hasErrors());
-		if (Declaration const* typeDefinition = _usingFor.typeName()->annotation().type->typeDefinition())
-		{
-			if (typeDefinition->scope() != m_currentSourceUnit)
-				m_errorReporter.typeError(
-					4117_error,
-					_usingFor.location(),
-					"Can only use \"global\" with types defined in the same source unit at file level."
-				);
-		}
-		else
-			m_errorReporter.typeError(
-				8841_error,
-				_usingFor.location(),
-				"Can only use \"global\" with user-defined types."
-			);
-	}
-
-
 	for (ASTPointer<IdentifierPath> const& path: _usingFor.functionsOrLibrary())
 	{
 		solAssert(path->annotation().referencedDeclaration);
--- a/libsolidity/lsp/FileRepository.cpp
+++ b/libsolidity/lsp/FileRepository.cpp
@ -17,48 +17,130 @@
 // SPDX-License-Identifier: GPL-3.0

 #include <libsolidity/lsp/FileRepository.h>
+#include <libsolidity/lsp/Utils.h>
+
+#include <libsolutil/StringUtils.h>
+#include <libsolutil/CommonIO.h>
+
+#include <range/v3/range/conversion.hpp>
+#include <range/v3/view/transform.hpp>
+
+#include <regex>

 using namespace std;
 using namespace solidity;
 using namespace solidity::lsp;
+using namespace solidity::frontend;

-namespace
-{
+using solidity::util::readFileAsString;
+using solidity::util::joinHumanReadable;

-string stripFilePrefix(string const& _path)
+FileRepository::FileRepository(boost::filesystem::path _basePath): m_basePath(std::move(_basePath))
 {
-	if (_path.find("file://") == 0)
-		return _path.substr(7);
-	else
-		return _path;
 }

-}
-
-string FileRepository::sourceUnitNameToClientPath(string const& _sourceUnitName) const
+string FileRepository::sourceUnitNameToUri(string const& _sourceUnitName) const
 {
-	if (m_sourceUnitNamesToClientPaths.count(_sourceUnitName))
-		return m_sourceUnitNamesToClientPaths.at(_sourceUnitName);
+	regex const windowsDriveLetterPath("^[a-zA-Z]:/");
+
+	if (m_sourceUnitNamesToUri.count(_sourceUnitName))
+		return m_sourceUnitNamesToUri.at(_sourceUnitName);
 	else if (_sourceUnitName.find("file://") == 0)
 		return _sourceUnitName;
+	else if (regex_search(_sourceUnitName, windowsDriveLetterPath))
+		return "file:///" + _sourceUnitName;
+	else if (_sourceUnitName.find("/") == 0)
+		return "file://" + _sourceUnitName;
 	else
-		return "file://" + (m_fileReader.basePath() / _sourceUnitName).generic_string();
+		return "file://" + m_basePath.generic_string() + "/" + _sourceUnitName;
 }

-string FileRepository::clientPathToSourceUnitName(string const& _path) const
+string FileRepository::uriToSourceUnitName(string const& _path) const
 {
-	return m_fileReader.cliPathToSourceUnitName(stripFilePrefix(_path));
+	return stripFileUriSchemePrefix(_path);
 }

-map<string, string> const& FileRepository::sourceUnits() const
-{
-	return m_fileReader.sourceUnits();
-}
-
-void FileRepository::setSourceByClientPath(string const& _uri, string _text)
+void FileRepository::setSourceByUri(string const& _uri, string _source)
 {
 	// This is needed for uris outside the base path. It can lead to collisions,
 	// but we need to mostly rewrite this in a future version anyway.
-	m_sourceUnitNamesToClientPaths.emplace(clientPathToSourceUnitName(_uri), _uri);
-	m_fileReader.addOrUpdateFile(stripFilePrefix(_uri), move(_text));
+	auto sourceUnitName = uriToSourceUnitName(_uri);
+	m_sourceUnitNamesToUri.emplace(sourceUnitName, _uri);
+	m_sourceCodes[sourceUnitName] = std::move(_source);
 }
+
+frontend::ReadCallback::Result FileRepository::readFile(string const& _kind, string const& _sourceUnitName)
+{
+	solAssert(
+		_kind == ReadCallback::kindString(ReadCallback::Kind::ReadFile),
+		"ReadFile callback used as callback kind " + _kind
+	);
+
+	try
+	{
+		// File was read already. Use local store.
+		if (m_sourceCodes.count(_sourceUnitName))
+			return ReadCallback::Result{true, m_sourceCodes.at(_sourceUnitName)};
+
+		string const strippedSourceUnitName = stripFileUriSchemePrefix(_sourceUnitName);
+
+		if (
+			boost::filesystem::path(strippedSourceUnitName).has_root_path() &&
+			boost::filesystem::exists(strippedSourceUnitName)
+		)
+		{
+			auto contents = readFileAsString(strippedSourceUnitName);
+			solAssert(m_sourceCodes.count(_sourceUnitName) == 0, "");
+			m_sourceCodes[_sourceUnitName] = contents;
+			return ReadCallback::Result{true, move(contents)};
+		}
+
+		vector<boost::filesystem::path> candidates;
+		vector<reference_wrapper<boost::filesystem::path>> prefixes = {m_basePath};
+		prefixes += (m_includePaths | ranges::to<vector<reference_wrapper<boost::filesystem::path>>>);
+
+		auto const pathToQuotedString = [](boost::filesystem::path const& _path) { return "\"" + _path.string() + "\""; };
+
+		for (auto const& prefix: prefixes)
+		{
+			boost::filesystem::path canonicalPath = boost::filesystem::path(prefix) / boost::filesystem::path(strippedSourceUnitName);
+
+			if (boost::filesystem::exists(canonicalPath))
+				candidates.push_back(move(canonicalPath));
+		}
+
+		if (candidates.empty())
+			return ReadCallback::Result{
+				false,
+				"File not found. Searched the following locations: " +
+				joinHumanReadable(prefixes | ranges::views::transform(pathToQuotedString), ", ") +
+				"."
+			};
+
+		if (candidates.size() >= 2)
+			return ReadCallback::Result{
+				false,
+				"Ambiguous import. "
+				"Multiple matching files found inside base path and/or include paths: " +
+				joinHumanReadable(candidates | ranges::views::transform(pathToQuotedString), ", ") +
+				"."
+			};
+
+		if (!boost::filesystem::is_regular_file(candidates[0]))
+			return ReadCallback::Result{false, "Not a valid file."};
+
+		auto contents = readFileAsString(candidates[0]);
+		solAssert(m_sourceCodes.count(_sourceUnitName) == 0, "");
+		m_sourceCodes[_sourceUnitName] = contents;
+		return ReadCallback::Result{true, move(contents)};
+	}
+	catch (std::exception const& _exception)
+	{
+		return ReadCallback::Result{false, "Exception in read callback: " + boost::diagnostic_information(_exception)};
+	}
+	catch (...)
+	{
+		return ReadCallback::Result{false, "Unknown exception in read callback: " + boost::current_exception_diagnostic_information()};
+	}
+}
+
--- a/libsolidity/lsp/FileRepository.h
+++ b/libsolidity/lsp/FileRepository.h
@ -28,26 +28,42 @@ namespace solidity::lsp
 class FileRepository
 {
 public:
-	explicit FileRepository(boost::filesystem::path const& _basePath):
-		m_fileReader(_basePath) {}
+	explicit FileRepository(boost::filesystem::path _basePath);

-	boost::filesystem::path const& basePath() const { return m_fileReader.basePath(); }
+	boost::filesystem::path const& basePath() const { return m_basePath; }

 	/// Translates a compiler-internal source unit name to an LSP client path.
-	std::string sourceUnitNameToClientPath(std::string const& _sourceUnitName) const;
-	/// Translates an LSP client path into a compiler-internal source unit name.
-	std::string clientPathToSourceUnitName(std::string const& _uri) const;
+	std::string sourceUnitNameToUri(std::string const& _sourceUnitName) const;
+
+	/// Translates an LSP file URI into a compiler-internal source unit name.
+	std::string uriToSourceUnitName(std::string const& _uri) const;

 	/// @returns all sources by their compiler-internal source unit name.
-	std::map<std::string, std::string> const& sourceUnits() const;
-	/// Changes the source identified by the LSP client path _uri to _text.
-	void setSourceByClientPath(std::string const& _uri, std::string _text);
+	StringMap const& sourceUnits() const noexcept { return m_sourceCodes; }

-	frontend::ReadCallback::Callback reader() { return m_fileReader.reader(); }
+	/// Changes the source identified by the LSP client path _uri to _text.
+	void setSourceByUri(std::string const& _uri, std::string _text);
+
+	void addOrUpdateFile(boost::filesystem::path const& _path, frontend::SourceCode _source);
+	void setSourceUnits(StringMap _sources);
+	frontend::ReadCallback::Result readFile(std::string const& _kind, std::string const& _sourceUnitName);
+	frontend::ReadCallback::Callback reader()
+	{
+		return [this](std::string const& _kind, std::string const& _path) { return readFile(_kind, _path); };
+	}

 private:
-	std::map<std::string, std::string> m_sourceUnitNamesToClientPaths;
-	frontend::FileReader m_fileReader;
+	/// Base path without URI scheme.
+	boost::filesystem::path m_basePath;
+
+	/// Additional directories used for resolving relative paths in imports.
+	std::vector<boost::filesystem::path> m_includePaths;
+
+	/// Mapping of source unit names to their URIs as understood by the client.
+	StringMap m_sourceUnitNamesToUri;
+
+	/// Mapping of source unit names to their file content.
+	StringMap m_sourceCodes;
 };

 }
--- a/libsolidity/lsp/HandlerBase.cpp
+++ b/libsolidity/lsp/HandlerBase.cpp
@ -47,7 +47,7 @@ Json::Value HandlerBase::toJson(SourceLocation const& _location) const
 {
 	solAssert(_location.sourceName);
 	Json::Value item = Json::objectValue;
-	item["uri"] = fileRepository().sourceUnitNameToClientPath(*_location.sourceName);
+	item["uri"] = fileRepository().sourceUnitNameToUri(*_location.sourceName);
 	item["range"] = toRange(_location);
 	return item;
 }
@ -55,7 +55,7 @@ Json::Value HandlerBase::toJson(SourceLocation const& _location) const
 pair<string, LineColumn> HandlerBase::extractSourceUnitNameAndLineColumn(Json::Value const& _args) const
 {
 	string const uri = _args["textDocument"]["uri"].asString();
-	string const sourceUnitName = fileRepository().clientPathToSourceUnitName(uri);
+	string const sourceUnitName = fileRepository().uriToSourceUnitName(uri);
 	if (!fileRepository().sourceUnits().count(sourceUnitName))
 		BOOST_THROW_EXCEPTION(
 			RequestError(ErrorCode::RequestFailed) <<
--- a/libsolidity/lsp/LanguageServer.cpp
+++ b/libsolidity/lsp/LanguageServer.cpp
@ -37,8 +37,6 @@
 #include <boost/filesystem.hpp>
 #include <boost/algorithm/string/predicate.hpp>

-#include <fmt/format.h>
-
 #include <ostream>
 #include <string>

@ -114,9 +112,9 @@ void LanguageServer::compile()
 	swap(oldRepository, m_fileRepository);

 	for (string const& fileName: m_openFiles)
-		m_fileRepository.setSourceByClientPath(
+		m_fileRepository.setSourceByUri(
 			fileName,
-			oldRepository.sourceUnits().at(oldRepository.clientPathToSourceUnitName(fileName))
+			oldRepository.sourceUnits().at(oldRepository.uriToSourceUnitName(fileName))
 		);

 	// TODO: optimize! do not recompile if nothing has changed (file(s) not flagged dirty).
@ -178,7 +176,7 @@ void LanguageServer::compileAndUpdateDiagnostics()
 	for (auto&& [sourceUnitName, diagnostics]: diagnosticsBySourceUnit)
 	{
 		Json::Value params;
-		params["uri"] = m_fileRepository.sourceUnitNameToClientPath(sourceUnitName);
+		params["uri"] = m_fileRepository.sourceUnitNameToUri(sourceUnitName);
 		if (!diagnostics.empty())
 			m_nonemptyDiagnostics.insert(sourceUnitName);
 		params["diagnostics"] = move(diagnostics);
@ -252,13 +250,12 @@ void LanguageServer::handleInitialize(MessageID _id, Json::Value const& _args)
 			ErrorCode::InvalidParams,
 			"rootUri only supports file URI scheme."
 		);
-
-		rootPath = rootPath.substr(7);
+		rootPath = stripFileUriSchemePrefix(rootPath);
 	}
 	else if (Json::Value rootPath = _args["rootPath"])
 		rootPath = rootPath.asString();

-	m_fileRepository = FileRepository(boost::filesystem::path(rootPath));
+	m_fileRepository = FileRepository(rootPath);
 	if (_args["initializationOptions"].isObject())
 		changeConfiguration(_args["initializationOptions"]);

@ -309,7 +306,7 @@ void LanguageServer::handleTextDocumentDidOpen(Json::Value const& _args)
 	string text = _args["textDocument"]["text"].asString();
 	string uri = _args["textDocument"]["uri"].asString();
 	m_openFiles.insert(uri);
-	m_fileRepository.setSourceByClientPath(uri, move(text));
+	m_fileRepository.setSourceByUri(uri, move(text));
 	compileAndUpdateDiagnostics();
 }

@ -327,7 +324,7 @@ void LanguageServer::handleTextDocumentDidChange(Json::Value const& _args)
 			"Invalid content reference."
 		);

-		string const sourceUnitName = m_fileRepository.clientPathToSourceUnitName(uri);
+		string const sourceUnitName = m_fileRepository.uriToSourceUnitName(uri);
 		lspAssert(
 			m_fileRepository.sourceUnits().count(sourceUnitName),
 			ErrorCode::RequestFailed,
@ -348,7 +345,7 @@ void LanguageServer::handleTextDocumentDidChange(Json::Value const& _args)
 			buffer.replace(static_cast<size_t>(change->start), static_cast<size_t>(change->end - change->start), move(text));
 			text = move(buffer);
 		}
-		m_fileRepository.setSourceByClientPath(uri, move(text));
+		m_fileRepository.setSourceByUri(uri, move(text));
 	}

 	compileAndUpdateDiagnostics();
--- a/libsolidity/lsp/LanguageServer.h
+++ b/libsolidity/lsp/LanguageServer.h
@ -92,7 +92,7 @@ private:
 	Transport& m_client;
 	std::map<std::string, MessageHandler> m_handlers;

-	/// Set of files known to be open by the client.
+	/// Set of files (names in URI form) known to be open by the client.
 	std::set<std::string> m_openFiles;
 	/// Set of source unit names for which we sent diagnostics to the client in the last iteration.
 	std::set<std::string> m_nonemptyDiagnostics;
--- a/libsolidity/lsp/Transport.cpp
+++ b/libsolidity/lsp/Transport.cpp
@ -22,31 +22,25 @@
 #include <libsolutil/CommonIO.h>
 #include <liblangutil/Exceptions.h>

+#include <fmt/format.h>
+
 #include <boost/algorithm/string.hpp>

 #include <iostream>
 #include <sstream>
+#include <string>
+
+
+#if defined(_WIN32)
+#include <io.h>
+#include <fcntl.h>
+#endif

 using namespace std;
 using namespace solidity::lsp;

-IOStreamTransport::IOStreamTransport(istream& _in, ostream& _out):
-	m_input{_in},
-	m_output{_out}
-{
-}
-
-IOStreamTransport::IOStreamTransport():
-	IOStreamTransport(cin, cout)
-{
-}
-
-bool IOStreamTransport::closed() const noexcept
-{
-	return m_input.eof();
-}
-
-optional<Json::Value> IOStreamTransport::receive()
+// {{{ Transport
+optional<Json::Value> Transport::receive()
 {
 	auto const headers = parseHeaders();
 	if (!headers)
@ -61,7 +55,7 @@ optional<Json::Value> IOStreamTransport::receive()
 		return nullopt;
 	}

-	string const data = util::readBytes(m_input, stoul(headers->at("content-length")));
+	string const data = readBytes(stoul(headers->at("content-length")));

 	Json::Value jsonMessage;
 	string jsonParsingErrors;
@ -75,29 +69,6 @@ optional<Json::Value> IOStreamTransport::receive()
 	return {move(jsonMessage)};
 }

-void IOStreamTransport::notify(string _method, Json::Value _message)
-{
-	Json::Value json;
-	json["method"] = move(_method);
-	json["params"] = move(_message);
-	send(move(json));
-}
-
-void IOStreamTransport::reply(MessageID _id, Json::Value _message)
-{
-	Json::Value json;
-	json["result"] = move(_message);
-	send(move(json), _id);
-}
-
-void IOStreamTransport::error(MessageID _id, ErrorCode _code, string _message)
-{
-	Json::Value json;
-	json["error"]["code"] = static_cast<int>(_code);
-	json["error"]["message"] = move(_message);
-	send(move(json), _id);
-}
-
 void Transport::trace(std::string _message, Json::Value _extra)
 {
 	if (m_logTrace != TraceValue::Off)
@ -110,30 +81,13 @@ void Transport::trace(std::string _message, Json::Value _extra)
 	}
 }

-void IOStreamTransport::send(Json::Value _json, MessageID _id)
-{
-	solAssert(_json.isObject());
-	_json["jsonrpc"] = "2.0";
-	if (_id != Json::nullValue)
-		_json["id"] = _id;
-
-	string const jsonString = solidity::util::jsonCompactPrint(_json);
-
-	m_output << "Content-Length: " << jsonString.size() << "\r\n";
-	m_output << "\r\n";
-	m_output << jsonString;
-
-	m_output.flush();
-}
-
-optional<map<string, string>> IOStreamTransport::parseHeaders()
+optional<map<string, string>> Transport::parseHeaders()
 {
 	map<string, string> headers;

 	while (true)
 	{
-		string line;
-		getline(m_input, line);
+		auto line = getline();
 		if (boost::trim_copy(line).empty())
 			break;

@ -141,13 +95,127 @@ optional<map<string, string>> IOStreamTransport::parseHeaders()
 		if (delimiterPos == string::npos)
 			return nullopt;

-		string name = boost::to_lower_copy(line.substr(0, delimiterPos));
-		string value = line.substr(delimiterPos + 1);
-		if (!headers.emplace(
-			boost::trim_copy(name),
-			boost::trim_copy(value)
-		).second)
+		auto const name = boost::to_lower_copy(line.substr(0, delimiterPos));
+		auto const value = line.substr(delimiterPos + 1);
+		if (!headers.emplace(boost::trim_copy(name), boost::trim_copy(value)).second)
 			return nullopt;
 	}
 	return {move(headers)};
 }
+
+void Transport::notify(string _method, Json::Value _message)
+{
+	Json::Value json;
+	json["method"] = move(_method);
+	json["params"] = move(_message);
+	send(move(json));
+}
+
+void Transport::reply(MessageID _id, Json::Value _message)
+{
+	Json::Value json;
+	json["result"] = move(_message);
+	send(move(json), _id);
+}
+
+void Transport::error(MessageID _id, ErrorCode _code, string _message)
+{
+	Json::Value json;
+	json["error"]["code"] = static_cast<int>(_code);
+	json["error"]["message"] = move(_message);
+	send(move(json), _id);
+}
+
+void Transport::send(Json::Value _json, MessageID _id)
+{
+	solAssert(_json.isObject());
+	_json["jsonrpc"] = "2.0";
+	if (_id != Json::nullValue)
+		_json["id"] = _id;
+
+	// Trailing CRLF only for easier readability.
+	string const jsonString = solidity::util::jsonCompactPrint(_json);
+
+	writeBytes(fmt::format("Content-Length: {}\r\n\r\n", jsonString.size()));
+	writeBytes(jsonString);
+	flushOutput();
+}
+// }}}
+
+// {{{ IOStreamTransport
+IOStreamTransport::IOStreamTransport(istream& _in, ostream& _out):
+	m_input{_in},
+	m_output{_out}
+{
+}
+
+bool IOStreamTransport::closed() const noexcept
+{
+	return m_input.eof();
+}
+
+std::string IOStreamTransport::readBytes(size_t _length)
+{
+	return util::readBytes(m_input, _length);
+}
+
+std::string IOStreamTransport::getline()
+{
+	string line;
+	std::getline(m_input, line);
+	return line;
+}
+
+void IOStreamTransport::writeBytes(std::string_view _data)
+{
+	m_output.write(_data.data(), static_cast<std::streamsize>(_data.size()));
+}
+
+void IOStreamTransport::flushOutput()
+{
+	m_output.flush();
+}
+// }}}
+
+// {{{ StdioTransport
+StdioTransport::StdioTransport()
+{
+	#if defined(_WIN32)
+	// Attempt to change the modes of stdout from text to binary.
+	setmode(fileno(stdout), O_BINARY);
+	#endif
+}
+
+bool StdioTransport::closed() const noexcept
+{
+	return feof(stdin);
+}
+
+std::string StdioTransport::readBytes(size_t _byteCount)
+{
+	std::string buffer;
+	buffer.resize(_byteCount);
+	auto const n = fread(buffer.data(), 1, _byteCount, stdin);
+	if (n < _byteCount)
+		buffer.resize(n);
+	return buffer;
+}
+
+std::string StdioTransport::getline()
+{
+	std::string line;
+	std::getline(std::cin, line);
+	return line;
+}
+
+void StdioTransport::writeBytes(std::string_view _data)
+{
+	auto const bytesWritten = fwrite(_data.data(), 1, _data.size(), stdout);
+	solAssert(bytesWritten == _data.size());
+}
+
+void StdioTransport::flushOutput()
+{
+	fflush(stdout);
+}
+// }}}
--- a/libsolidity/lsp/Transport.h
+++ b/libsolidity/lsp/Transport.h
@ -91,20 +91,44 @@ class Transport
 public:
 	virtual ~Transport() = default;

+	std::optional<Json::Value> receive();
+	void notify(std::string _method, Json::Value _params);
+	void reply(MessageID _id, Json::Value _result);
+	void error(MessageID _id, ErrorCode _code, std::string _message);
+
 	virtual bool closed() const noexcept = 0;
-	virtual std::optional<Json::Value> receive() = 0;
-	virtual void notify(std::string _method, Json::Value _params) = 0;
-	virtual void reply(MessageID _id, Json::Value _result) = 0;
-	virtual void error(MessageID _id, ErrorCode _code, std::string _message) = 0;

 	void trace(std::string _message, Json::Value _extra = Json::nullValue);

 	TraceValue traceValue() const noexcept { return m_logTrace; }
 	void setTrace(TraceValue _value) noexcept { m_logTrace = _value; }

-
 private:
 	TraceValue m_logTrace = TraceValue::Off;
+
+protected:
+	/// Reads from the transport and parses the headers until the beginning
+	/// of the contents.
+	std::optional<std::map<std::string, std::string>> parseHeaders();
+
+	/// Consumes exactly @p _byteCount bytes, as needed for consuming
+	/// the message body from the transport line.
+	virtual std::string readBytes(size_t _byteCount) = 0;
+
+	// Mimmicks std::getline() on this Transport API.
+	virtual std::string getline() = 0;
+
+	/// Writes the given payload @p _data to transport.
+	/// This call may or may not buffer.
+	virtual void writeBytes(std::string_view _data) = 0;
+
+	/// Ensures transport output is flushed.
+	virtual void flushOutput() = 0;
+
+	/// Sends an arbitrary raw message to the client.
+	///
+	/// Used by the notify/reply/error function family.
+	virtual void send(Json::Value _message, MessageID _id = Json::nullValue);
 };

 /**
@ -119,27 +143,34 @@ public:
 	/// @param _out for example std::cout (stdout)
 	IOStreamTransport(std::istream& _in, std::ostream& _out);

-	// Constructs a JSON transport using standard I/O streams.
-	IOStreamTransport();
-
 	bool closed() const noexcept override;
-	std::optional<Json::Value> receive() override;
-	void notify(std::string _method, Json::Value _params) override;
-	void reply(MessageID _id, Json::Value _result) override;
-	void error(MessageID _id, ErrorCode _code, std::string _message) override;

 protected:
-	/// Sends an arbitrary raw message to the client.
-	///
-	/// Used by the notify/reply/error function family.
-	virtual void send(Json::Value _message, MessageID _id = Json::nullValue);
-
-	/// Parses header section from the client including message-delimiting empty line.
-	std::optional<std::map<std::string, std::string>> parseHeaders();
+	std::string readBytes(size_t _byteCount) override;
+	std::string getline() override;
+	void writeBytes(std::string_view _data) override;
+	void flushOutput() override;

 private:
 	std::istream& m_input;
 	std::ostream& m_output;
 };

+/**
+ * Standard I/O transport Layer utilizing stdin/stdout for communication.
+ */
+class StdioTransport: public Transport
+{
+public:
+	StdioTransport();
+
+	bool closed() const noexcept override;
+
+protected:
+	std::string readBytes(size_t _byteCount) override;
+	std::string getline() override;
+	void writeBytes(std::string_view _data) override;
+	void flushOutput() override;
+};
+
 }
--- a/libsolidity/lsp/Utils.cpp
+++ b/libsolidity/lsp/Utils.cpp
@ -22,7 +22,7 @@
 #include <libsolidity/lsp/FileRepository.h>
 #include <libsolidity/lsp/Utils.h>

-#include <fmt/format.h>
+#include <regex>
 #include <fstream>

 namespace solidity::lsp
@ -115,4 +115,15 @@ optional<SourceLocation> parseRange(FileRepository const& _fileRepository, strin
 	return start;
 }

+string stripFileUriSchemePrefix(string const& _path)
+{
+	regex const windowsDriveLetterPath("^file:///[a-zA-Z]:/");
+	if (regex_search(_path, windowsDriveLetterPath))
+		return _path.substr(8);
+	if (_path.find("file://") == 0)
+		return _path.substr(7);
+	else
+		return _path;
+}
+
 }
--- a/libsolidity/lsp/Utils.h
+++ b/libsolidity/lsp/Utils.h
@ -64,6 +64,13 @@ std::optional<langutil::SourceLocation> parseRange(
 	Json::Value const& _range
 );

+/// Strips the file:// URI prefix off the given path, if present,
+/// also taking special care of Windows-drive-letter paths.
+///
+/// So file:///path/to/some/file.txt returns /path/to/some/file.txt, as well as,
+/// file:///C:/file.txt will return C:/file.txt (forward-slash is okay on Windows).
+std::string stripFileUriSchemePrefix(std::string const& _path);
+
 /// Extracts the resolved declaration of the given expression AST node.
 ///
 /// This may for example be the type declaration of an identifier,
--- a/libsolidity/parsing/Parser.cpp
+++ b/libsolidity/parsing/Parser.cpp
@ -142,7 +142,7 @@ ASTPointer<SourceUnit> Parser::parse(CharStream& _charStream)
 					expectToken(Token::Semicolon);
 				}
 				else
-					fatalParserError(7858_error, "Expected pragma, import directive or contract/interface/library/struct/enum/constant/function definition.");
+					fatalParserError(7858_error, "Expected pragma, import directive or contract/interface/library/struct/enum/constant/function/error definition.");
 			}
 		}
 		solAssert(m_recursionDepth == 0, "");
--- a/libsolutil/Visitor.h
+++ b/libsolutil/Visitor.h
@ -56,6 +56,17 @@ struct VisitorFallback<R> { template<typename T> R operator()(T&&) const { retur
 template<>
 struct VisitorFallback<> { template<typename T> void operator()(T&&) const {} };

-template <typename... Visitors> struct GenericVisitor: Visitors... { using Visitors::operator()...; };
+// MSVC. Empty base class optimization does not happen in some scenarios.
+// Enforcing it with __declspec(empty_bases) avoids MSVC Debug test crash
+// (Run-Time Check Failure #2 - Stack around the variable '....' was corrupted).
+// See https://docs.microsoft.com/en-us/cpp/cpp/empty-bases,
+//     https://developercommunity.visualstudio.com/t/10005513.
+#if defined(_MSC_VER)
+#define SOLC_EMPTY_BASES __declspec(empty_bases)
+#else
+#define SOLC_EMPTY_BASES
+#endif
+
+template <typename... Visitors> struct SOLC_EMPTY_BASES GenericVisitor: Visitors... { using Visitors::operator()...; };
 template <typename... Visitors> GenericVisitor(Visitors...) -> GenericVisitor<Visitors...>;
 }
--- a/libyul/optimiser/StructuralSimplifier.cpp
+++ b/libyul/optimiser/StructuralSimplifier.cpp
@ -93,31 +93,26 @@ void StructuralSimplifier::operator()(Block& _block)

 void StructuralSimplifier::simplify(std::vector<yul::Statement>& _statements)
 {
-	// Explicit local variables ifLambda, switchLambda, forLoopLambda are created to avoid MSVC C++17 Debug test crash
-	// (Run-Time Check Failure #2 - Stack around the variable '....' was corrupted).
-	// As soon as the issue is fixed, this workaround can be removed.
-	auto ifLambda = [&](If& _ifStmt) -> OptionalStatements
-	{
-		if (expressionAlwaysTrue(*_ifStmt.condition))
-			return {std::move(_ifStmt.body.statements)};
-		else if (expressionAlwaysFalse(*_ifStmt.condition))
-			return {vector<Statement>{}};
-		return {};
+	util::GenericVisitor visitor{
+		util::VisitorFallback<OptionalStatements>{},
+		[&](If& _ifStmt) -> OptionalStatements {
+			if (expressionAlwaysTrue(*_ifStmt.condition))
+				return {std::move(_ifStmt.body.statements)};
+			else if (expressionAlwaysFalse(*_ifStmt.condition))
+				return {vector<Statement>{}};
+			return {};
+		},
+		[&](Switch& _switchStmt) -> OptionalStatements {
+			if (std::optional<u256> const constExprVal = hasLiteralValue(*_switchStmt.expression))
+				return replaceConstArgSwitch(_switchStmt, constExprVal.value());
+			return {};
+		},
+		[&](ForLoop& _forLoop) -> OptionalStatements {
+			if (expressionAlwaysFalse(*_forLoop.condition))
+				return {std::move(_forLoop.pre.statements)};
+			return {};
+		}
 	};
-	auto switchLambda = [&](Switch& _switchStmt) -> OptionalStatements
-	{
-		if (std::optional<u256> const constExprVal = hasLiteralValue(*_switchStmt.expression))
-			return replaceConstArgSwitch(_switchStmt, constExprVal.value());
-		return {};
-	};
-	auto forLoopLambda = [&](ForLoop& _forLoop) -> OptionalStatements
-	{
-		if (expressionAlwaysFalse(*_forLoop.condition))
-			return {std::move(_forLoop.pre.statements)};
-		return {};
-	};
-
-	util::GenericVisitor visitor{util::VisitorFallback<OptionalStatements>{}, ifLambda, switchLambda, forLoopLambda};

 	util::iterateReplacing(
 		_statements,
--- a/scripts/build_emscripten.sh
+++ b/scripts/build_emscripten.sh
@ -34,7 +34,7 @@ else
    BUILD_DIR="$1"
 fi

-# solbuildpackpusher/solidity-buildpack-deps:emscripten-9
+# solbuildpackpusher/solidity-buildpack-deps:emscripten-10
 docker run -v "$(pwd):/root/project" -w /root/project \
-    solbuildpackpusher/solidity-buildpack-deps@sha256:d51534dfdd05ece86f69ed7beafd68c15b88606da00a4b7fe2873ccfbd0dce24\
+    solbuildpackpusher/solidity-buildpack-deps@sha256:bd23831e0025e35a106005b4ac06cb3618f690bfa2833a5881b573c02d35d9fc\
    ./scripts/ci/build_emscripten.sh "$BUILD_DIR"
--- a/scripts/deps-ppa/static_z3.sh
+++ b/scripts/deps-ppa/static_z3.sh
@ -25,9 +25,9 @@ set -ev
 keyid=70D110489D66E2F6
 email=builds@ethereum.org
 packagename=z3-static
-version=4.8.14
+version=4.8.16

-DISTRIBUTIONS="focal hirsute impish jammy"
+DISTRIBUTIONS="focal impish jammy"

 for distribution in $DISTRIBUTIONS
 do
--- a/scripts/tests.sh
+++ b/scripts/tests.sh
@ -84,7 +84,7 @@ printTask "Testing Python scripts..."
 "$REPO_ROOT/test/pyscriptTests.py"

 printTask "Testing LSP..."
-"$REPO_ROOT/scripts/test_solidity_lsp.py" "${SOLIDITY_BUILD_DIR}/solc/solc"
+"$REPO_ROOT/test/lsp.py" "${SOLIDITY_BUILD_DIR}/solc/solc"

 printTask "Running commandline tests..."
 # Only run in parallel if this is run on CI infrastructure
--- a/solc/CommandLineInterface.cpp
+++ b/solc/CommandLineInterface.cpp
@ -912,7 +912,7 @@ void CommandLineInterface::handleAst()

 void CommandLineInterface::serveLSP()
 {
-	lsp::IOStreamTransport transport;
+	lsp::StdioTransport transport;
 	if (!lsp::LanguageServer{transport}.run())
 		solThrow(CommandLineExecutionError, "LSP terminated abnormally.");
 }
--- a/test/cmdlineTests/model_checker_invariants_all/err
+++ b/test/cmdlineTests/model_checker_invariants_all/err
@ -5,10 +5,8 @@ Warning: Return value of low-level calls not used.
  | 		^^^^^^^^^^^

 Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test:
-(x <= 0)
+((x <= 0) || true)
 Reentrancy property(ies) for model_checker_invariants_all/input.sol:test:
-((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
 <errorCode> = 0 -> no errors
-<errorCode> = 1 -> Assertion failed at assert(x < 10)
-<errorCode> = 3 -> Assertion failed at assert(x < 10)
+<errorCode> = 1 -> Assertion failed at assert(x == 0)
--- a/test/cmdlineTests/model_checker_invariants_all/input.sol
+++ b/test/cmdlineTests/model_checker_invariants_all/input.sol
@ -4,9 +4,6 @@ contract test {
 	uint x;
    function f(address _a) public {
 		_a.call("");
-		assert(x < 10);
+		assert(x == 0);
    }
-	function g() public view {
-		assert(x < 10);
-	}
 }
--- a/test/cmdlineTests/model_checker_invariants_contract/err
+++ b/test/cmdlineTests/model_checker_invariants_contract/err
@ -1,2 +1,2 @@
 Info: Contract invariant(s) for model_checker_invariants_contract/input.sol:test:
-(x <= 0)
+((x <= 0) || true)
--- a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err
+++ b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err
@ -5,10 +5,8 @@ Warning: Return value of low-level calls not used.
  | 		^^^^^^^^^^^

 Info: Contract invariant(s) for model_checker_invariants_contract_reentrancy/input.sol:test:
-(x <= 0)
+((x <= 0) || true)
 Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
-((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
 <errorCode> = 0 -> no errors
-<errorCode> = 1 -> Assertion failed at assert(x < 10)
-<errorCode> = 3 -> Assertion failed at assert(x < 10)
+<errorCode> = 1 -> Assertion failed at assert(x == 0)
--- a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol
+++ b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol
@ -4,9 +4,6 @@ contract test {
 	uint x;
    function f(address _a) public {
 		_a.call("");
-		assert(x < 10);
+		assert(x == 0);
    }
-	function g() public view {
-		assert(x < 10);
-	}
 }
--- a/test/cmdlineTests/model_checker_invariants_reentrancy/err
+++ b/test/cmdlineTests/model_checker_invariants_reentrancy/err
@ -5,6 +5,6 @@ Warning: Return value of low-level calls not used.
  | 		^^^^^^^^^^^

 Info: Reentrancy property(ies) for model_checker_invariants_reentrancy/input.sol:test:
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x < 10)
--- a/test/cmdlineTests/recovery_ast_empty_contract/err
+++ b/test/cmdlineTests/recovery_ast_empty_contract/err
@ -1,4 +1,4 @@
-Error: Expected pragma, import directive or contract/interface/library/struct/enum/constant/function definition.
+Error: Expected pragma, import directive or contract/interface/library/struct/enum/constant/function/error definition.
 --> recovery_ast_empty_contract/input.sol:3:1:
  |
 3 | c
--- a/test/cmdlineTests/standard_model_checker_invariants_contract/output.json
+++ b/test/cmdlineTests/standard_model_checker_invariants_contract/output.json
@ -1,7 +1,7 @@
 {"errors":[{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test:
-(x <= 0)
+((x <= 0) || true)


 ","message":"Contract invariant(s) for A:test:
-(x <= 0)
+((x <= 0) || true)
 ","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}
--- a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json
+++ b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json
@ -8,10 +8,7 @@
 					uint x;
 					function f(address _a) public {
 						_a.call(\"\");
-						assert(x < 10);
-					}
-					function g() public view {
-						assert(x < 10);
+						assert(x == 10);
 					}
 				}"
 		}
--- a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json
+++ b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json
@ -4,22 +4,28 @@
 7 | \t\t\t\t\t\t_a.call(\"\");
  | \t\t\t\t\t\t^^^^^^^^^^^

-","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test:
-(x <= 0)
-Reentrancy property(ies) for A:test:
-((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
-<errorCode> = 0 -> no errors
-<errorCode> = 1 -> Assertion failed at assert(x < 10)
-<errorCode> = 3 -> Assertion failed at assert(x < 10)
+","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+Counterexample:
+x = 0
+_a = 0x0

+Transaction trace:
+test.constructor()
+State: x = 0
+test.f(0x0)
+    _a.call(\"\") -- untrusted external call
+ --> A:8:7:
+  |
+8 | \t\t\t\t\t\tassert(x == 10);
+  | \t\t\t\t\t\t^^^^^^^^^^^^^^^

-","message":"Contract invariant(s) for A:test:
-(x <= 0)
-Reentrancy property(ies) for A:test:
-((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
-<errorCode> = 0 -> no errors
-<errorCode> = 1 -> Assertion failed at assert(x < 10)
-<errorCode> = 3 -> Assertion failed at assert(x < 10)
-","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}
+","message":"CHC: Assertion violation happens here.
+Counterexample:
+x = 0
+_a = 0x0
+
+Transaction trace:
+test.constructor()
+State: x = 0
+test.f(0x0)
+    _a.call(\"\") -- untrusted external call","severity":"warning","sourceLocation":{"end":166,"file":"A","start":151},"type":"Warning"}],"sources":{"A":{"id":0}}}
--- a/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json
+++ b/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json
@ -5,13 +5,13 @@
  | \t\t\t\t\t\t^^^^^^^^^^^

 ","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Reentrancy property(ies) for A:test:
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x < 10)


 ","message":"Reentrancy property(ies) for A:test:
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x < 10)
 ","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}
--- a/test/libsolidity/SMTCheckerTest.cpp
+++ b/test/libsolidity/SMTCheckerTest.cpp
@ -69,7 +69,17 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
 	else
 		BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT counterexample choice."));

-	auto const& ignoreInv = m_reader.stringSetting("SMTIgnoreInv", "no");
+	static auto removeInv = [](vector<SyntaxTestError>&& errors) {
+		vector<SyntaxTestError> filtered;
+		for (auto&& e: errors)
+			if (e.errorId != 1180_error)
+				filtered.emplace_back(e);
+		return filtered;
+	};
+	if (m_modelCheckerSettings.invariants.invariants.empty())
+		m_expectations = removeInv(move(m_expectations));
+
+	auto const& ignoreInv = m_reader.stringSetting("SMTIgnoreInv", "yes");
 	if (ignoreInv == "no")
 		m_modelCheckerSettings.invariants = ModelCheckerInvariants::All();
 	else if (ignoreInv == "yes")
--- a/test/libsolidity/lsp/didOpen_with_import.sol
+++ b/test/libsolidity/lsp/didOpen_with_import.sol
@ -1,7 +1,7 @@
 // SPDX-License-Identifier: UNLICENSED
 pragma solidity >=0.8.0;

-import './lib.sol';
+import './goto/lib.sol';

 contract C
 {
--- a/test/libsolidity/lsp/goto/goto_definition.sol
+++ b/test/libsolidity/lsp/goto/goto_definition.sol
@ -0,0 +1,207 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity >=0.8.0;
+
+import "./lib.sol";
+//      ^ @importDirective
+
+interface I
+{
+    function f(uint x) external returns (uint);
+    //       ^ @functionF
+}
+
+contract IA is I
+    //   ^^ @IASymbol
+{
+    function f(uint x) public pure override returns (uint) { return x + 1; }
+}
+
+contract IB is I
+{
+    function f(uint x) public pure override returns (uint) { return x + 2; }
+}
+
+library IntLib
+{
+    function add(int self, int b) public pure returns (int) { return self + b; }
+    //       ^^^ @IntLibAdd
+}
+
+contract C
+{
+    I obj;
+    function virtual_inheritance() public payable
+    {
+        obj = new IA();
+        //        ^ @usingIASymbol
+        obj.f(1); // goto-definition should jump to definition of interface.
+    //      ^ @virtualFunctionLookup
+    }
+
+    using IntLib for *;
+    function using_for(int i) pure public
+    {
+        i.add(5);
+ //       ^ @usingIntAdd
+        14.add(4);
+    }
+
+    function useLib(uint n) public payable returns (uint)
+    {
+        return Lib.add(n, 1);
+        //     ^ @LibSymbol
+        //         ^ @LibAddSymbol
+    }
+
+    function enums(Color c) public pure returns (Color d)
+    //             ^ @ColorSymbolInParameter
+    {
+        Color e = Color.Red;
+        //    ^ @eVariableDeclaration
+        //              ^ @RedEnumMemberAccess
+        if (c == e)
+        //       ^ @eVariableAccess
+            d = Color.Green;
+        else
+            d = c;
+    }
+
+    type Price is uint128;
+    //   ^^^^^ @PriceDeclaration
+    function udlTest() public pure returns (uint128)
+    {
+        Price p = Price.wrap(128);
+    //  ^ @PriceSymbol
+    //            ^ @PriceInWrap
+        return Price.unwrap(p);
+    }
+
+    function structCtorTest(uint8 v) public pure returns (uint8 result)
+    {
+        RGBColor memory c = RGBColor(v, 2 * v, 3 * v);
+        //                       ^ @RGBColorCursor
+        result = c.red;
+        int a;
+//      ^^^^^ @unusedLocalVar
+    }
+}
+// ----
+// goto_definition: @unusedLocalVar 2072
+// lib: @diagnostics 2072
+// -> textDocument/definition {
+//     "position": @importDirective
+// }
+// <- [
+//     {
+//         "range": {
+//             "end": {
+//                 "character": 0,
+//                 "line": 0
+//             },
+//             "start": {
+//                 "character": 0,
+//                 "line": 0
+//             }
+//         },
+//         "uri": "lib.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @usingIASymbol
+// }
+// <- [
+//     {
+//         "range": @IASymbol,
+//         "uri": "goto_definition.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @virtualFunctionLookup
+// }
+// <- [
+//     {
+//         "range": @functionF,
+//         "uri": "goto_definition.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @usingIntAdd
+// }
+// <- [
+//     {
+//         "range": @IntLibAdd,
+//         "uri": "goto_definition.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @LibSymbol
+// }
+// <- [
+//     {
+//         "range": @LibLibrary,
+//         "uri": "lib.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @LibAddSymbol
+// }
+// <- [
+//     {
+//         "range": @addSymbol,
+//         "uri": "lib.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @ColorSymbolInParameter
+// }
+// <- [
+//     {
+//         "range": @ColorEnum,
+//         "uri": "lib.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @RedEnumMemberAccess
+// }
+// <- [
+//     {
+//         "range": @EnumMemberRed,
+//         "uri": "lib.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @eVariableAccess
+// }
+// <- [
+//     {
+//         "range": @eVariableDeclaration,
+//         "uri": "goto_definition.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @PriceSymbol
+// }
+// <- [
+//     {
+//         "range": @PriceDeclaration,
+//         "uri": "goto_definition.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @PriceInWrap
+// }
+// <- [
+//     {
+//         "range": @PriceDeclaration,
+//         "uri": "goto_definition.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @RGBColorCursor
+// }
+// <- [
+//     {
+//         "range": @RGBColorStruct,
+//         "uri": "lib.sol"
+//     }
+// ]
--- a/test/libsolidity/lsp/goto/goto_definition_imports.sol
+++ b/test/libsolidity/lsp/goto/goto_definition_imports.sol
@ -0,0 +1,71 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity >=0.8.0;
+
+import {Weather as Wetter} from "./lib.sol";
+//       ^ @wheatherImportCursor
+import "./lib.sol" as That;
+//                    ^^^^ @ThatImport
+
+contract C
+{
+    function test_symbol_alias() public pure returns (Wetter result)
+                                             //        ^ @WetterCursor
+    {
+        result = Wetter.Sunny;
+    }
+
+    function test_library_alias() public pure returns (That.Color result)
+                                                //     ^ @ThatCursor
+    {
+        That.Color color = That.Color.Red;
+//      ^ @ThatVarCursor   ^ @ThatExpressionCursor
+        result = color;
+    }
+}
+// ----
+// lib: @diagnostics 2072
+// -> textDocument/definition {
+//     "position": @wheatherImportCursor
+// }
+// <- [
+//     {
+//         "range": @whetherEnum,
+//         "uri": "lib.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @WetterCursor
+// }
+// <- [
+//     {
+//         "range": @whetherEnum,
+//         "uri": "lib.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @ThatCursor
+// }
+// <- [
+//     {
+//         "range": @ColorEnum,
+//         "uri": "lib.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @ThatVarCursor
+// }
+// <- [
+//     {
+//         "range": @ColorEnum,
+//         "uri": "lib.sol"
+//     }
+// ]
+// -> textDocument/definition {
+//     "position": @ThatExpressionCursor
+// }
+// <- [
+//     {
+//         "range": @ThatImport,
+//         "uri": "goto_definition_imports.sol"
+//     }
+// ]
--- a/test/libsolidity/lsp/goto/lib.sol
+++ b/test/libsolidity/lsp/goto/lib.sol
@ -5,6 +5,7 @@ pragma solidity >=0.8.0;
 error E(uint, uint);

 enum Weather {
+//   ^^^^^^^ @whetherEnum
    Sunny,
    Cloudy,
    Rainy
@ -12,8 +13,10 @@ enum Weather {

 /// Some custom Color enum type holding 3 colors.
 enum Color {
+//   ^^^^^ @ColorEnum
    /// Red color.
    Red,
+//  ^^^ @EnumMemberRed
    /// Green color.
    Green,
    /// Blue color.
@ -21,9 +24,11 @@ enum Color {
 }

 library Lib
+//   @  ^^^ @LibLibrary
 {
    function add(uint a, uint b) public pure returns (uint result)
 // ^( @addFunction
+//           ^^^ @addSymbol
    {
        result = a + b;
    }
@ -37,8 +42,11 @@ library Lib
 }

 struct RGBColor
+//     ^^^^^^^^ @RGBColorStruct
 {
    uint8 red;
    uint8 green;
    uint8 blue;
 }
+// ----
+// lib: @diagnostics 2072
--- a/test/libsolidity/lsp/goto/publish_diagnostics_1.sol
+++ b/test/libsolidity/lsp/goto/publish_diagnostics_1.sol
@ -19,3 +19,5 @@ contract D
   //   ^^^^^^^^^^^^ @unusedContractVariable
    }
 }
+// ----
+// publish_diagnostics_1: @unusedReturnVariable 6321 @unusedVariable 2072 @unusedContractVariable 2072
--- a/test/libsolidity/lsp/goto/publish_diagnostics_2.sol
+++ b/test/libsolidity/lsp/goto/publish_diagnostics_2.sol
@ -22,3 +22,5 @@ contract D
          //   ^^^^^^^^^^^^^^^^^^^^^ @wrongArgumentsCount
    }
 }
+// ----
+// publish_diagnostics_2: @conversionError 9574 @argumentsRequired 6777 @wrongArgumentsCount 6160
--- a/test/libsolidity/lsp/goto_definition.sol
+++ b/test/libsolidity/lsp/goto_definition.sol
@ -1,68 +0,0 @@
-// SPDX-License-Identifier: UNLICENSED
-pragma solidity >=0.8.0;
-
-import "./lib.sol";
-
-interface I
-{
-    function f(uint x) external returns (uint);
-}
-
-contract IA is I
-{
-    function f(uint x) public pure override returns (uint) { return x + 1; }
-}
-
-contract IB is I
-{
-    function f(uint x) public pure override returns (uint) { return x + 2; }
-}
-
-library IntLib
-{
-    function add(int self, int b) public pure returns (int) { return self + b; }
-}
-
-contract C
-{
-    I obj;
-    function virtual_inheritance() public payable
-    {
-        obj = new IA();
-        obj.f(1); // goto-definition should jump to definition of interface.
-    }
-
-    using IntLib for *;
-    function using_for(int i) pure public
-    {
-        i.add(5);
-        14.add(4);
-    }
-
-    function useLib(uint n) public payable returns (uint)
-    {
-        return Lib.add(n, 1);
-    }
-
-    function enums(Color c) public pure returns (Color d)
-    {
-        Color e = Color.Red;
-        if (c == e)
-            d = Color.Green;
-        else
-            d = c;
-    }
-
-    type Price is uint128;
-    function udlTest() public pure returns (uint128)
-    {
-        Price p = Price.wrap(128);
-        return Price.unwrap(p);
-    }
-
-    function structCtorTest(uint8 v) public pure returns (uint8 result)
-    {
-        RGBColor memory c = RGBColor(v, 2 * v, 3 * v);
-        result = c.red;
-    }
-}
--- a/test/libsolidity/lsp/goto_definition_imports.sol
+++ b/test/libsolidity/lsp/goto_definition_imports.sol
@ -1,19 +0,0 @@
-// SPDX-License-Identifier: UNLICENSED
-pragma solidity >=0.8.0;
-
-import {Weather as Wetter} from "./lib.sol";
-import "./lib.sol" as That;
-
-contract C
-{
-    function test_symbol_alias() public pure returns (Wetter result)
-    {
-        result = Wetter.Sunny;
-    }
-
-    function test_library_alias() public pure returns (That.Color result)
-    {
-        That.Color color = That.Color.Red;
-        result = color;
-    }
-}
--- a/test/libsolidity/semanticTests/using/library_on_interface.sol
+++ b/test/libsolidity/semanticTests/using/library_on_interface.sol
@ -0,0 +1,18 @@
+using L for I;
+interface I { function f() external pure returns (uint); }
+library L {
+    function execute(I i) internal pure returns (uint) {
+        return i.f();
+    }
+}
+contract C is I {
+    function x() public view returns (uint) {
+        I i = this;
+        return i.execute();
+    }
+    function f() public pure returns (uint) { return 7; }
+}
+// ====
+// compileViaYul: also
+// ----
+// x() -> 7
--- a/test/libsolidity/semanticTests/using/using_global_all_the_types.sol
+++ b/test/libsolidity/semanticTests/using/using_global_all_the_types.sol
@ -0,0 +1,38 @@
+==== Source: A ====
+enum E {A, B}
+struct S { uint x; }
+type T is uint;
+using L for E global;
+using L for S global;
+using L for T global;
+library L {
+    function f(E e) internal pure returns (uint) {
+        return uint(e);
+    }
+    function f(S memory s) internal pure returns (uint) {
+        return s.x;
+    }
+    function f(T t) internal pure returns (uint) {
+        return T.unwrap(t);
+    }
+}
+
+==== Source: B ====
+contract C {
+    function f() public pure returns (uint a, uint b, uint c) {
+        E e = E.B;
+        a = e.f();
+        S memory s;
+        s.x = 7;
+        b = s.f();
+        T t = T.wrap(9);
+        c = t.f();
+    }
+}
+
+import {E, S, T} from "A";
+
+// ====
+// compileViaYul: also
+// ----
+// f() -> 1, 7, 9
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
@ -3,7 +3,8 @@ contract C {
 		require(a == b);
 		bytes memory b1 = abi.encodeWithSelector(sel, a, a, a, a);
 		bytes memory b2 = abi.encodeWithSelector(sel, b, a, b, a);
-		assert(keccak256(b1) == keccak256(b2));
+		// Disabled because of OSX nondeterminism
+		//assert(keccak256(b1) == keccak256(b2));

 		bytes memory b3 = abi.encodeWithSelector(0xcafecafe, a, a, a, a);
 		assert(keccak256(b1) == keccak256(b3)); // should fail
@ -13,9 +14,10 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 1218: (333-371): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (390-428): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (333-371): CHC: Assertion violation might happen here.
-// Warning 6328: (390-428): CHC: Assertion violation might happen here.
-// Warning 4661: (333-371): BMC: Assertion violation happens here.
-// Warning 4661: (390-428): BMC: Assertion violation happens here.
+// Warning 2072: (161-176): Unused local variable.
+// Warning 1218: (379-417): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (436-474): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (379-417): CHC: Assertion violation might happen here.
+// Warning 6328: (436-474): CHC: Assertion violation might happen here.
+// Warning 4661: (379-417): BMC: Assertion violation happens here.
+// Warning 4661: (436-474): BMC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
@ -19,4 +19,4 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()
+// Warning 6328: (199-229): CHC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol
@ -18,5 +18,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (265-310): CHC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol
@ -22,5 +22,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (435-508): CHC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
@ -11,13 +11,13 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // SMTIgnoreOS: macos
 // ----
 // Warning 4984: (82-85): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4984: (154-160): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4984: (212-218): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 6328: (180-219): CHC: Assertion violation happens here.\nCounterexample:\nc = 1\n\nTransaction trace:\nC.constructor()\nState: c = 0\nC.f(){ msg.value: 11 }\nState: c = 1\nC.inv()
-// Info 1180: Contract invariant(s) for :C:\n(((11 * c) + ((- 1) * (:var 1).balances[address(this)])) <= 0)\n
+// Warning 6328: (180-219): CHC: Assertion violation happens here.
 // Warning 2661: (82-85): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (154-160): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (212-218): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
--- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol
@ -45,5 +45,5 @@ contract C {
 // SMTIgnoreOS: macos
 // ----
 // Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()\n    C.reset_if_overflow() -- internal call
-// Warning 6328: (502-519): CHC: Assertion violation happens here.
+// Warning 6328: (502-519): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\noldx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n    C.reset_if_overflow() -- internal call
 // Warning 6328: (615-629): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(10)\nState: x = 10\nC.test()\n    C.reset_if_overflow() -- internal call
--- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
@ -48,12 +48,10 @@ contract C {
 // Warning 1218: (693-712): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (716-735): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (739-758): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (762-781): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (693-712): CHC: Assertion violation might happen here.
 // Warning 6328: (716-735): CHC: Assertion violation might happen here.
 // Warning 6328: (739-758): CHC: Assertion violation might happen here.
-// Warning 6328: (762-781): CHC: Assertion violation might happen here.
+// Warning 6328: (762-781): CHC: Assertion violation happens here.
 // Warning 4661: (693-712): BMC: Assertion violation happens here.
 // Warning 4661: (716-735): BMC: Assertion violation happens here.
 // Warning 4661: (739-758): BMC: Assertion violation happens here.
-// Warning 4661: (762-781): BMC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol
@ -12,5 +12,5 @@ contract C {
 // ----
 // Warning 9302: (96-117): Return value of low-level calls not used.
 // Warning 6328: (121-156): CHC: Assertion violation might happen here.
-// Warning 6328: (175-211): CHC: Assertion violation happens here.
+// Warning 6328: (175-211): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n    i.call{value: 10}("") -- untrusted external call
 // Warning 4661: (121-156): BMC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol
@ -11,5 +11,5 @@ contract C {
 // ----
 // Warning 9302: (96-116): Return value of low-level calls not used.
 // Warning 6328: (120-156): CHC: Assertion violation might happen here.
-// Warning 6328: (175-210): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n    i.call{value: 0}("") -- untrusted external call
+// Warning 6328: (175-210): CHC: Assertion violation happens here.
 // Warning 4661: (120-156): BMC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol
@ -20,4 +20,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
-// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()
+// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()
--- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol
@ -42,4 +42,6 @@ contract C {
 // SMTIgnoreOS: macos
 // ----
 // Warning 2018: (33-88): Function state mutability can be restricted to view
-// Warning 6328: (367-381): CHC: Assertion violation happens here.
+// Warning 1218: (367-381): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (367-381): CHC: Assertion violation might happen here.
+// Warning 4661: (367-381): BMC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol
@ -44,7 +44,5 @@ contract C {
 // SMTIgnoreCex: yes
 // SMTIgnoreOS: macos
 // ----
-// Warning 1218: (437-463): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (419-433): CHC: Assertion violation happens here.
-// Warning 6328: (437-463): CHC: Assertion violation might happen here.
-// Warning 4661: (437-463): BMC: Assertion violation happens here.
+// Warning 6328: (437-463): CHC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol
@ -14,6 +14,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0, 0, 0]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0, 0, 0]\nC.f()
+// Warning 6328: (187-201): CHC: Assertion violation happens here.
 // Info 1180: Contract invariant(s) for :C:\n!(a.length <= 2)\n
--- a/test/libsolidity/smtCheckerTests/functions/payable_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/payable_2.sol
@ -24,4 +24,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (261-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g2(){ msg.value: 35 }\n    C.i() -- internal call
+// Warning 6328: (261-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g2(){ msg.value: 1 }\n    C.i() -- internal call
--- a/test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol
@ -27,7 +27,5 @@ contract C
 // ====
 // SMTEngine: all
 // ----
-// Warning 1218: (290-305): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (290-305): CHC: Assertion violation might happen here.
+// Warning 6328: (290-305): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 15\nb = false\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, false, false)
 // Warning 6328: (329-344): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 0\nb = true\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, true, false)
-// Warning 4661: (290-305): BMC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
@ -19,4 +19,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 1180: Contract invariant(s) for :C:\n!(s.x.length <= 2)\n
+// Warning 6368: (196-202): CHC: Out of bounds access might happen here.
--- a/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol
+++ b/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol
@ -3,8 +3,9 @@ contract C {
 		require(b.length == 30);
 		require(b[10] == 0xff);
 		require(b[b.length - 1] == 0xaa);
-		assert(bytes(b[10:]).length == 20);
-		assert(bytes(b[10:])[0] == 0xff);
+		assert(bytes(b[10:]).length == 20); // should hold
+		// Disabled because of Spacer's nondeterminism.
+		//assert(bytes(b[10:])[0] == 0xff); // should hold
 		//assert(bytes(b[10:])[5] == 0xff); // Removed because of Spacer's nondeterminism
 		//assert(bytes(b[10:])[19] == 0xaa); // Removed because of Spacer nondeterminism
 	}
@ -12,5 +13,3 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (188-220): CHC: Assertion violation might happen here.
-// Warning 4661: (188-220): BMC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol
@ -5,5 +5,6 @@ contract C  {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819968\ny = 2\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819968, 2)
+// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
--- a/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol
+++ b/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol
@ -32,4 +32,4 @@ contract C {
 // ====
 // SMTEngine: chc
 // ----
-// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x0, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n    C.g() -- internal call
+// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x1e28, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x1e28, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n    C.g() -- internal call
--- a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol
+++ b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol
@ -13,4 +13,4 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 2997\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2803 }\n    _i.f() -- untrusted external call, synthesized as:\n        C.g(0){ msg.value: 2446 } -- reentrant call\n            _i.f() -- untrusted external call
+// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 9726\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2070 }\n    _i.f() -- untrusted external call, synthesized as:\n        C.g(0){ msg.value: 0 } -- reentrant call\n            _i.f() -- untrusted external call
--- a/test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol
+++ b/test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol
@ -19,5 +19,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (342-362): CHC: Assertion violation happens here.\nCounterexample:\n\nchoice = 3\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (342-362): CHC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol
+++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol
@ -36,11 +36,12 @@ contract C
 // SMTIgnoreCex: yes
 // ----
 // Warning 6368: (439-453): CHC: Out of bounds access happens here.
+// Warning 6368: (465-480): CHC: Out of bounds access might happen here.
 // Warning 6368: (492-508): CHC: Out of bounds access happens here.
 // Warning 6368: (492-511): CHC: Out of bounds access happens here.
 // Warning 6368: (622-636): CHC: Out of bounds access happens here.
+// Warning 6368: (737-752): CHC: Out of bounds access might happen here.
 // Warning 6368: (850-866): CHC: Out of bounds access happens here.
 // Warning 6368: (850-869): CHC: Out of bounds access happens here.
 // Warning 6328: (936-956): CHC: Assertion violation happens here.
 // Warning 6368: (1029-1043): CHC: Out of bounds access might happen here.
-// Info 1180: Contract invariant(s) for :C:\n!(severalMaps8.length <= 0)\n
--- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
+++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
@ -30,7 +30,8 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 6368: (340-355): CHC: Out of bounds access might happen here.
+// Warning 6368: (612-627): CHC: Out of bounds access might happen here.
 // Warning 6328: (860-880): CHC: Assertion violation happens here.
 // Warning 6368: (936-952): CHC: Out of bounds access might happen here.
 // Warning 6368: (936-955): CHC: Out of bounds access might happen here.
-// Info 1180: Contract invariant(s) for :C:\n!(severalMaps8.length <= 1)\n
--- a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol
@ -53,3 +53,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 6368: (212-217): CHC: Out of bounds access might happen here.
--- a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol
@ -20,4 +20,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (289-322): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 11}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 11}\nC.g(){ msg.sender: 0x0985 }
+// Warning 6328: (289-322): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 10}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 10}\nC.g(){ msg.sender: 0x0985 }
--- a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol
@ -25,5 +25,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (307-327): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 11, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 11, s: {innerM, sum: 21239}}\nC.g()
+// Warning 6328: (307-327): CHC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol
+++ b/test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol
@ -9,5 +9,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 65535) happens here.\nCounterexample:\n\na = 1\nb = 65535\n = 0\n\nTransaction trace:\nC.constructor()\nC.add(1, 65535)
+// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 65535) happens here.
--- a/test/libsolidity/smtCheckerTests/userTypes/conversion.sol
+++ b/test/libsolidity/smtCheckerTests/userTypes/conversion.sol
@ -1,87 +0,0 @@
-pragma abicoder v2;
-
-type MyUInt8 is uint8;
-type MyInt8 is int8;
-type MyUInt16 is uint16;
-
-contract C {
-	function f(uint a) internal pure returns(MyUInt8) {
-		return MyUInt8.wrap(uint8(a));
-	}
-	function g(uint a) internal pure returns(MyInt8) {
-		return MyInt8.wrap(int8(int(a)));
-	}
-	function h(MyUInt8 a) internal pure returns (MyInt8) {
-		return MyInt8.wrap(int8(MyUInt8.unwrap(a)));
-	}
-	function i(MyUInt8 a) internal pure returns(MyUInt16) {
-		return MyUInt16.wrap(MyUInt8.unwrap(a));
-	}
-	function j(MyUInt8 a) internal pure returns (uint) {
-		return MyUInt8.unwrap(a);
-	}
-	function k(MyUInt8 a) internal pure returns (MyUInt16) {
-		return MyUInt16.wrap(MyUInt8.unwrap(a));
-	}
-	function m(MyUInt16 a) internal pure returns (MyUInt8) {
-		return MyUInt8.wrap(uint8(MyUInt16.unwrap(a)));
-	}
-
-	function p() public pure {
-		assert(MyUInt8.unwrap(f(1)) == 1);
-		assert(MyUInt8.unwrap(f(2)) == 2);
-		assert(MyUInt8.unwrap(f(257)) == 1);
-		assert(MyUInt8.unwrap(f(257)) == 257); // should fail
-	}
-
-	function q() public pure {
-		assert(MyInt8.unwrap(g(1)) == 1);
-		assert(MyInt8.unwrap(g(2)) == 2);
-		assert(MyInt8.unwrap(g(255)) == -1);
-		assert(MyInt8.unwrap(g(257)) == 1);
-		assert(MyInt8.unwrap(g(257)) == -1); // should fail
-	}
-
-	function r() public pure {
-		assert(MyInt8.unwrap(h(MyUInt8.wrap(1))) == 1);
-		assert(MyInt8.unwrap(h(MyUInt8.wrap(2))) == 2);
-		assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == -1);
-		assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == 1); // should fail
-	}
-
-	function s() public pure {
-		assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 250);
-		assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 0); // should fail
-	}
-
-	function t() public pure {
-		assert(j(MyUInt8.wrap(1)) == 1);
-		assert(j(MyUInt8.wrap(2)) == 2);
-		assert(j(MyUInt8.wrap(255)) == 0xff);
-		assert(j(MyUInt8.wrap(255)) == 1); // should fail
-	}
-
-	function v() public pure {
-		assert(MyUInt16.unwrap(k(MyUInt8.wrap(1))) == 1);
-		assert(MyUInt16.unwrap(k(MyUInt8.wrap(2))) == 2);
-		assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 0xff);
-		assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 1); // should fail
-	}
-
-	function w() public pure {
-		assert(MyUInt8.unwrap(m(MyUInt16.wrap(1))) == 1);
-		assert(MyUInt8.unwrap(m(MyUInt16.wrap(2))) == 2);
-		assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 0xff);
-		assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 1); // should fail
-	}
-}
-// ====
-// SMTEngine: all
-// ----
-// Warning 6328: (937-974): CHC: Assertion violation happens here.
-// Warning 6328: (1174-1209): CHC: Assertion violation happens here.
-// Warning 6328: (1413-1461): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.r()\n    C.h(1) -- internal call\n    C.h(2) -- internal call\n    C.h(255) -- internal call\n    C.h(255) -- internal call
-// Warning 6328: (1568-1618): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.s()\n    C.i(250) -- internal call\n    C.i(250) -- internal call
-// Warning 6328: (1779-1812): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.t()\n    C.j(1) -- internal call\n    C.j(2) -- internal call\n    C.j(255) -- internal call\n    C.j(255) -- internal call
-// Warning 6328: (2024-2074): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.v()\n    C.k(1) -- internal call\n    C.k(2) -- internal call\n    C.k(255) -- internal call\n    C.k(255) -- internal call
-// Warning 6328: (2286-2336): CHC: Assertion violation happens here.
--- a/test/libsolidity/smtCheckerTests/userTypes/conversion_1.sol
+++ b/test/libsolidity/smtCheckerTests/userTypes/conversion_1.sol
@ -0,0 +1,35 @@
+pragma abicoder v2;
+
+type MyUInt8 is uint8;
+type MyInt8 is int8;
+type MyUInt16 is uint16;
+
+contract C {
+	function f(uint a) internal pure returns(MyUInt8) {
+		return MyUInt8.wrap(uint8(a));
+	}
+	function g(uint a) internal pure returns(MyInt8) {
+		return MyInt8.wrap(int8(int(a)));
+	}
+
+	function p() public pure {
+		assert(MyUInt8.unwrap(f(1)) == 1);
+		assert(MyUInt8.unwrap(f(2)) == 2);
+		assert(MyUInt8.unwrap(f(257)) == 1);
+		assert(MyUInt8.unwrap(f(257)) == 257); // should fail
+	}
+
+	function q() public pure {
+		assert(MyInt8.unwrap(g(1)) == 1);
+		assert(MyInt8.unwrap(g(2)) == 2);
+		assert(MyInt8.unwrap(g(255)) == -1);
+		assert(MyInt8.unwrap(g(257)) == 1);
+		assert(MyInt8.unwrap(g(257)) == -1); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (428-465): CHC: Assertion violation happens here.
+// Warning 6328: (665-700): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n(true || true || true || true || true)\nReentrancy property(ies) for :C:\n(true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true || true)\n(true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true)\n(true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true)\n(true || true || true || true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(MyUInt8.unwrap(f(1)) == 1)\n<errorCode> = 2 -> Assertion failed at assert(MyUInt8.unwrap(f(2)) == 2)\n<errorCode> = 3 -> Assertion failed at assert(MyUInt8.unwrap(f(257)) == 1)\n<errorCode> = 4 -> Assertion failed at assert(MyUInt8.unwrap(f(257)) == 257)\n<errorCode> = 6 -> Assertion failed at assert(MyInt8.unwrap(g(1)) == 1)\n<errorCode> = 7 -> Assertion failed at assert(MyInt8.unwrap(g(2)) == 2)\n<errorCode> = 8 -> Assertion failed at assert(MyInt8.unwrap(g(255)) == -1)\n<errorCode> = 9 -> Assertion failed at assert(MyInt8.unwrap(g(257)) == 1)\n<errorCode> = 10 -> Assertion failed at assert(MyInt8.unwrap(g(257)) == -1)\n
--- a/test/libsolidity/smtCheckerTests/userTypes/conversion_2.sol
+++ b/test/libsolidity/smtCheckerTests/userTypes/conversion_2.sol
@ -0,0 +1,32 @@
+pragma abicoder v2;
+
+type MyUInt8 is uint8;
+type MyInt8 is int8;
+type MyUInt16 is uint16;
+
+contract C {
+	function h(MyUInt8 a) internal pure returns (MyInt8) {
+		return MyInt8.wrap(int8(MyUInt8.unwrap(a)));
+	}
+	function i(MyUInt8 a) internal pure returns(MyUInt16) {
+		return MyUInt16.wrap(MyUInt8.unwrap(a));
+	}
+
+	function r() public pure {
+		assert(MyInt8.unwrap(h(MyUInt8.wrap(1))) == 1);
+		assert(MyInt8.unwrap(h(MyUInt8.wrap(2))) == 2);
+		assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == -1);
+		assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == 1); // should fail
+	}
+
+	function s() public pure {
+		assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 250);
+		assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (497-545): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.r()\n    C.h(1) -- internal call\n    C.h(2) -- internal call\n    C.h(255) -- internal call\n    C.h(255) -- internal call
+// Warning 6328: (652-702): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.s()\n    C.i(250) -- internal call\n    C.i(250) -- internal call
+// Info 1180: Contract invariant(s) for :C:\n(true || true || true || true || true)\nReentrancy property(ies) for :C:\n(((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true || true || true)\n(true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true || true)\n(true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(MyInt8.unwrap(h(MyUInt8.wrap(1))) == 1)\n<errorCode> = 2 -> Assertion failed at assert(MyInt8.unwrap(h(MyUInt8.wrap(2))) == 2)\n<errorCode> = 3 -> Assertion failed at assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == -1)\n<errorCode> = 4 -> Assertion failed at assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == 1)\n<errorCode> = 6 -> Assertion failed at assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 250)\n<errorCode> = 7 -> Assertion failed at assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 0)\n
--- a/test/libsolidity/smtCheckerTests/userTypes/conversion_3.sol
+++ b/test/libsolidity/smtCheckerTests/userTypes/conversion_3.sol
@ -0,0 +1,34 @@
+pragma abicoder v2;
+
+type MyUInt8 is uint8;
+type MyInt8 is int8;
+type MyUInt16 is uint16;
+
+contract C {
+	function j(MyUInt8 a) internal pure returns (uint) {
+		return MyUInt8.unwrap(a);
+	}
+	function k(MyUInt8 a) internal pure returns (MyUInt16) {
+		return MyUInt16.wrap(MyUInt8.unwrap(a));
+	}
+
+	function t() public pure {
+		assert(j(MyUInt8.wrap(1)) == 1);
+		assert(j(MyUInt8.wrap(2)) == 2);
+		assert(j(MyUInt8.wrap(255)) == 0xff);
+		assert(j(MyUInt8.wrap(255)) == 1); // should fail
+	}
+
+	function v() public pure {
+		assert(MyUInt16.unwrap(k(MyUInt8.wrap(1))) == 1);
+		assert(MyUInt16.unwrap(k(MyUInt8.wrap(2))) == 2);
+		assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 0xff);
+		assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 1); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (434-467): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.t()\n    C.j(1) -- internal call\n    C.j(2) -- internal call\n    C.j(255) -- internal call\n    C.j(255) -- internal call
+// Warning 6328: (679-729): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.v()\n    C.k(1) -- internal call\n    C.k(2) -- internal call\n    C.k(255) -- internal call\n    C.k(255) -- internal call
+// Info 1180: Contract invariant(s) for :C:\n(true || true || true || true || true)\nReentrancy property(ies) for :C:\n(((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true || true || true)\n(true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true)\n(true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || true || true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true)\n(true || true || true || true || true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(j(MyUInt8.wrap(1)) == 1)\n<errorCode> = 2 -> Assertion failed at assert(j(MyUInt8.wrap(2)) == 2)\n<errorCode> = 3 -> Assertion failed at assert(j(MyUInt8.wrap(255)) == 0xff)\n<errorCode> = 4 -> Assertion failed at assert(j(MyUInt8.wrap(255)) == 1)\n<errorCode> = 6 -> Assertion failed at assert(MyUInt16.unwrap(k(MyUInt8.wrap(1))) == 1)\n<errorCode> = 7 -> Assertion failed at assert(MyUInt16.unwrap(k(MyUInt8.wrap(2))) == 2)\n<errorCode> = 8 -> Assertion failed at assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 0xff)\n<errorCode> = 9 -> Assertion failed at assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 1)\n
--- a/test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol
+++ b/test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol
@ -0,0 +1,24 @@
+pragma abicoder v2;
+
+type MyUInt8 is uint8;
+type MyInt8 is int8;
+type MyUInt16 is uint16;
+
+contract C {
+	function m(MyUInt16 a) internal pure returns (MyUInt8) {
+		return MyUInt8.wrap(uint8(MyUInt16.unwrap(a)));
+	}
+
+	function w() public pure {
+		assert(MyUInt8.unwrap(m(MyUInt16.wrap(1))) == 1);
+		assert(MyUInt8.unwrap(m(MyUInt16.wrap(2))) == 2);
+		assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 0xff);
+		assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 1); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (407-457): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n(true || true || true)\nReentrancy property(ies) for :C:\n(((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(1))) == 1)\n<errorCode> = 2 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(2))) == 2)\n<errorCode> = 3 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 0xff)\n<errorCode> = 4 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 1)\n
--- a/test/libsolidity/syntaxTests/freeFunctions/free_constructor.sol
+++ b/test/libsolidity/syntaxTests/freeFunctions/free_constructor.sol
@ -1,3 +1,3 @@
 constructor() {}
 // ----
-// ParserError 7858: (0-11): Expected pragma, import directive or contract/interface/library/struct/enum/constant/function definition.
+// ParserError 7858: (0-11): Expected pragma, import directive or contract/interface/library/struct/enum/constant/function/error definition.
--- a/test/libsolidity/syntaxTests/freeFunctions/free_fallback.sol
+++ b/test/libsolidity/syntaxTests/freeFunctions/free_fallback.sol
@ -1,3 +1,3 @@
 fallback(){}
 // ----
-// ParserError 7858: (0-8): Expected pragma, import directive or contract/interface/library/struct/enum/constant/function definition.
+// ParserError 7858: (0-8): Expected pragma, import directive or contract/interface/library/struct/enum/constant/function/error definition.
--- a/test/libsolidity/syntaxTests/freeFunctions/free_receive.sol
+++ b/test/libsolidity/syntaxTests/freeFunctions/free_receive.sol
@ -1,3 +1,3 @@
 receive() {}
 // ----
-// ParserError 7858: (0-7): Expected pragma, import directive or contract/interface/library/struct/enum/constant/function definition.
+// ParserError 7858: (0-7): Expected pragma, import directive or contract/interface/library/struct/enum/constant/function/error definition.
--- a/test/libsolidity/syntaxTests/inlineAssembly/evm_byzantium.sol
+++ b/test/libsolidity/syntaxTests/inlineAssembly/evm_byzantium.sol
@ -1,5 +1,5 @@
 contract C {
-    function f() pure external {
+    function f() view external {
        assembly {
            let s := returndatasize()
            returndatacopy(0, 0, s)
--- a/test/libsolidity/syntaxTests/inlineAssembly/evm_byzantium_on_homestead.sol
+++ b/test/libsolidity/syntaxTests/inlineAssembly/evm_byzantium_on_homestead.sol
@ -1,5 +1,5 @@
 contract C {
-    function f() pure external {
+    function f() view external {
        assembly {
            let s := returndatasize()
            returndatacopy(0, 0, s)
--- a/test/libsolidity/syntaxTests/inlineAssembly/returndatasize_as_variable_call_post_byzantium.sol.sol
+++ b/test/libsolidity/syntaxTests/inlineAssembly/returndatasize_as_variable_call_post_byzantium.sol.sol
@ -1,5 +1,5 @@
 contract C {
-    function f() public pure {
+    function f() public view {
        uint returndatasize;
        returndatasize;
        assembly {
--- a/test/libsolidity/syntaxTests/inlineAssembly/returndatasize_as_variable_post_byzantium.sol
+++ b/test/libsolidity/syntaxTests/inlineAssembly/returndatasize_as_variable_post_byzantium.sol
@ -1,5 +1,5 @@
 contract C {
-    function f() public pure {
+    function f() public view {
        uint returndatasize;
        returndatasize;
        assembly {
--- a/test/libsolidity/syntaxTests/inlineAssembly/returndatasize_as_variable_pre_byzantium.sol
+++ b/test/libsolidity/syntaxTests/inlineAssembly/returndatasize_as_variable_pre_byzantium.sol
@ -1,4 +1,4 @@
-contract C { function f() public pure { uint returndatasize; returndatasize; assembly { pop(returndatasize()) }}}
+contract C { function f() public view { uint returndatasize; returndatasize; assembly { pop(returndatasize()) }}}
 // ====
 // EVMVersion: =homestead
 // ----
--- a/test/libsolidity/syntaxTests/unexpected.sol
+++ b/test/libsolidity/syntaxTests/unexpected.sol
@ -1,3 +1,3 @@
 unexpected
 // ----
-// ParserError 7858: (0-10): Expected pragma, import directive or contract/interface/library/struct/enum/constant/function definition.
+// ParserError 7858: (0-10): Expected pragma, import directive or contract/interface/library/struct/enum/constant/function/error definition.
--- a/test/libsolidity/syntaxTests/using/global_inside_contract.sol
+++ b/test/libsolidity/syntaxTests/using/global_inside_contract.sol
@ -4,4 +4,3 @@ contract C {
 function f(uint) pure{}
 // ----
 // SyntaxError 3367: (17-43): "global" can only be used at file level.
-// TypeError 8841: (17-43): Can only use "global" with user-defined types.
--- a/test/libsolidity/syntaxTests/using/global_library_for_builtin.sol
+++ b/test/libsolidity/syntaxTests/using/global_library_for_builtin.sol
@ -0,0 +1,9 @@
+using L for uint global;
+using L for uint[] global;
+using L for function() returns (uint) global;
+library L {
+}
+// ----
+// TypeError 8841: (0-24): Can only use "global" with user-defined types.
+// TypeError 8841: (25-51): Can only use "global" with user-defined types.
+// TypeError 8841: (52-97): Can only use "global" with user-defined types.
--- a/test/libsolidity/syntaxTests/using/global_library_for_defined_elsewhere.sol
+++ b/test/libsolidity/syntaxTests/using/global_library_for_defined_elsewhere.sol
@ -0,0 +1,6 @@
+using L for L.S global;
+library L {
+    struct S { uint x; }
+}
+// ----
+// TypeError 4117: (0-23): Can only use "global" with types defined in the same source unit at file level.
--- a/test/libsolidity/syntaxTests/using/global_library_for_interface.sol
+++ b/test/libsolidity/syntaxTests/using/global_library_for_interface.sol
@ -0,0 +1,6 @@
+interface I {}
+using L for I global;
+library L {
+}
+// ----
+// TypeError 8841: (15-36): Can only use "global" with user-defined types.
--- a/test/libsolidity/syntaxTests/using/global_library_foreign.sol
+++ b/test/libsolidity/syntaxTests/using/global_library_foreign.sol
@ -0,0 +1,8 @@
+==== Source: A ====
+struct S { uint x; }
+==== Source: B ====
+library L {}
+using L for S global;
+import {S} from "A";
+// ----
+// TypeError 4117: (B:13-34): Can only use "global" with types defined in the same source unit at file level.
--- a/test/libsolidity/syntaxTests/using/global_library_with_asterisk.sol
+++ b/test/libsolidity/syntaxTests/using/global_library_with_asterisk.sol
@ -0,0 +1,5 @@
+using L for * global;
+library L {}
+// ----
+// SyntaxError 8118: (0-21): The type has to be specified explicitly at file level (cannot use '*').
+// SyntaxError 2854: (0-21): Can only globally bind functions to specific types.
--- a/test/libsolidity/syntaxTests/using/global_with_asterisk.sol
+++ b/test/libsolidity/syntaxTests/using/global_with_asterisk.sol
@ -0,0 +1,5 @@
+using {f} for * global;
+function f(uint) pure{}
+// ----
+// SyntaxError 8118: (0-23): The type has to be specified explicitly at file level (cannot use '*').
+// SyntaxError 2854: (0-23): Can only globally bind functions to specific types.
--- a/test/libsolidity/syntaxTests/viewPureChecker/inline_assembly_instructions_allowed.sol
+++ b/test/libsolidity/syntaxTests/viewPureChecker/inline_assembly_instructions_allowed.sol
@ -0,0 +1,92 @@
+contract C {
+    function f() public {
+        assembly {
+            stop()
+            pop(add(0, 1))
+            pop(sub(0, 1))
+            pop(mul(0, 1))
+            pop(div(0, 1))
+            pop(sdiv(0, 1))
+            pop(mod(0, 1))
+            pop(smod(0, 1))
+            pop(exp(0, 1))
+            pop(not(0))
+            pop(lt(0, 1))
+            pop(gt(0, 1))
+            pop(slt(0, 1))
+            pop(sgt(0, 1))
+            pop(eq(0, 1))
+            pop(iszero(0))
+            pop(and(0, 1))
+            pop(or(0, 1))
+            pop(xor(0, 1))
+            pop(byte(0, 1))
+            pop(shl(0, 1))
+            pop(shr(0, 1))
+            pop(sar(0, 1))
+            pop(addmod(0, 1, 2))
+            pop(mulmod(0, 1, 2))
+            pop(signextend(0, 1))
+            pop(keccak256(0, 1))
+            pop(0)
+            pop(mload(0))
+            mstore(0, 1)
+            mstore8(0, 1)
+            pop(sload(0))
+            sstore(0, 1)
+            pop(gas())
+            pop(address())
+            pop(balance(0))
+            pop(selfbalance())
+            pop(caller())
+            pop(callvalue())
+            pop(calldataload(0))
+            pop(calldatasize())
+            calldatacopy(0, 1, 2)
+            pop(codesize())
+            codecopy(0, 1, 2)
+            pop(extcodesize(0))
+            extcodecopy(0, 1, 2, 3)
+            pop(returndatasize())
+            returndatacopy(0, 1, 2)
+            pop(extcodehash(0))
+            pop(create(0, 1, 2))
+            pop(create2(0, 1, 2, 3))
+            pop(call(0, 1, 2, 3, 4, 5, 6))
+            pop(callcode(0, 1, 2, 3, 4, 5, 6))
+            pop(delegatecall(0, 1, 2, 3, 4, 5))
+            pop(staticcall(0, 1, 2, 3, 4, 5))
+            return(0, 1)
+            revert(0, 1)
+            selfdestruct(0)
+            invalid()
+            log0(0, 1)
+            log1(0, 1, 2)
+            log2(0, 1, 2, 3)
+            log3(0, 1, 2, 3, 4)
+            log4(0, 1, 2, 3, 4, 5)
+            pop(chainid())
+            pop(basefee())
+            pop(origin())
+            pop(gasprice())
+            pop(blockhash(0))
+            pop(coinbase())
+            pop(timestamp())
+            pop(number())
+            pop(difficulty())
+            pop(gaslimit())
+
+            // NOTE: msize() is allowed only with optimizer disabled
+            //pop(msize())
+            //pop(pc())
+        }
+    }
+}
+// ====
+// EVMVersion: >=london
+// ----
+// Warning 5740: (89-1716): Unreachable code.
+// Warning 5740: (1729-1741): Unreachable code.
+// Warning 5740: (1754-1769): Unreachable code.
+// Warning 5740: (1782-1791): Unreachable code.
+// Warning 5740: (1804-2215): Unreachable code.
--- a/test/libsolidity/syntaxTests/viewPureChecker/inline_assembly_instructions_allowed_pure.sol
+++ b/test/libsolidity/syntaxTests/viewPureChecker/inline_assembly_instructions_allowed_pure.sol
@ -0,0 +1,90 @@
+contract C {
+    function f() public pure {
+        assembly {
+            stop()
+            pop(add(0, 1))
+            pop(sub(0, 1))
+            pop(mul(0, 1))
+            pop(div(0, 1))
+            pop(sdiv(0, 1))
+            pop(mod(0, 1))
+            pop(smod(0, 1))
+            pop(exp(0, 1))
+            pop(not(0))
+            pop(lt(0, 1))
+            pop(gt(0, 1))
+            pop(slt(0, 1))
+            pop(sgt(0, 1))
+            pop(eq(0, 1))
+            pop(iszero(0))
+            pop(and(0, 1))
+            pop(or(0, 1))
+            pop(xor(0, 1))
+            pop(byte(0, 1))
+            pop(shl(0, 1))
+            pop(shr(0, 1))
+            pop(sar(0, 1))
+            pop(addmod(0, 1, 2))
+            pop(mulmod(0, 1, 2))
+            pop(signextend(0, 1))
+            pop(keccak256(0, 1))
+            pop(0)
+            pop(mload(0))
+            mstore(0, 1)
+            mstore8(0, 1)
+            //pop(sload(0))
+            //sstore(0, 1)
+            //pop(gas())
+            //pop(address())
+            //pop(balance(0))
+            //pop(selfbalance())
+            //pop(caller())
+            //pop(callvalue())
+            pop(calldataload(0))
+            pop(calldatasize())
+            calldatacopy(0, 1, 2)
+            pop(codesize())
+            codecopy(0, 1, 2)
+            //pop(extcodesize(0))
+            //extcodecopy(0, 1, 2, 3)
+            //pop(returndatasize())
+            //returndatacopy(0, 1, 2)
+            //pop(extcodehash(0))
+            //pop(create(0, 1, 2))
+            //pop(create2(0, 1, 2, 3))
+            //pop(call(0, 1, 2, 3, 4, 5, 6))
+            //pop(callcode(0, 1, 2, 3, 4, 5, 6))
+            //pop(delegatecall(0, 1, 2, 3, 4, 5))
+            //pop(staticcall(0, 1, 2, 3, 4, 5))
+            return(0, 1)
+            revert(0, 1)
+            //selfdestruct(0)
+            invalid()
+            //log0(0, 1)
+            //log1(0, 1, 2)
+            //log2(0, 1, 2, 3)
+            //log3(0, 1, 2, 3, 4)
+            //log4(0, 1, 2, 3, 4, 5)
+            //pop(chainid())
+            //pop(basefee())
+            //pop(origin())
+            //pop(gasprice())
+            //pop(blockhash(0))
+            //pop(coinbase())
+            //pop(timestamp())
+            //pop(number())
+            //pop(difficulty())
+            //pop(gaslimit())
+
+            // NOTE: msize() is allowed only with optimizer disabled
+            //pop(msize())
+            //pop(pc())
+        }
+    }
+}
+// ====
+// EVMVersion: >=london
+// ----
+// Warning 5740: (94-1759): Unreachable code.
+// Warning 5740: (1772-1784): Unreachable code.
+// Warning 5740: (1827-1836): Unreachable code.
--- a/test/libsolidity/syntaxTests/viewPureChecker/inline_assembly_instructions_allowed_view.sol
+++ b/test/libsolidity/syntaxTests/viewPureChecker/inline_assembly_instructions_allowed_view.sol
@ -0,0 +1,91 @@
+contract C {
+    function f() public view {
+        assembly {
+            stop()
+            pop(add(0, 1))
+            pop(sub(0, 1))
+            pop(mul(0, 1))
+            pop(div(0, 1))
+            pop(sdiv(0, 1))
+            pop(mod(0, 1))
+            pop(smod(0, 1))
+            pop(exp(0, 1))
+            pop(not(0))
+            pop(lt(0, 1))
+            pop(gt(0, 1))
+            pop(slt(0, 1))
+            pop(sgt(0, 1))
+            pop(eq(0, 1))
+            pop(iszero(0))
+            pop(and(0, 1))
+            pop(or(0, 1))
+            pop(xor(0, 1))
+            pop(byte(0, 1))
+            pop(shl(0, 1))
+            pop(shr(0, 1))
+            pop(sar(0, 1))
+            pop(addmod(0, 1, 2))
+            pop(mulmod(0, 1, 2))
+            pop(signextend(0, 1))
+            pop(keccak256(0, 1))
+            pop(0)
+            pop(mload(0))
+            mstore(0, 1)
+            mstore8(0, 1)
+            pop(sload(0))
+            //sstore(0, 1)
+            pop(gas())
+            pop(address())
+            pop(balance(0))
+            pop(selfbalance())
+            pop(caller())
+            pop(callvalue())
+            pop(calldataload(0))
+            pop(calldatasize())
+            calldatacopy(0, 1, 2)
+            pop(codesize())
+            codecopy(0, 1, 2)
+            pop(extcodesize(0))
+            extcodecopy(0, 1, 2, 3)
+            pop(returndatasize())
+            returndatacopy(0, 1, 2)
+            pop(extcodehash(0))
+            //pop(create(0, 1, 2))
+            //pop(create2(0, 1, 2, 3))
+            //pop(call(0, 1, 2, 3, 4, 5, 6))
+            //pop(callcode(0, 1, 2, 3, 4, 5, 6))
+            //pop(delegatecall(0, 1, 2, 3, 4, 5))
+            pop(staticcall(0, 1, 2, 3, 4, 5))
+            return(0, 1)
+            revert(0, 1)
+            //selfdestruct(0)
+            invalid()
+            //log0(0, 1)
+            //log1(0, 1, 2)
+            //log2(0, 1, 2, 3)
+            //log3(0, 1, 2, 3, 4)
+            //log4(0, 1, 2, 3, 4, 5)
+            pop(chainid())
+            pop(basefee())
+            pop(origin())
+            pop(gasprice())
+            pop(blockhash(0))
+            pop(coinbase())
+            pop(timestamp())
+            pop(number())
+            pop(difficulty())
+            pop(gaslimit())
+
+            // NOTE: msize() is allowed only with optimizer disabled
+            //pop(msize())
+            //pop(pc())
+        }
+    }
+}
+// ====
+// EVMVersion: >=london
+// ----
+// Warning 5740: (94-1733): Unreachable code.
+// Warning 5740: (1746-1758): Unreachable code.
+// Warning 5740: (1801-1810): Unreachable code.
+// Warning 5740: (1978-2244): Unreachable code.
--- a/test/libsolidity/syntaxTests/viewPureChecker/inline_assembly_instructions_disallowed.sol
+++ b/test/libsolidity/syntaxTests/viewPureChecker/inline_assembly_instructions_disallowed.sol
@ -0,0 +1,28 @@
+contract C {
+    function f() public {
+        assembly {
+            datasize(0)
+            dataoffset(0)
+            datacopy(0, 1, 2)
+            setimmutable(0, "x", 1)
+            loadimmutable("x")
+            linkersymbol("x")
+            memoryguard(0)
+            verbatim_1i_1o(hex"600202", 0)
+
+            pop(msize())
+            pop(pc())
+        }
+    }
+}
+// ----
+// SyntaxError 6553: (47-362): The msize instruction cannot be used when the Yul optimizer is activated because it can change its semantics. Either disable the Yul optimizer or do not use the instruction.
+// DeclarationError 4619: (70-78): Function "datasize" not found.
+// DeclarationError 4619: (94-104): Function "dataoffset" not found.
+// DeclarationError 4619: (120-128): Function "datacopy" not found.
+// DeclarationError 4619: (150-162): Function "setimmutable" not found.
+// DeclarationError 4619: (186-199): Function "loadimmutable" not found.
+// DeclarationError 4619: (217-229): Function "linkersymbol" not found.
+// DeclarationError 4619: (247-258): Function "memoryguard" not found.
+// DeclarationError 4619: (274-288): Function "verbatim_1i_1o" not found.
+// SyntaxError 2450: (347-349): PC instruction is a low-level EVM feature. Because of that PC is disallowed in strict assembly.
--- a/Show More
+++ b/Show More