Merge remote-tracking branch 'origin/develop' into breaking

.circleci/config.yml

@@ -121,18 +121,7 @@ defaults:
       no_output_timeout: 30m
       command: ./.circleci/soltest_all.sh
 
-  - run_cmdline_tests: &run_cmdline_tests
+  - run_soltest_steps: &run_soltest_steps
-      name: command line tests
-      no_output_timeout: 30m
-      command: ./test/cmdlineTests.sh
-
-  - run_docs_pragma_min_version: &run_docs_pragma_min_version
-      name: docs pragma version check
-      command: ./scripts/docs_version_pragma_check.sh
-
-  - test_ubuntu1604_clang: &test_ubuntu1604_clang
-      docker:
-        - image: << pipeline.parameters.ubuntu-1604-clang-ossfuzz-docker-image >>
       steps:
         - checkout
         - attach_workspace:
@@ -141,21 +130,7 @@ defaults:
         - store_test_results: *store_test_results
         - store_artifacts: *artifacts_test_results
 
-  - test_ubuntu2004_clang: &test_ubuntu2004_clang
+  - run_soltest_all_steps: &run_soltest_all_steps
-      docker:
-        - image: << pipeline.parameters.ubuntu-2004-clang-docker-image >>
-      steps:
-        - checkout
-        - attach_workspace:
-            at: build
-        - run: *run_soltest
-        - store_test_results: *store_test_results
-        - store_artifacts: *artifacts_test_results
-
-  - test_ubuntu2004: &test_ubuntu2004
-      docker:
-        - image: << pipeline.parameters.ubuntu-2004-docker-image >>
-      parallelism: 6
       steps:
         - checkout
         - attach_workspace:
@@ -164,27 +139,48 @@ defaults:
         - store_test_results: *store_test_results
         - store_artifacts: *artifacts_test_results
 
+  - run_cmdline_tests: &run_cmdline_tests
+      name: command line tests
+      no_output_timeout: 30m
+      command: ./test/cmdlineTests.sh
+
+  - run_cmdline_tests_steps: &run_cmdline_tests_steps
+      steps:
+        - checkout
+        - attach_workspace:
+            at: build
+        - run: *run_cmdline_tests
+        - store_test_results: *store_test_results
+        - store_artifacts: *artifacts_test_results
+
+  - run_docs_pragma_min_version: &run_docs_pragma_min_version
+      name: docs pragma version check
+      command: ./scripts/docs_version_pragma_check.sh
+
+  - test_ubuntu1604_clang: &test_ubuntu1604_clang
+      docker:
+        - image: << pipeline.parameters.ubuntu-1604-clang-ossfuzz-docker-image >>
+      <<: *run_soltest_steps
+
+  - test_ubuntu2004_clang: &test_ubuntu2004_clang
+      docker:
+        - image: << pipeline.parameters.ubuntu-2004-clang-docker-image >>
+      <<: *run_soltest_steps
+
+  - test_ubuntu2004: &test_ubuntu2004
+      docker:
+        - image: << pipeline.parameters.ubuntu-2004-docker-image >>
+      parallelism: 6
+      <<: *run_soltest_all_steps
+
   - test_asan: &test_asan
       <<: *test_ubuntu2004
-      steps:
+      <<: *run_soltest_steps
-      - checkout
-      - attach_workspace:
-          at: build
-      - run:
-          <<: *run_soltest
-      - store_test_results: *store_test_results
-      - store_artifacts: *artifacts_test_results
 
-  - test_asan_clang: &test_asan_clang
+  - test_ubuntu2004_clang_cli: &test_ubuntu2004_clang_cli
-      <<: *test_ubuntu2004_clang
+      docker:
-      steps:
+        - image: << pipeline.parameters.ubuntu-2004-clang-docker-image >>
-      - checkout
+      <<: *run_cmdline_tests_steps
-      - attach_workspace:
-          at: build
-      - run:
-          <<: *run_soltest
-      - store_test_results: *store_test_results
-      - store_artifacts: *artifacts_test_results
 
   # --------------------------------------------------------------------------
   # Workflow Templates
@@ -239,6 +235,11 @@ defaults:
       requires:
         - b_ubu_asan_clang
 
+  - workflow_ubuntu2004_ubsan_clang: &workflow_ubuntu2004_ubsan_clang
+      <<: *workflow_trigger_on_tags
+      requires:
+        - b_ubu_ubsan_clang
+
   - workflow_emscripten: &workflow_emscripten
       <<: *workflow_trigger_on_tags
       requires:
@@ -367,7 +368,7 @@ jobs:
       - checkout
       - run:
           name: Install Java
-          command: apt -q update && apt install -y openjdk-14-jdk
+          command: apt -q update && apt install -y openjdk-16-jdk
       - run:
           name: Run tests
           command: ./scripts/test_antlr_grammar.sh
@@ -433,7 +434,7 @@ jobs:
           name: Python unit tests
           command: python.exe test/pyscriptTests.py
 
-  b_ubu_clang: &build_ubuntu2004_clang
+  b_ubu_clang: &b_ubu_clang
     resource_class: xlarge
     docker:
       - image: << pipeline.parameters.ubuntu-2004-clang-docker-image >>
@@ -447,8 +448,7 @@ jobs:
       - store_artifacts: *artifacts_solc
       - persist_to_workspace: *artifacts_executables
 
-
+  b_ubu_asan_clang: &b_ubu_asan_clang
-  b_ubu_asan_clang: &build_ubuntu2004_clang
     docker:
       - image: << pipeline.parameters.ubuntu-2004-clang-docker-image >>
     environment:
@@ -462,7 +462,22 @@ jobs:
       - store_artifacts: *artifacts_solc
       - persist_to_workspace: *artifacts_executables
 
-  b_ubu: &build_ubuntu2004
+  b_ubu_ubsan_clang: &b_ubu_ubsan_clang
+    docker:
+      - image: << pipeline.parameters.ubuntu-2004-clang-docker-image >>
+    environment:
+      CC: clang
+      CXX: clang++
+      CMAKE_OPTIONS: -DSANITIZE=undefined
+      MAKEFLAGS: -j 3
+    steps:
+      - checkout
+      - run: *run_build
+      - run: *gitter_notify_failure
+      - store_artifacts: *artifacts_solc
+      - persist_to_workspace: *artifacts_executables
+
+  b_ubu: &b_ubu
     resource_class: xlarge
     docker:
       - image: << pipeline.parameters.ubuntu-2004-docker-image >>
@@ -475,14 +490,14 @@ jobs:
       - store_artifacts: *artifacts_tools
       - persist_to_workspace: *artifacts_executables
 
-  b_ubu_release: &build_ubuntu2004_release
+  b_ubu_release: &b_ubu_release
-    <<: *build_ubuntu2004
+    <<: *b_ubu
     environment:
       FORCE_RELEASE: ON
       MAKEFLAGS: -j 10
 
   b_ubu_static:
-    <<: *build_ubuntu2004
+    <<: *b_ubu
     environment:
       MAKEFLAGS: -j 10
       CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Release -DUSE_Z3_DLOPEN=ON -DUSE_CVC4=OFF -DSOLC_STATIC_STDLIBS=ON
@@ -495,7 +510,7 @@ jobs:
       - store_artifacts: *artifacts_solc
 
   b_ubu_codecov:
-    <<: *build_ubuntu2004
+    <<: *b_ubu
     environment:
       COVERAGE: ON
       CMAKE_BUILD_TYPE: Debug
@@ -529,7 +544,7 @@ jobs:
   # Builds in C++20 mode and uses debug build in order to speed up.
   # Do *NOT* store any artifacts or workspace as we don't run tests on this build.
   b_ubu_cxx20:
-    <<: *build_ubuntu2004
+    <<: *b_ubu
     environment:
       CMAKE_BUILD_TYPE: Debug
       CMAKE_OPTIONS: -DCMAKE_CXX_STANDARD=20 -DUSE_CVC4=OFF
@@ -538,7 +553,7 @@ jobs:
       - checkout
       - run: *run_build
 
-  b_ubu_ossfuzz: &build_ubuntu1604_clang
+  b_ubu_ossfuzz: &b_ubu_ossfuzz
     docker:
       - image: << pipeline.parameters.ubuntu-1604-clang-ossfuzz-docker-image >>
     environment:
@@ -683,7 +698,7 @@ jobs:
 
   # x64 ASAN build, for testing for memory related bugs
   b_ubu_asan: &b_ubu_asan
-    <<: *build_ubuntu2004
+    <<: *b_ubu
     environment:
       CMAKE_OPTIONS: -DSANITIZE=address
       MAKEFLAGS: -j 10
@@ -768,13 +783,7 @@ jobs:
       - image: << pipeline.parameters.ubuntu-2004-docker-image >>
     environment:
       TERM: xterm
-    steps:
+    <<: *run_cmdline_tests_steps
-      - checkout
-      - attach_workspace:
-          at: build
-      - run: *run_cmdline_tests
-      - store_test_results: *store_test_results
-      - store_artifacts: *artifacts_test_results
 
   t_ubu_release_cli: &t_ubu_release_cli
     <<: *t_ubu_cli
@@ -784,14 +793,7 @@ jobs:
     environment:
       TERM: xterm
       ASAN_OPTIONS: check_initialization_order=true:detect_stack_use_after_return=true:strict_init_order=true:strict_string_checks=true:detect_invalid_pointer_pairs=2
-    steps:
+    <<: *run_cmdline_tests_steps
-      - checkout
-      - attach_workspace:
-          at: build
-      - run:
-          <<: *run_cmdline_tests
-      - store_test_results: *store_test_results
-      - store_artifacts: *artifacts_test_results
 
   t_ubu_asan_constantinople:
     <<: *test_asan
@@ -802,13 +804,37 @@ jobs:
       ASAN_OPTIONS: check_initialization_order=true:detect_stack_use_after_return=true:strict_init_order=true:strict_string_checks=true:detect_invalid_pointer_pairs=2
 
   t_ubu_asan_constantinople_clang:
-    <<: *test_asan_clang
+    <<: *test_ubuntu2004_clang
     environment:
       EVM: constantinople
       OPTIMIZE: 0
       SOLTEST_FLAGS: --no-smt
       ASAN_OPTIONS: check_initialization_order=true:detect_stack_use_after_return=true:strict_init_order=true:strict_string_checks=true:detect_invalid_pointer_pairs=2
 
+  t_ubu_ubsan_clang:
+    docker:
+      - image: << pipeline.parameters.ubuntu-2004-clang-docker-image >>
+    steps:
+      - checkout
+      - attach_workspace:
+          at: build
+      - run: *run_soltest
+      - run: *gitter_notify_failure
+      - store_test_results: *store_test_results
+      - store_artifacts: *artifacts_test_results
+
+  t_ubu_ubsan_clang_cli:
+    docker:
+      - image: << pipeline.parameters.ubuntu-2004-clang-docker-image >>
+    steps:
+      - checkout
+      - attach_workspace:
+          at: build
+      - run: *run_cmdline_tests
+      - run: *gitter_notify_failure
+      - store_test_results: *store_test_results
+      - store_artifacts: *artifacts_test_results
+
   t_ems_solcjs:
     docker:
       - image: << pipeline.parameters.ubuntu-2004-docker-image >>
@@ -1208,6 +1234,11 @@ workflows:
       - t_ubu_asan_constantinople_clang: *workflow_ubuntu2004_asan_clang
       - t_ubu_asan_cli: *workflow_ubuntu2004_asan
 
+      # UBSan build and tests
+      - b_ubu_ubsan_clang: *workflow_trigger_on_tags
+      - t_ubu_ubsan_clang: *workflow_ubuntu2004_ubsan_clang
+      - t_ubu_ubsan_clang_cli: *workflow_ubuntu2004_ubsan_clang
+
       # Emscripten build and tests that take more than 15 minutes to execute
       - b_ems: *workflow_trigger_on_tags
       - t_ems_ext:

Changelog.md

@@ -11,12 +11,17 @@ Language Features:
 
 
 Compiler Features:
+ * Commandline Interface: Normalize paths specified on the command line and make them relative for files located inside base path.
  * Immutable variables can be read at construction time once they are initialized.
  * SMTChecker: Support low level ``call`` as external calls to unknown code.
+ * SMTChecker: Add constraints to better correlate ``address(this).balance`` and ``msg.value``.
+ * Commandline Interface: Disallowed the ``--experimental-via-ir`` option to be used with Standard Json, Assembler and Linker modes.
 
 
 Bugfixes:
  * SMTChecker: Fix false positive in external calls from constructors.
+ * SMTChecker: Fix internal error on some multi-source uses of ``abi.*``, cryptographic functions and constants.
+ * SMTChecker: Fix false negative caused by ``push`` on storage array references returned by internal functions.
 
 
 

cmake/EthCompilerSettings.cmake

@@ -192,11 +192,43 @@ endif ()
 
 if (SANITIZE)
 	# Perform case-insensitive string compare
-	string(TOLOWER "${SANITIZE}" san)
+	string(TOLOWER "${SANITIZE}" sanitizer)
 	# -fno-omit-frame-pointer gives more informative stack trace in case of an error
 	# -fsanitize-address-use-after-scope throws an error when a variable is used beyond its scope
-	if (san STREQUAL "address")
+	if (sanitizer STREQUAL "address")
 		set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fno-omit-frame-pointer -fsanitize=address -fsanitize-address-use-after-scope")
+	elseif (sanitizer STREQUAL "undefined")
+		# The following flags not used by fuzzer but used by us may create problems, so consider
+		# disabling them: alignment, pointer-overflow.
+		# Flags are alphabetically sorted and are for clang v10.0
+		list(APPEND undefinedSanitizerChecks
+			alignment
+			array-bounds
+			bool
+			builtin
+			enum
+			float-divide-by-zero
+			function
+			integer-divide-by-zero
+			null
+			object-size
+			pointer-overflow
+			return
+			returns-nonnull-attribute
+			shift
+			signed-integer-overflow
+			unsigned-integer-overflow
+			unreachable
+			vla-bound
+			vptr
+		)
+		list(JOIN undefinedSanitizerChecks "," sanitizerChecks)
+		list(REMOVE_ITEM undefinedSanitizerChecks unsigned-integer-overflow)
+		# The fuzzer excludes reports of unsigned-integer-overflow. Hence, we remove it
+		# from the -fno-sanitize-recover checks. Consider reducing this list if we do not
+		# want to be notified about other failed checks.
+		list(JOIN undefinedSanitizerChecks "," dontRecoverFromChecks)
+		set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fsanitize=${sanitizerChecks} -fno-sanitize-recover=${dontRecoverFromChecks}")
 	endif()
 endif()
 

docs/examples/blind-auction.rst

@@ -64,15 +64,15 @@ to receive their money - contracts cannot activate themselves.
         /// The function auctionEnd has already been called.
         error AuctionEndAlreadyCalled();
 
-        /// Create a simple auction with `_biddingTime`
+        /// Create a simple auction with `biddingTime`
         /// seconds bidding time on behalf of the
-        /// beneficiary address `_beneficiary`.
+        /// beneficiary address `beneficiaryAddress`.
         constructor(
-            uint _biddingTime,
+            uint biddingTime,
-            address payable _beneficiary
+            address payable beneficiaryAddress
         ) {
-            beneficiary = _beneficiary;
+            beneficiary = beneficiaryAddress;
-            auctionEndTime = block.timestamp + _biddingTime;
+            auctionEndTime = block.timestamp + biddingTime;
         }
 
         /// Bid on the auction with the value sent
@@ -232,26 +232,26 @@ invalid bids.
         // functions. `onlyBefore` is applied to `bid` below:
         // The new function body is the modifier's body where
         // `_` is replaced by the old function body.
-        modifier onlyBefore(uint _time) {
+        modifier onlyBefore(uint time) {
-            if (block.timestamp >= _time) revert TooLate(_time);
+            if (block.timestamp >= time) revert TooLate(time);
             _;
         }
-        modifier onlyAfter(uint _time) {
+        modifier onlyAfter(uint time) {
-            if (block.timestamp <= _time) revert TooEarly(_time);
+            if (block.timestamp <= time) revert TooEarly(time);
             _;
         }
 
         constructor(
-            uint _biddingTime,
+            uint biddingTime,
-            uint _revealTime,
+            uint revealTime,
-            address payable _beneficiary
+            address payable beneficiaryAddress
         ) {
-            beneficiary = _beneficiary;
+            beneficiary = beneficiaryAddress;
-            biddingEnd = block.timestamp + _biddingTime;
+            biddingEnd = block.timestamp + biddingTime;
-            revealEnd = biddingEnd + _revealTime;
+            revealEnd = biddingEnd + revealTime;
         }
 
-        /// Place a blinded bid with `_blindedBid` =
+        /// Place a blinded bid with `blindedBid` =
         /// keccak256(abi.encodePacked(value, fake, secret)).
         /// The sent ether is only refunded if the bid is correctly
         /// revealed in the revealing phase. The bid is valid if the
@@ -260,13 +260,13 @@ invalid bids.
         /// not the exact amount are ways to hide the real bid but
         /// still make the required deposit. The same address can
         /// place multiple bids.
-        function bid(bytes32 _blindedBid)
+        function bid(bytes32 blindedBid)
             external
             payable
             onlyBefore(biddingEnd)
         {
             bids[msg.sender].push(Bid({
-                blindedBid: _blindedBid,
+                blindedBid: blindedBid,
                 deposit: msg.value
             }));
         }
@@ -275,24 +275,24 @@ invalid bids.
         /// correctly blinded invalid bids and for all bids except for
         /// the totally highest.
         function reveal(
-            uint[] calldata _values,
+            uint[] calldata values,
-            bool[] calldata _fake,
+            bool[] calldata fakes,
-            bytes32[] calldata _secret
+            bytes32[] calldata secrets
         )
             external
             onlyAfter(biddingEnd)
             onlyBefore(revealEnd)
         {
             uint length = bids[msg.sender].length;
-            require(_values.length == length);
+            require(values.length == length);
-            require(_fake.length == length);
+            require(fakes.length == length);
-            require(_secret.length == length);
+            require(secrets.length == length);
 
             uint refund;
             for (uint i = 0; i < length; i++) {
                 Bid storage bidToCheck = bids[msg.sender][i];
                 (uint value, bool fake, bytes32 secret) =
-                        (_values[i], _fake[i], _secret[i]);
+                        (values[i], fakes[i], secrets[i]);
                 if (bidToCheck.blindedBid != keccak256(abi.encodePacked(value, fake, secret))) {
                     // Bid was not actually revealed.
                     // Do not refund deposit.

docs/examples/micropayment.rst

@@ -346,11 +346,11 @@ The full contract
         address payable public recipient;   // The account receiving the payments.
         uint256 public expiration;  // Timeout in case the recipient never closes.
 
-        constructor (address payable _recipient, uint256 duration)
+        constructor (address payable recipientAddress, uint256 duration)
             payable
         {
             sender = payable(msg.sender);
-            recipient = _recipient;
+            recipient = recipientAddress;
             expiration = block.timestamp + duration;
         }
 

docs/examples/safe-remote.rst

@@ -36,8 +36,8 @@ you can use state machine-like constructs inside a contract.
         // The state variable has a default value of the first member, `State.created`
         State public state;
 
-        modifier condition(bool _condition) {
+        modifier condition(bool condition_) {
-            require(_condition);
+            require(condition_);
             _;
         }
 
@@ -62,8 +62,8 @@ you can use state machine-like constructs inside a contract.
             _;
         }
 
-        modifier inState(State _state) {
+        modifier inState(State state_) {
-            if (state != _state)
+            if (state != state_)
                 revert InvalidState();
             _;
         }

docs/path-resolution.rst

@@ -71,8 +71,10 @@ The initial content of the VFS depends on how you invoke the compiler:
 
        solc contract.sol /usr/local/dapp-bin/token.sol
 
-   The source unit name of a file loaded this way is simply the specified path after shell expansion
+   The source unit name of a file loaded this way is constructed by converting its path to a
-   and with platform-specific separators converted to forward slashes.
+   canonical form and making it relative to the base path if it is located inside.
+   See :ref:`Base Path Normalization and Stripping <base-path-normalization-and-stripping>` for
+   a detailed description of this process.
 
    .. index:: standard JSON
 
@@ -309,9 +311,67 @@ When the source unit name is a relative path, this results in the file being loo
 directory the compiler has been invoked from.
 It is also the only value that results in absolute paths in source unit names being actually
 interpreted as absolute paths on disk.
+If the base path itself is relative, it is interpreted as relative to the current working directory
+of the compiler.
 
-If the base path itself is relative, it is also interpreted as relative to the current working
+.. _base-path-normalization-and-stripping:
-directory of the compiler.
+
+Base Path Normalization and Stripping
+-------------------------------------
+
+On the command line the compiler behaves just as you would expect from any other program:
+it accepts paths in a format native to the platform and relative paths are relative to the current
+working directory.
+The source unit names assigned to files whose paths are specified on the command line, however,
+should not change just because the project is being compiled on a different platform or because the
+compiler happens to have been invoked from a different directory.
+To achieve this, paths to source files coming from the command line must be converted to a canonical
+form, and, if possible, made relative to the base path.
+
+The normalization rules are as follows:
+
+- If a path is relative, it is made absolute by prepending the current working directory to it.
+- Internal ``.`` and ``..`` segments are collapsed.
+- Platform-specific path separators are replaced with forward slashes.
+- Sequences of multiple consecutive path separators are squashed into a single separator (unless
+  they are the leading slashes of an `UNC path <https://en.wikipedia.org/wiki/Path_(computing)#UNC>`_).
+- If the path includes a root name (e.g. a drive letter on Windows) and the root is the same as the
+  root of the current working directory, the root is replaced with ``/``.
+- Symbolic links in the path are **not** resolved.
+
+  - The only exception is the path to the current working directory prepended to relative paths in
+    the process of making them absolute.
+    On some platforms the working directory is reported always with symbolic links resolved so for
+    consistency the compiler resolves them everywhere.
+
+- The original case of the path is preserved even if the filesystem is case-insensitive but
+  `case-preserving <https://en.wikipedia.org/wiki/Case_preservation>`_ and the actual case on
+  disk is different.
+
+.. note::
+
+    There are situations where paths cannot be made platform-independent.
+    For example on Windows the compiler can avoid using drive letters by referring to the root
+    directory of the current drive as ``/`` but drive letters are still necessary for paths leading
+    to other drives.
+    You can avoid such situations by ensuring that all the files are available within a single
+    directory tree on the same drive.
+
+Once canonicalized, the base path is stripped from all source file paths that start with it.
+If the base path is empty or not specified, it is treated as if it was equal to the path to the
+current working directory (with all symbolic links resolved).
+The result is accepted only if the normalized directory path is the exact prefix of the normalized
+file path.
+Otherwise the file path remains absolute.
+This makes the conversion unambiguous and ensures that the relative path does not start with ``../``.
+The resulting file path becomes the source unit name.
+
+.. note::
+
+    Prior to version 0.8.8, CLI path stripping was not performed and the only normalization applied
+    was the conversion of path separators.
+    When working with older versions of the compiler it is recommended to invoke the compiler from
+    the base path and to only use relative paths on the command line.
 
 .. index:: ! remapping; import, ! import; remapping, ! remapping; context, ! remapping; prefix, ! remapping; target
 .. _import-remapping:
@@ -414,7 +474,7 @@ Here are the detailed rules governing the behaviour of remappings:
 
      .. code-block:: bash
 
-         solc /project/=/contracts/ /project/contract.sol --base-path /project # source unit name: /project/contract.sol
+         solc /project/=/contracts/ /project/contract.sol --base-path /project # source unit name: contract.sol
 
      .. code-block:: solidity
          :caption: /project/contract.sol

docs/smtchecker.rst

@@ -830,6 +830,25 @@ are located in storage, even though they also have type ``uint[]``.  However,
 if ``d`` was assigned, we would need to clear knowledge about ``array`` and
 vice-versa.
 
+Contract Balance
+================
+
+A contract may be deployed with funds sent to it, if ``msg.value`` > 0 in the
+deployment transaction.
+However, the contract's address may already have funds before deployment,
+which are kept by the contract.
+Therefore, the SMTChecker assumes that ``address(this).balance >= msg.value``
+in the constructor in order to be consistent with the EVM rules.
+The contract's balance may also increase without triggering any calls to the
+contract, if
+
+- ``selfdestruct`` is executed by another contract with the analyzed contract
+  as the target of the remaining funds,
+- the contract is the coinbase (i.e., ``block.coinbase``) of some block.
+
+To model this properly, the SMTChecker assumes that at every new transaction
+the contract's balance may grow by at least ``msg.value``.
+
 **********************
 Real World Assumptions
 **********************
@@ -841,3 +860,7 @@ push: If the ``push`` operation is applied to an array of length 2^256 - 1, its
 length silently overflows.
 However, this is unlikely to happen in practice, since the operations required
 to grow the array to that point would take billions of years to execute.
+Another similar assumption taken by the SMTChecker is that an address' balance
+can never overflow.
+
+A similar idea was presented in `EIP-1985 <https://eips.ethereum.org/EIPS/eip-1985>`_.

liblangutil/CMakeLists.txt

@@ -25,6 +25,7 @@ set(sources
 	Token.cpp
 	Token.h
 	UndefMacros.h
+	UniqueErrorReporter.h
 )
 
 add_library(langutil ${sources})

liblangutil/Exceptions.h

@@ -105,6 +105,7 @@ struct ErrorId
 	unsigned long long error = 0;
 	bool operator==(ErrorId const& _rhs) const { return error == _rhs.error; }
 	bool operator!=(ErrorId const& _rhs) const { return !(*this == _rhs); }
+	bool operator<(ErrorId const& _rhs) const { return error < _rhs.error; }
 };
 constexpr ErrorId operator"" _error(unsigned long long _error) { return ErrorId{ _error }; }
 

liblangutil/UniqueErrorReporter.h

@@ -0,0 +1,94 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <liblangutil/ErrorReporter.h>
+#include <liblangutil/Exceptions.h>
+
+namespace solidity::langutil
+{
+
+/*
+ * Wrapper for ErrorReporter that removes duplicates.
+ * Two errors are considered the same if their error ID and location are the same.
+ */
+class UniqueErrorReporter
+{
+public:
+	UniqueErrorReporter(): m_errorReporter(m_uniqueErrors) {}
+
+	void warning(ErrorId _error, SourceLocation const& _location, std::string const& _description)
+	{
+		if (!seen(_error, _location, _description))
+		{
+			m_errorReporter.warning(_error, _location, _description);
+			markAsSeen(_error, _location, _description);
+		}
+	}
+
+	void warning(
+		ErrorId _error,
+		SourceLocation const& _location,
+		std::string const& _description,
+		SecondarySourceLocation const& _secondaryLocation
+	)
+	{
+		if (!seen(_error, _location, _description))
+		{
+			m_errorReporter.warning(_error, _location, _description, _secondaryLocation);
+			markAsSeen(_error, _location, _description);
+		}
+	}
+
+	void warning(ErrorId _error, std::string const& _description)
+	{
+		if (!seen(_error, {}, _description))
+		{
+			m_errorReporter.warning(_error, _description);
+			markAsSeen(_error, {}, _description);
+		}
+	}
+
+	bool seen(ErrorId _error, SourceLocation const& _location, std::string const& _description) const
+	{
+		if (m_seenErrors.count({_error, _location}))
+		{
+			solAssert(m_seenErrors.at({_error, _location}) == _description, "");
+			return true;
+		}
+		return false;
+	}
+
+	void markAsSeen(ErrorId _error, SourceLocation const& _location, std::string const& _description)
+	{
+		solAssert(!seen(_error, _location, _description), "");
+		m_seenErrors[{_error, _location}] = _description;
+	}
+
+	ErrorList const& errors() const { return m_errorReporter.errors(); }
+
+	void clear() { m_errorReporter.clear(); }
+
+private:
+	ErrorReporter m_errorReporter;
+	ErrorList m_uniqueErrors;
+	std::map<std::pair<ErrorId, SourceLocation>, std::string> m_seenErrors;
+};
+
+}

libsmtutil/Sorts.h

@@ -159,7 +159,15 @@ struct TupleSort: public Sort
 		name(std::move(_name)),
 		members(std::move(_members)),
 		components(std::move(_components))
-	{}
+	{
+		for (size_t i = 0; i < members.size(); ++i)
+			memberToIndex[members.at(i)] = i;
+	}
+
+	SortPointer memberSort(std::string const& _member)
+	{
+		return components.at(memberToIndex.at(_member));
+	}
 
 	bool operator==(Sort const& _other) const override
 	{
@@ -186,8 +194,10 @@ struct TupleSort: public Sort
 	std::string const name;
 	std::vector<std::string> const members;
 	std::vector<SortPointer> const components;
+	std::map<std::string, size_t> memberToIndex;
 };
 
+
 /** Frequently used sorts.*/
 struct SortProvider
 {

libsolidity/analysis/ControlFlowAnalyzer.cpp

@@ -20,7 +20,8 @@
 
 #include <liblangutil/SourceLocation.h>
 #include <libsolutil/Algorithms.h>
-#include <boost/range/algorithm/sort.hpp>
+
+#include <range/v3/algorithm/sort.hpp>
 
 #include <functional>
 
@@ -141,7 +142,7 @@ void ControlFlowAnalyzer::checkUninitializedAccess(CFGNode const* _entry, CFGNod
 			exitInfo.uninitializedVariableAccesses.begin(),
 			exitInfo.uninitializedVariableAccesses.end()
 		);
-		boost::range::sort(
+		ranges::sort(
 			uninitializedAccessesOrdered,
 			[](VariableOccurrence const* lhs, VariableOccurrence const* rhs) -> bool
 			{

libsolidity/analysis/TypeChecker.cpp

@@ -38,7 +38,6 @@
 
 #include <boost/algorithm/string/join.hpp>
 #include <boost/algorithm/string/predicate.hpp>
-#include <boost/range/adaptor/reversed.hpp>
 
 #include <range/v3/view/zip.hpp>
 #include <range/v3/view/drop_exactly.hpp>

libsolidity/ast/ASTJsonConverter.cpp

@@ -34,7 +34,8 @@
 #include <libsolutil/UTF8.h>
 
 #include <boost/algorithm/string/join.hpp>
-#include <boost/range/algorithm/sort.hpp>
+
+#include <range/v3/algorithm/sort.hpp>
 
 #include <utility>
 #include <vector>
@@ -563,8 +564,9 @@ bool ASTJsonConverter::visit(InlineAssembly const& _node)
 
 	Json::Value externalReferencesJson = Json::arrayValue;
 
-	for (auto&& it: boost::range::sort(externalReferences))
+	ranges::sort(externalReferences);
-		externalReferencesJson.append(std::move(it.second));
+	for (Json::Value& it: externalReferences | ranges::views::values)
+		externalReferencesJson.append(std::move(it));
 
 	setJsonNode(_node, "InlineAssembly", {
 		make_pair("AST", Json::Value(yul::AsmJsonConverter(sourceIndexFromLocation(_node.location()))(_node.operations()))),

libsolidity/formal/BMC.cpp

@@ -37,15 +37,14 @@ using namespace solidity::frontend;
 
 BMC::BMC(
 	smt::EncodingContext& _context,
-	ErrorReporter& _errorReporter,
+	UniqueErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
 	ModelCheckerSettings const& _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _charStreamProvider),
+	SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
-	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout)),
+	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout))
-	m_outerErrorReporter(_errorReporter)
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
 	if (m_settings.solvers.cvc4 || m_settings.solvers.z3)
@@ -67,7 +66,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		if (!m_noSolverWarning)
 		{
 			m_noSolverWarning = true;
-			m_outerErrorReporter.warning(
+			m_errorReporter.warning(
 				7710_error,
 				SourceLocation(),
 				"BMC analysis was not possible since no SMT solver was found and enabled."
@@ -76,30 +75,30 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		return;
 	}
 
-	if (SMTEncoder::analyze(_source))
+	SMTEncoder::resetSourceAnalysis();
-	{
-		m_solvedTargets = move(_solvedTargets);
-		m_context.setSolver(m_interface.get());
-		m_context.reset();
-		m_context.setAssertionAccumulation(true);
-		m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
-		createFreeConstants(sourceDependencies(_source));
-		m_unprovedAmt = 0;
 
-		_source.accept(*this);
+	m_solvedTargets = move(_solvedTargets);
+	m_context.setSolver(m_interface.get());
+	m_context.reset();
+	m_context.setAssertionAccumulation(true);
+	m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
+	createFreeConstants(sourceDependencies(_source));
+	state().prepareForSourceUnit(_source);
+	m_unprovedAmt = 0;
 
-		if (m_unprovedAmt > 0 && !m_settings.showUnproved)
+	_source.accept(*this);
-			m_errorReporter.warning(
+
-				2788_error,
+	if (m_unprovedAmt > 0 && !m_settings.showUnproved)
-				{},
+		m_errorReporter.warning(
-				"BMC: " +
+			2788_error,
-				to_string(m_unprovedAmt) +
+			{},
-				" verification condition(s) could not be proved." +
+			"BMC: " +
-				" Enable the model checker option \"show unproved\" to see all of them." +
+			to_string(m_unprovedAmt) +
-				" Consider choosing a specific contract to be verified in order to reduce the solving problems." +
+			" verification condition(s) could not be proved." +
-				" Consider increasing the timeout per query."
+			" Enable the model checker option \"show unproved\" to see all of them." +
-			);
+			" Consider choosing a specific contract to be verified in order to reduce the solving problems." +
-	}
+			" Consider increasing the timeout per query."
+		);
 
 	// If this check is true, Z3 and CVC4 are not available
 	// and the query answers were not provided, since SMTPortfolio
@@ -113,7 +112,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		if (!m_noSolverWarning)
 		{
 			m_noSolverWarning = true;
-			m_outerErrorReporter.warning(
+			m_errorReporter.warning(
 				8084_error,
 				SourceLocation(),
 				"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available."
@@ -124,10 +123,6 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 			);
 		}
 	}
-	else
-		m_outerErrorReporter.append(m_errorReporter.errors());
-
-	m_errorReporter.clear();
 }
 
 bool BMC::shouldInlineFunctionCall(

libsolidity/formal/BMC.h

@@ -36,7 +36,7 @@
 #include <libsolidity/interface/ReadFile.h>
 
 #include <libsmtutil/SolverInterface.h>
-#include <liblangutil/ErrorReporter.h>
+#include <liblangutil/UniqueErrorReporter.h>
 
 #include <set>
 #include <string>
@@ -59,7 +59,7 @@ class BMC: public SMTEncoder
 public:
 	BMC(
 		smt::EncodingContext& _context,
-		langutil::ErrorReporter& _errorReporter,
+		langutil::UniqueErrorReporter& _errorReporter,
 		std::map<h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		ModelCheckerSettings const& _settings,
@@ -186,9 +186,6 @@ private:
 	bool m_loopExecutionHappened = false;
 	bool m_externalFunctionCallHappened = false;
 
-	/// ErrorReporter that comes from CompilerStack.
-	langutil::ErrorReporter& m_outerErrorReporter;
-
 	std::vector<BMCVerificationTarget> m_verificationTargets;
 
 	/// Targets that were already proven.

libsolidity/formal/CHC.cpp

@@ -53,14 +53,13 @@ using namespace solidity::frontend::smt;
 
 CHC::CHC(
 	EncodingContext& _context,
-	ErrorReporter& _errorReporter,
+	UniqueErrorReporter& _errorReporter,
 	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
 	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
 	ModelCheckerSettings const& _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _charStreamProvider),
+	SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider)
-	m_outerErrorReporter(_errorReporter)
 {
 	bool usesZ3 = m_settings.solvers.z3;
 #ifdef HAVE_Z3
@@ -79,7 +78,7 @@ void CHC::analyze(SourceUnit const& _source)
 		if (!m_noSolverWarning)
 		{
 			m_noSolverWarning = true;
-			m_outerErrorReporter.warning(
+			m_errorReporter.warning(
 				7649_error,
 				SourceLocation(),
 				"CHC analysis was not possible since no Horn solver was enabled."
@@ -88,20 +87,19 @@ void CHC::analyze(SourceUnit const& _source)
 		return;
 	}
 
-	if (SMTEncoder::analyze(_source))
+	resetSourceAnalysis();
-	{
-		resetSourceAnalysis();
 
-		auto sources = sourceDependencies(_source);
+	auto sources = sourceDependencies(_source);
-		collectFreeFunctions(sources);
+	collectFreeFunctions(sources);
-		createFreeConstants(sources);
+	createFreeConstants(sources);
-		for (auto const* source: sources)
+	state().prepareForSourceUnit(_source);
-			defineInterfacesAndSummaries(*source);
-		for (auto const* source: sources)
-			source->accept(*this);
 
-		checkVerificationTargets();
+	for (auto const* source: sources)
-	}
+		defineInterfacesAndSummaries(*source);
+	for (auto const* source: sources)
+		source->accept(*this);
+
+	checkVerificationTargets();
 
 	bool ranSolver = true;
 	// If ranSolver is true here it's because an SMT solver callback was
@@ -111,7 +109,7 @@ void CHC::analyze(SourceUnit const& _source)
 	if (!ranSolver && !m_noSolverWarning)
 	{
 		m_noSolverWarning = true;
-		m_outerErrorReporter.warning(
+		m_errorReporter.warning(
 			3996_error,
 			SourceLocation(),
 #ifdef HAVE_Z3_DLOPEN
@@ -122,10 +120,6 @@ void CHC::analyze(SourceUnit const& _source)
 #endif
 		);
 	}
-	else
-		m_outerErrorReporter.append(m_errorReporter.errors());
-
-	m_errorReporter.clear();
 }
 
 vector<string> CHC::unhandledQueries() const
@@ -169,7 +163,13 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	smtutil::Expression zeroes(true);
 	for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
 		zeroes = zeroes && currentValue(*var) == smt::zeroValue(var->type());
-	addRule(smtutil::Expression::implies(initialConstraints(_contract) && zeroes, predicate(entry)), entry.functor().name);
+	// The contract's address might already have funds before deployment,
+	// so the balance must be at least `msg.value`, but not equals.
+	auto initialBalanceConstraint = state().balance(state().thisAddress()) >= state().txMember("msg.value");
+	addRule(smtutil::Expression::implies(
+		initialConstraints(_contract) && zeroes && initialBalanceConstraint,
+		predicate(entry)
+	), entry.functor().name);
 	setCurrentBlock(entry);
 
 	solAssert(!m_errorDest, "");
@@ -315,11 +315,16 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		shouldAnalyze(*m_currentContract)
 	)
 	{
-		auto sum = summary(_function);
+		defineExternalFunctionInterface(_function, *m_currentContract);
+		setCurrentBlock(*m_interfaces.at(m_currentContract));
+
+		// Create the rule
+		// interface \land externalFunctionEntry => interface'
 		auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
-		auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(_function);
+		auto sum = externalSummary(_function);
-		m_queryPlaceholders[&_function].push_back({txConstraints && sum, errorFlag().currentValue(), ifacePre});
+
-		connectBlocks(ifacePre, interface(), txConstraints && sum && errorFlag().currentValue() == 0);
+		m_queryPlaceholders[&_function].push_back({sum, errorFlag().currentValue(), ifacePre});
+		connectBlocks(ifacePre, interface(), sum && errorFlag().currentValue() == 0);
 	}
 
 	m_currentFunction = nullptr;
@@ -941,6 +946,8 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 
 void CHC::resetSourceAnalysis()
 {
+	SMTEncoder::resetSourceAnalysis();
+
 	m_safeTargets.clear();
 	m_unsafeTargets.clear();
 	m_unprovedTargets.clear();
@@ -949,6 +956,7 @@ void CHC::resetSourceAnalysis()
 	m_queryPlaceholders.clear();
 	m_callGraph.clear();
 	m_summaries.clear();
+	m_externalSummaries.clear();
 	m_interfaces.clear();
 	m_nondetInterfaces.clear();
 	m_constructorSummaries.clear();
@@ -1128,6 +1136,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 
 				if (!function->isConstructor() && function->isPublic() && resolved.count(function))
 				{
+					m_externalSummaries[contract].emplace(function, createSummaryBlock(*function, *contract));
+
 					auto state1 = stateVariablesAtIndex(1, *contract);
 					auto state2 = stateVariablesAtIndex(2, *contract);
 
@@ -1144,12 +1154,41 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 						applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
 						applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
 
-					connectBlocks(nondetPre, nondetPost, errorPre == 0 && (*m_summaries.at(contract).at(function))(args));
+					connectBlocks(nondetPre, nondetPost, errorPre == 0 && (*m_externalSummaries.at(contract).at(function))(args));
 				}
 			}
 		}
 }
 
+void CHC::defineExternalFunctionInterface(FunctionDefinition const& _function, ContractDefinition const& _contract)
+{
+	// Create a rule that represents an external call to this function.
+	// This contains more things than the function body itself,
+	// such as balance updates because of ``msg.value``.
+	auto functionEntryBlock = createBlock(&_function, PredicateType::FunctionBlock);
+	auto functionPred = predicate(*functionEntryBlock);
+	addRule(functionPred, functionPred.name);
+	setCurrentBlock(*functionEntryBlock);
+
+	m_context.addAssertion(initialConstraints(_contract, &_function));
+	m_context.addAssertion(state().txTypeConstraints() && state().txFunctionConstraints(_function));
+
+	// The contract may have received funds through a selfdestruct or
+	// block.coinbase, which do not trigger calls into the contract.
+	// So the only constraint we can add here is that the balance of
+	// the contract grows by at least `msg.value`.
+	SymbolicIntVariable k{TypeProvider::uint256(), TypeProvider::uint256(), "funds_" + to_string(m_context.newUniqueId()), m_context};
+	m_context.addAssertion(k.currentValue() >= state().txMember("msg.value"));
+	// Assume that address(this).balance cannot overflow.
+	m_context.addAssertion(smt::symbolicUnknownConstraints(state().balance(state().thisAddress()) + k.currentValue(), TypeProvider::uint256()));
+	state().addBalance(state().thisAddress(), k.currentValue());
+
+	errorFlag().increaseIndex();
+	m_context.addAssertion(summaryCall(_function));
+
+	connectBlocks(functionPred, externalSummary(_function));
+}
+
 void CHC::defineContractInitializer(ContractDefinition const& _contract, ContractDefinition const& _contextContract)
 {
 	m_contractInitializers[&_contextContract][&_contract] = createConstructorBlock(_contract, "contract_initializer");
@@ -1220,12 +1259,34 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDe
 	return smt::function(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
 }
 
+smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract)
+{
+	return smt::functionCall(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
+}
+
+smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract)
+{
+	return smt::function(*m_externalSummaries.at(&_contract).at(&_function), &_contract, m_context);
+}
+
 smtutil::Expression CHC::summary(FunctionDefinition const& _function)
 {
 	solAssert(m_currentContract, "");
 	return summary(_function, *m_currentContract);
 }
 
+smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function)
+{
+	solAssert(m_currentContract, "");
+	return summaryCall(_function, *m_currentContract);
+}
+
+smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function)
+{
+	solAssert(m_currentContract, "");
+	return externalSummary(_function, *m_currentContract);
+}
+
 Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, string const& _prefix)
 {
 	auto block = createSymbolicBlock(

libsolidity/formal/CHC.h

@@ -40,6 +40,7 @@
 #include <libsmtutil/CHCSolverInterface.h>
 
 #include <liblangutil/SourceLocation.h>
+#include <liblangutil/UniqueErrorReporter.h>
 
 #include <boost/algorithm/string/join.hpp>
 
@@ -55,7 +56,7 @@ class CHC: public SMTEncoder
 public:
 	CHC(
 		smt::EncodingContext& _context,
-		langutil::ErrorReporter& _errorReporter,
+		langutil::UniqueErrorReporter& _errorReporter,
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		ModelCheckerSettings const& _settings,
@@ -164,6 +165,12 @@ private:
 	/// in a given _source.
 	void defineInterfacesAndSummaries(SourceUnit const& _source);
 
+	/// Creates the rule
+	/// summary_function \land transaction_entry_constraints => external_summary_function
+	/// This is needed to add these transaction entry constraints which include
+	/// potential balance increase by external means, for example.
+	void defineExternalFunctionInterface(FunctionDefinition const& _function, ContractDefinition const& _contract);
+
 	/// Creates a CHC system that, for a given contract,
 	/// - initializes its state variables (as 0 or given value, if any).
 	/// - "calls" the explicit constructor function of the contract, if any.
@@ -225,6 +232,13 @@ private:
 	/// @returns a predicate that defines a function summary.
 	smtutil::Expression summary(FunctionDefinition const& _function);
 	smtutil::Expression summary(FunctionDefinition const& _function, ContractDefinition const& _contract);
+	/// @returns a predicate that applies a function summary
+	/// over the constrained variables.
+	smtutil::Expression summaryCall(FunctionDefinition const& _function);
+	smtutil::Expression summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract);
+	/// @returns a predicate that defines an external function summary.
+	smtutil::Expression externalSummary(FunctionDefinition const& _function);
+	smtutil::Expression externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract);
 	//@}
 
 	/// Solver related.
@@ -317,6 +331,9 @@ private:
 
 	/// Function predicates.
 	std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_summaries;
+
+	/// External function predicates.
+	std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_externalSummaries;
 	//@}
 
 	/// Variables.
@@ -399,9 +416,6 @@ private:
 
 	/// CHC solver.
 	std::unique_ptr<smtutil::CHCSolverInterface> m_interface;
-
-	/// ErrorReporter that comes from CompilerStack.
-	langutil::ErrorReporter& m_outerErrorReporter;
 };
 
 }

libsolidity/formal/ModelChecker.cpp

@@ -40,8 +40,8 @@ ModelChecker::ModelChecker(
 	m_errorReporter(_errorReporter),
 	m_settings(move(_settings)),
 	m_context(),
-	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
+	m_bmc(m_context, m_uniqueErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
-	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
+	m_chc(m_context, m_uniqueErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
 {
 }
 
@@ -68,7 +68,7 @@ void ModelChecker::checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUni
 	{
 		if (!exist.count(sourceName))
 		{
-			m_errorReporter.warning(
+			m_uniqueErrorReporter.warning(
 				9134_error,
 				SourceLocation(),
 				"Requested source \"" + sourceName + "\" does not exist."
@@ -79,7 +79,7 @@ void ModelChecker::checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUni
 		// Requested contracts in source `s`.
 		for (auto const& contract: m_settings.contracts.contracts.at(sourceName))
 			if (!source.count(contract))
-				m_errorReporter.warning(
+				m_uniqueErrorReporter.warning(
 					7400_error,
 					SourceLocation(),
 					"Requested contract \"" + contract + "\" does not exist in source \"" + sourceName + "\"."
@@ -104,7 +104,7 @@ void ModelChecker::analyze(SourceUnit const& _source)
 					break;
 				}
 		solAssert(smtPragma, "");
-		m_errorReporter.warning(
+		m_uniqueErrorReporter.warning(
 			5523_error,
 			smtPragma->location(),
 			"The SMTChecker pragma has been deprecated and will be removed in the future. "
@@ -125,6 +125,9 @@ void ModelChecker::analyze(SourceUnit const& _source)
 
 	if (m_settings.engine.bmc)
 		m_bmc.analyze(_source, solvedTargets);
+
+	m_errorReporter.append(m_uniqueErrorReporter.errors());
+	m_uniqueErrorReporter.clear();
 }
 
 vector<string> ModelChecker::unhandledQueries()

libsolidity/formal/ModelChecker.h

@@ -31,7 +31,9 @@
 #include <libsolidity/interface/ReadFile.h>
 
 #include <libsmtutil/SolverInterface.h>
+
 #include <liblangutil/ErrorReporter.h>
+#include <liblangutil/UniqueErrorReporter.h>
 
 namespace solidity::langutil
 {
@@ -73,8 +75,16 @@ public:
 	static smtutil::SMTSolverChoice availableSolvers();
 
 private:
+	/// Error reporter from CompilerStack.
+	/// We need to append m_uniqueErrorReporter
+	/// to this one when the analysis is done.
 	langutil::ErrorReporter& m_errorReporter;
 
+	/// Used by ModelChecker, SMTEncoder, BMC and CHC to avoid duplicates.
+	/// This is local to ModelChecker, so needs to be appended
+	/// to m_errorReporter at the end of the analysis.
+	langutil::UniqueErrorReporter m_uniqueErrorReporter;
+
 	ModelCheckerSettings m_settings;
 
 	/// Stores the context of the encoding.

libsolidity/formal/SMTEncoder.cpp

@@ -34,8 +34,6 @@
 
 #include <range/v3/view.hpp>
 
-#include <boost/range/adaptors.hpp>
-
 
 #include <deque>
 
@@ -48,20 +46,19 @@ using namespace solidity::frontend;
 SMTEncoder::SMTEncoder(
 	smt::EncodingContext& _context,
 	ModelCheckerSettings const& _settings,
+	UniqueErrorReporter& _errorReporter,
 	langutil::CharStreamProvider const& _charStreamProvider
 ):
-	m_errorReporter(m_smtErrors),
+	m_errorReporter(_errorReporter),
 	m_context(_context),
 	m_settings(_settings),
 	m_charStreamProvider(_charStreamProvider)
 {
 }
 
-bool SMTEncoder::analyze(SourceUnit const& _source)
+void SMTEncoder::resetSourceAnalysis()
 {
-	state().prepareForSourceUnit(_source);
+	m_freeFunctions.clear();
-
-	return true;
 }
 
 bool SMTEncoder::visit(ContractDefinition const& _contract)
@@ -1980,26 +1977,32 @@ void SMTEncoder::assignment(
 		indexOrMemberAssignment(*left, _right);
 	else if (auto const* funCall = dynamic_cast<FunctionCall const*>(left))
 	{
-		if (
+		if (auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type))
-			auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type);
-			funType && funType->kind() == FunctionType::Kind::ArrayPush
-		)
 		{
-			auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
+			if (funType->kind() == FunctionType::Kind::ArrayPush)
-			solAssert(memberAccess, "");
+			{
-			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
+				auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
-			solAssert(symbArray, "");
+				solAssert(memberAccess, "");
+				auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
+				solAssert(symbArray, "");
 
-			auto oldLength = symbArray->length();
+				auto oldLength = symbArray->length();
-			auto store = smtutil::Expression::store(
+				auto store = smtutil::Expression::store(
-				symbArray->elements(),
+					symbArray->elements(),
-				symbArray->length() - 1,
+					symbArray->length() - 1,
-				_right
+					_right
-			);
+				);
-			symbArray->increaseIndex();
+				symbArray->increaseIndex();
-			m_context.addAssertion(symbArray->elements() == store);
+				m_context.addAssertion(symbArray->elements() == store);
-			m_context.addAssertion(symbArray->length() == oldLength);
+				m_context.addAssertion(symbArray->length() == oldLength);
-			assignment(memberAccess->expression(), symbArray->currentValue());
+				assignment(memberAccess->expression(), symbArray->currentValue());
+			}
+			else if (funType->kind() == FunctionType::Kind::Internal)
+			{
+				for (auto type: funType->returnParameterTypes())
+					if (type->category() == Type::Category::Mapping || dynamic_cast<ReferenceType const*>(type))
+						resetReferences(type);
+			}
 		}
 	}
 	else
@@ -2283,9 +2286,7 @@ void SMTEncoder::resetStorageVariables()
 
 void SMTEncoder::resetBalances()
 {
-	// TODO this should be changed to `balances` only
+	state().newBalances();
-	// when `state` gets more members.
-	state().newState();
 }
 
 void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)

libsolidity/formal/SMTEncoder.h

@@ -32,7 +32,7 @@
 #include <libsolidity/ast/AST.h>
 #include <libsolidity/ast/ASTVisitor.h>
 #include <libsolidity/interface/ReadFile.h>
-#include <liblangutil/ErrorReporter.h>
+#include <liblangutil/UniqueErrorReporter.h>
 
 #include <string>
 #include <unordered_map>
@@ -55,12 +55,10 @@ public:
 	SMTEncoder(
 		smt::EncodingContext& _context,
 		ModelCheckerSettings const& _settings,
+		langutil::UniqueErrorReporter& _errorReporter,
 		langutil::CharStreamProvider const& _charStreamProvider
 	);
 
-	/// @returns true if engine should proceed with analysis.
-	bool analyze(SourceUnit const& _sources);
-
 	/// @returns the leftmost identifier in a multi-d IndexAccess.
 	static Expression const* leftmostBase(IndexAccess const& _indexAccess);
 
@@ -122,6 +120,8 @@ public:
 	static std::set<SourceUnit const*, ASTNode::CompareByID> sourceDependencies(SourceUnit const& _source);
 
 protected:
+	void resetSourceAnalysis();
+
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined
 	// TODO: or just force a certain order, but people might have a different idea about that.
@@ -420,11 +420,7 @@ protected:
 	/// or unchecked arithmetic.
 	bool m_checked = true;
 
-	/// Local SMTEncoder ErrorReporter.
+	langutil::UniqueErrorReporter& m_errorReporter;
-	/// This is necessary to show the "No SMT solver available"
-	/// warning before the others in case it's needed.
-	langutil::ErrorReporter m_errorReporter;
-	langutil::ErrorList m_smtErrors;
 
 	/// Stores the current function/modifier call/invocation path.
 	std::vector<CallStackEntry> m_callStack;

libsolidity/formal/SymbolicState.cpp

@@ -78,10 +78,8 @@ void SymbolicState::reset()
 	m_state.reset();
 	m_tx.reset();
 	m_crypto.reset();
-	/// We don't reset m_abi's pointer nor clear m_abiMembers on purpose,
+	if (m_abi)
-	/// since it only helps to keep the already generated types.
+		m_abi->reset();
-	solAssert(m_abi, "");
-	m_abi->reset();
 }
 
 smtutil::Expression SymbolicState::balances() const
@@ -104,6 +102,14 @@ smtutil::Expression SymbolicState::blockhash(smtutil::Expression _blockNumber) c
 	return smtutil::Expression::select(m_tx.member("blockhash"), move(_blockNumber));
 }
 
+void SymbolicState::newBalances()
+{
+	auto tupleSort = dynamic_pointer_cast<TupleSort>(stateSort());
+	auto balanceSort = tupleSort->components.at(tupleSort->memberToIndex.at("balances"));
+	SymbolicVariable newBalances(balanceSort, "fresh_balances_" + to_string(m_context.newUniqueId()), m_context);
+	m_state.assignMember("balances", newBalances.currentValue());
+}
+
 void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
 {
 	unsigned indexBefore = m_state.index();
@@ -121,6 +127,16 @@ void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to,
 	m_context.addAssertion(m_state.value() == newState);
 }
 
+void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
+{
+	auto newBalances = smtutil::Expression::store(
+		balances(),
+		_address,
+		balance(_address) + move(_value)
+	);
+	m_state.assignMember("balances", newBalances);
+}
+
 smtutil::Expression SymbolicState::txMember(string const& _member) const
 {
 	return m_tx.member(_member);
@@ -181,16 +197,6 @@ void SymbolicState::prepareForSourceUnit(SourceUnit const& _source)
 
 /// Private helpers.
 
-void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
-{
-	auto newBalances = smtutil::Expression::store(
-		balances(),
-		_address,
-		balance(_address) + move(_value)
-	);
-	m_state.assignMember("balances", newBalances);
-}
-
 void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFunctions)
 {
 	map<string, SortPointer> functions;

libsolidity/formal/SymbolicState.h

@@ -108,6 +108,8 @@ public:
 	smtutil::Expression state(unsigned _idx) const { return m_state.value(_idx); }
 	smtutil::SortPointer const& stateSort() const { return m_state.sort(); }
 	void newState() { m_state.newVar(); }
+
+	void newBalances();
 	/// @returns the symbolic balances.
 	smtutil::Expression balances() const;
 	/// @returns the symbolic balance of address `this`.
@@ -117,6 +119,9 @@ public:
 
 	/// Transfer _value from _from to _to.
 	void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
+
+	/// Adds _value to _account's balance.
+	void addBalance(smtutil::Expression _account, smtutil::Expression _value);
 	//@}
 
 	/// Transaction data.
@@ -163,9 +168,6 @@ public:
 	//@}
 
 private:
-	/// Adds _value to _account's balance.
-	void addBalance(smtutil::Expression _account, smtutil::Expression _value);
-
 	/// Builds m_abi based on the abi.* calls _abiFunctions.
 	void buildABIFunctions(std::set<FunctionCall const*> const& _abiFunctions);
 

libsolidity/formal/SymbolicTypes.cpp

@@ -551,6 +551,11 @@ smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, fronte
 	solAssert(_type, "");
 	if (isEnum(*_type) || isInteger(*_type) || isAddress(*_type) || isFixedBytes(*_type))
 		return _expr >= minValue(_type) && _expr <= maxValue(_type);
+	else if (
+		auto arrayType = dynamic_cast<ArrayType const*>(_type);
+		arrayType && !arrayType->isDynamicallySized()
+	)
+		return smtutil::Expression::tuple_get(_expr, 1) == arrayType->length();
 	else if (isArray(*_type) || isMapping(*_type))
 		/// Length cannot be negative.
 		return smtutil::Expression::tuple_get(_expr, 1) >= 0;

libsolidity/interface/FileReader.cpp

@@ -22,6 +22,8 @@
 #include <libsolutil/CommonIO.h>
 #include <libsolutil/Exceptions.h>
 
+#include <boost/algorithm/string/predicate.hpp>
+
 using solidity::frontend::ReadCallback;
 using solidity::langutil::InternalCompilerError;
 using solidity::util::errinfo_comment;
@@ -31,9 +33,22 @@ using std::string;
 namespace solidity::frontend
 {
 
+void FileReader::setBasePath(boost::filesystem::path const& _path)
+{
+	m_basePath = (_path.empty() ? "" : normalizeCLIPathForVFS(_path));
+}
+
 void FileReader::setSource(boost::filesystem::path const& _path, SourceCode _source)
 {
-	m_sourceCodes[_path.generic_string()] = std::move(_source);
+	boost::filesystem::path normalizedPath = normalizeCLIPathForVFS(_path);
+	boost::filesystem::path prefix = (m_basePath.empty() ? normalizeCLIPathForVFS(".") : m_basePath);
+
+	m_sourceCodes[stripPrefixIfPresent(prefix, normalizedPath).generic_string()] = std::move(_source);
+}
+
+void FileReader::setStdin(SourceCode _source)
+{
+	m_sourceCodes["<stdin>"] = std::move(_source);
 }
 
 void FileReader::setSources(StringMap _sources)
@@ -92,5 +107,138 @@ ReadCallback::Result FileReader::readFile(string const& _kind, string const& _so
 	}
 }
 
+boost::filesystem::path FileReader::normalizeCLIPathForVFS(boost::filesystem::path const& _path)
+{
+	// Detailed normalization rules:
+	// - Makes the path either be absolute or have slash as root (note that on Windows paths with
+	//   slash as root are not considered absolute by Boost). If it is empty, it becomes
+	//   the current working directory.
+	// - Collapses redundant . and .. segments.
+	// - Removes leading .. segments from an absolute path (i.e. /../../ becomes just /).
+	// - Squashes sequences of multiple path separators into one.
+	// - Ensures that forward slashes are used as path separators on all platforms.
+	// - Removes the root name (e.g. drive letter on Windows) when it matches the root name in the
+	//   path to the current working directory.
+	//
+	// Also note that this function:
+	// - Does NOT resolve symlinks (except for symlinks in the path to the current working directory).
+	// - Does NOT check if the path refers to a file or a directory. If the path ends with a slash,
+	//   the slash is preserved even if it's a file.
+	//   - The only exception are paths where the file name is a dot (e.g. '.' or 'a/b/.'). These
+	//     always have a trailing slash after normalization.
+	// - Preserves case. Even if the filesystem is case-insensitive but case-preserving and the
+	//   case differs, the actual case from disk is NOT detected.
+
+	boost::filesystem::path canonicalWorkDir = boost::filesystem::weakly_canonical(boost::filesystem::current_path());
+
+	// NOTE: On UNIX systems the path returned from current_path() has symlinks resolved while on
+	// Windows it does not. To get consistent results we resolve them on all platforms.
+	boost::filesystem::path absolutePath = boost::filesystem::absolute(_path, canonicalWorkDir);
+
+	// NOTE: boost path preserves certain differences that are ignored by its operator ==.
+	// E.g. "a//b" vs "a/b" or "a/b/" vs "a/b/.". lexically_normal() does remove these differences.
+	boost::filesystem::path normalizedPath =  absolutePath.lexically_normal();
+	solAssert(normalizedPath.is_absolute() || normalizedPath.root_path() == "/", "");
+
+	// If the path is on the same drive as the working dir, for portability we prefer not to
+	// include the root name. Do this only for non-UNC paths - my experiments show that on Windows
+	// when the working dir is an UNC path, / does not not actually refer to the root of the UNC path.
+	boost::filesystem::path normalizedRootPath = normalizedPath.root_path();
+	if (!isUNCPath(normalizedPath))
+	{
+		boost::filesystem::path workingDirRootPath = canonicalWorkDir.root_path();
+		if (normalizedRootPath == workingDirRootPath)
+			normalizedRootPath = "/";
+	}
+
+	// lexically_normal() will not squash paths like "/../../" into "/". We have to do it manually.
+	boost::filesystem::path dotDotPrefix = absoluteDotDotPrefix(normalizedPath);
+
+	boost::filesystem::path normalizedPathNoDotDot = normalizedPath;
+	if (dotDotPrefix.empty())
+		normalizedPathNoDotDot = normalizedRootPath / normalizedPath.relative_path();
+	else
+		normalizedPathNoDotDot = normalizedRootPath / normalizedPath.lexically_relative(normalizedPath.root_path() / dotDotPrefix);
+	solAssert(!hasDotDotSegments(normalizedPathNoDotDot), "");
+
+	// NOTE: On Windows lexically_normal() converts all separators to forward slashes. Convert them back.
+	// Separators do not affect path comparison but remain in internal representation returned by native().
+	// This will also normalize the root name to start with // in UNC paths.
+	normalizedPathNoDotDot = normalizedPathNoDotDot.generic_string();
+
+	// For some reason boost considers "/." different than "/" even though for other directories
+	// the trailing dot is ignored.
+	if (normalizedPathNoDotDot == "/.")
+		return "/";
+
+	return normalizedPathNoDotDot;
 }
 
+bool FileReader::isPathPrefix(boost::filesystem::path const& _prefix, boost::filesystem::path const& _path)
+{
+	solAssert(!_prefix.empty() && !_path.empty(), "");
+	// NOTE: On Windows paths starting with a slash (rather than a drive letter) are considered relative by boost.
+	solAssert(_prefix.is_absolute() || isUNCPath(_prefix) || _prefix.root_path() == "/", "");
+	solAssert(_path.is_absolute() || isUNCPath(_path) || _path.root_path() == "/", "");
+	solAssert(_prefix == _prefix.lexically_normal() && _path == _path.lexically_normal(), "");
+	solAssert(!hasDotDotSegments(_prefix) && !hasDotDotSegments(_path), "");
+
+	boost::filesystem::path strippedPath = _path.lexically_relative(
+		// Before 1.72.0 lexically_relative() was not handling paths with empty, dot and dot dot segments
+		// correctly (see https://github.com/boostorg/filesystem/issues/76). The only case where this
+		// is possible after our normalization is a directory name ending in a slash (filename is a dot).
+		_prefix.filename_is_dot() ? _prefix.parent_path() : _prefix
+	);
+	return !strippedPath.empty() && *strippedPath.begin() != "..";
+}
+
+boost::filesystem::path FileReader::stripPrefixIfPresent(boost::filesystem::path const& _prefix, boost::filesystem::path const& _path)
+{
+	if (!isPathPrefix(_prefix, _path))
+		return _path;
+
+	boost::filesystem::path strippedPath = _path.lexically_relative(
+		_prefix.filename_is_dot() ? _prefix.parent_path() : _prefix
+	);
+	solAssert(strippedPath.empty() || *strippedPath.begin() != "..", "");
+	return strippedPath;
+}
+
+boost::filesystem::path FileReader::absoluteDotDotPrefix(boost::filesystem::path const& _path)
+{
+	solAssert(_path.is_absolute() || _path.root_path() == "/", "");
+
+	boost::filesystem::path _pathWithoutRoot = _path.relative_path();
+	boost::filesystem::path prefix;
+	for (boost::filesystem::path const& segment: _pathWithoutRoot)
+		if (segment.filename_is_dot_dot())
+			prefix /= segment;
+
+	return prefix;
+}
+
+bool FileReader::hasDotDotSegments(boost::filesystem::path const& _path)
+{
+	for (boost::filesystem::path const& segment: _path)
+		if (segment.filename_is_dot_dot())
+			return true;
+
+	return false;
+}
+
+bool FileReader::isUNCPath(boost::filesystem::path const& _path)
+{
+	string rootName = _path.root_name().string();
+
+	return (
+		rootName.size() == 2 ||
+		(rootName.size() > 2 && rootName[2] != rootName[1])
+	) && (
+		(rootName[0] == '/' && rootName[1] == '/')
+#if defined(_WIN32)
+		|| (rootName[0] == '\\' && rootName[1] == '\\')
+#endif
+	);
+}
+
+}

libsolidity/interface/FileReader.h

@@ -45,12 +45,13 @@ public:
 		boost::filesystem::path _basePath = {},
 		FileSystemPathSet _allowedDirectories = {}
 	):
-		m_basePath(std::move(_basePath)),
 		m_allowedDirectories(std::move(_allowedDirectories)),
 		m_sourceCodes()
-	{}
+	{
+		setBasePath(_basePath);
+	}
 
-	void setBasePath(boost::filesystem::path _path) { m_basePath = std::move(_path); }
+	void setBasePath(boost::filesystem::path const& _path);
 	boost::filesystem::path const& basePath() const noexcept { return m_basePath; }
 
 	void allowDirectory(boost::filesystem::path _path) { m_allowedDirectories.insert(std::move(_path)); }
@@ -58,17 +59,21 @@ public:
 
 	StringMap const& sourceCodes() const noexcept { return m_sourceCodes; }
 
-	/// Retrieves the source code for a given source unit ID.
+	/// Retrieves the source code for a given source unit name.
 	SourceCode const& sourceCode(SourceUnitName const& _sourceUnitName) const { return m_sourceCodes.at(_sourceUnitName); }
 
-	/// Resets all sources to the given map of source unit ID to source codes.
+	/// Resets all sources to the given map of source unit name to source codes.
 	/// Does not enforce @a allowedDirectories().
 	void setSources(StringMap _sources);
 
-	/// Adds the source code for a given source unit ID.
+	/// Adds the source code under a source unit name created by normalizing the file path.
 	/// Does not enforce @a allowedDirectories().
 	void setSource(boost::filesystem::path const& _path, SourceCode _source);
 
+	/// Adds the source code under the source unit name of @a <stdin>.
+	/// Does not enforce @a allowedDirectories().
+	void setStdin(SourceCode _source);
+
 	/// Receives a @p _sourceUnitName that refers to a source unit in compiler's virtual filesystem
 	/// and attempts to interpret it as a path and read the corresponding file from disk.
 	/// The read will only succeed if the canonical path of the file is within one of the @a allowedDirectories().
@@ -83,7 +88,43 @@ public:
 		return [this](std::string const& _kind, std::string const& _path) { return readFile(_kind, _path); };
 	}
 
+	/// Normalizes a filesystem path to make it include all components up to the filesystem root,
+	/// remove small, inconsequential differences that do not affect the meaning and make it look
+	/// the same on all platforms (if possible). Symlinks in the path are not resolved.
+	/// The resulting path uses forward slashes as path separators, has no redundant separators,
+	/// has no redundant . or .. segments and has no root name if removing it does not change the meaning.
+	/// The path does not have to actually exist.
+	static boost::filesystem::path normalizeCLIPathForVFS(boost::filesystem::path const& _path);
+
+	/// @returns true if all the path components of @a _prefix are present at the beginning of @a _path.
+	/// Both paths must be absolute (or have slash as root) and normalized (no . or .. segments, no
+	/// multiple consecutive slashes).
+	/// Paths are treated as case-sensitive. Does not require the path to actually exist in the
+	/// filesystem and does not follow symlinks. Only considers whole segments, e.g. /abc/d is not
+	/// considered a prefix of /abc/def. Both paths must be non-empty.
+	/// Ignores the trailing slash, i.e. /a/b/c.sol/ is treated as a valid prefix of /a/b/c.sol.
+	static bool isPathPrefix(boost::filesystem::path const& _prefix, boost::filesystem::path const& _path);
+
+	/// If @a _prefix is actually a prefix of @p _path, removes it from @a _path to make it relative.
+	/// @returns The path without the prefix or unchanged path if there is not prefix.
+	/// If @a _path and @_prefix are identical, the result is '.'.
+	static boost::filesystem::path stripPrefixIfPresent(boost::filesystem::path const& _prefix, boost::filesystem::path const& _path);
+
+	/// @returns true if the specified path is an UNC path.
+	/// UNC paths start with // followed by a name (on Windows they can also start with \\).
+	/// They are used for network shares on Windows. On UNIX systems they do not have the same
+	/// functionality but usually they are still recognized and treated in a special way.
+	static bool isUNCPath(boost::filesystem::path const& _path);
+
 private:
+	/// If @a _path starts with a number of .. segments, returns a path consisting only of those
+	/// segments (root name is not included). Otherwise returns an empty path. @a _path must be
+	/// absolute (or have slash as root).
+	static boost::filesystem::path absoluteDotDotPrefix(boost::filesystem::path const& _path);
+
+	/// @returns true if the path contains any .. segments.
+	static bool hasDotDotSegments(boost::filesystem::path const& _path);
+
 	/// Base path, used for resolving relative paths in imports.
 	boost::filesystem::path m_basePath;
 

libsolidity/parsing/DocStringParser.cpp

@@ -24,8 +24,9 @@
 #include <liblangutil/ErrorReporter.h>
 #include <liblangutil/Exceptions.h>
 
-#include <boost/range/algorithm/find_first_of.hpp>
+#include <range/v3/algorithm/find_first_of.hpp>
-#include <boost/range/irange.hpp>
+#include <range/v3/algorithm/find_if_not.hpp>
+#include <range/v3/view/subrange.hpp>
 
 using namespace std;
 using namespace solidity;
@@ -52,8 +53,7 @@ string::const_iterator firstNonIdentifier(
 	if (currPos == _pos && isIdentifierStart(*currPos))
 	{
 		currPos++;
-		while (currPos != _end && isIdentifierPart(*currPos))
+		currPos = ranges::find_if_not(ranges::make_subrange(currPos, _end), isIdentifierPart);
-			currPos++;
 	}
 	return currPos;
 }
@@ -63,7 +63,7 @@ string::const_iterator firstWhitespaceOrNewline(
 	string::const_iterator _end
 )
 {
-	return boost::range::find_first_of(make_pair(_pos, _end), " \t\n");
+	return ranges::find_first_of(ranges::make_subrange(_pos, _end), " \t\n");
 }
 
 
@@ -72,10 +72,8 @@ string::const_iterator skipWhitespace(
 	string::const_iterator _end
 )
 {
-	auto currPos = _pos;
+	auto isWhitespace = [](char const& c) { return (c == ' ' || c == '\t'); };
-	while (currPos != _end && (*currPos == ' ' || *currPos == '\t'))
+	return ranges::find_if_not(ranges::make_subrange(_pos, _end), isWhitespace);
-		currPos += 1;
-	return currPos;
 }
 
 }

solc/CommandLineInterface.cpp

@@ -451,7 +451,7 @@ bool CommandLineInterface::readInputFiles()
 			m_standardJsonInput = readUntilEnd(m_sin);
 		}
 		else
-			m_fileReader.setSource(g_stdinFileName, readUntilEnd(m_sin));
+			m_fileReader.setStdin(readUntilEnd(m_sin));
 	}
 
 	if (m_fileReader.sourceCodes().empty() && !m_standardJsonInput.has_value())

solc/CommandLineParser.cpp

@@ -927,6 +927,16 @@ General Information)").c_str(),
 	else
 		m_options.input.mode = InputMode::Compiler;
 
+	if (
+		m_args.count(g_strExperimentalViaIR) > 0 &&
+		m_options.input.mode != InputMode::Compiler &&
+		m_options.input.mode != InputMode::CompilerWithASTImport
+	)
+	{
+		serr() << "The option --" << g_strExperimentalViaIR << " is only supported in the compiler mode." << endl;
+		return false;
+	}
+
 	if (!parseInputPathsAndRemappings())
 		return false;
 

test/CMakeLists.txt

@@ -103,6 +103,7 @@ set(libsolidity_sources
     libsolidity/SyntaxTest.h
     libsolidity/ViewPureChecker.cpp
     libsolidity/analysis/FunctionCallGraph.cpp
+    libsolidity/interface/FileReader.cpp
 )
 detect_stray_source_files("${libsolidity_sources}" "libsolidity/")
 

test/FilesystemUtils.cpp

@@ -39,7 +39,7 @@ void solidity::test::createFilesWithParentDirs(set<boost::filesystem::path> cons
 	}
 }
 
-void solidity::test::createFileWithContent(boost::filesystem::path const& _path, string const& content)
+void solidity::test::createFileWithContent(boost::filesystem::path const& _path, string const& _content)
 {
 	if (boost::filesystem::is_regular_file(_path))
 		BOOST_THROW_EXCEPTION(runtime_error("File already exists: \"" + _path.string() + "\".")); \
@@ -49,16 +49,21 @@ void solidity::test::createFileWithContent(boost::filesystem::path const& _path,
 	if (newFile.fail() || !boost::filesystem::is_regular_file(_path))
 		BOOST_THROW_EXCEPTION(runtime_error("Failed to create a file: \"" + _path.string() + "\".")); \
 
-	newFile << content;
+	newFile << _content;
 }
 
 bool solidity::test::createSymlinkIfSupportedByFilesystem(
 	boost::filesystem::path const& _targetPath,
-	boost::filesystem::path const& _linkName
+	boost::filesystem::path const& _linkName,
+	bool _directorySymlink
 )
 {
 	boost::system::error_code symlinkCreationError;
-	boost::filesystem::create_symlink(_targetPath, _linkName, symlinkCreationError);
+
+	if (_directorySymlink)
+		boost::filesystem::create_directory_symlink(_targetPath, _linkName, symlinkCreationError);
+	else
+		boost::filesystem::create_symlink(_targetPath, _linkName, symlinkCreationError);
 
 	if (!symlinkCreationError)
 		return true;

test/FilesystemUtils.h

@@ -35,16 +35,20 @@ void createFilesWithParentDirs(std::set<boost::filesystem::path> const& _paths,
 
 /// Creates a file with the exact content specified in the second argument.
 /// Throws an exception if the file already exists or if the parent directory of the file does not.
-void createFileWithContent(boost::filesystem::path const& _path, std::string const& content);
+void createFileWithContent(boost::filesystem::path const& _path, std::string const& _content);
 
 /// Creates a symlink between two paths.
 /// The target does not have to exist.
+/// If @p directorySymlink is true, indicate to the operating system that this is a directory
+/// symlink. On some systems (e.g. Windows) it's possible to create a non-directory symlink pointing
+/// at a directory, which makes such a symlinks unusable.
 /// @returns true if the symlink has been successfully created, false if the filesystem does not
 /// support symlinks.
 /// Throws an exception of the operation fails for a different reason.
 bool createSymlinkIfSupportedByFilesystem(
 	boost::filesystem::path const& _targetPath,
-	boost::filesystem::path const& _linkName
+	boost::filesystem::path const& _linkName,
+	bool _directorySymlink
 );
 
 }

test/TemporaryDirectory.cpp

@@ -18,9 +18,11 @@
 
 #include <test/TemporaryDirectory.h>
 
+#include <test/libsolidity/util/SoltestErrors.h>
+
+#include <boost/algorithm/string/predicate.hpp>
 #include <boost/filesystem.hpp>
 
-#include <cassert>
 #include <regex>
 #include <iostream>
 
@@ -31,21 +33,39 @@ using namespace solidity::test;
 namespace fs = boost::filesystem;
 
 TemporaryDirectory::TemporaryDirectory(std::string const& _prefix):
-	m_path(fs::temp_directory_path() / fs::unique_path(_prefix + "%%%%-%%%%-%%%%-%%%%"))
+	m_path(fs::temp_directory_path() / fs::unique_path(_prefix + "-%%%%-%%%%-%%%%-%%%%"))
 {
 	// Prefix should just be a file name and not contain anything that would make us step out of /tmp.
-	assert(fs::path(_prefix) == fs::path(_prefix).stem());
+	soltestAssert(fs::path(_prefix) == fs::path(_prefix).stem(), "");
 
 	fs::create_directory(m_path);
 }
 
+TemporaryDirectory::TemporaryDirectory(
+	vector<boost::filesystem::path> const& _subdirectories,
+	string const& _prefix
+):
+	TemporaryDirectory(_prefix)
+{
+	for (boost::filesystem::path const& subdirectory: _subdirectories)
+	{
+		soltestAssert(!subdirectory.is_absolute() && subdirectory.root_path() != "/", "");
+		soltestAssert(
+			m_path.lexically_relative(subdirectory).empty() ||
+			*m_path.lexically_relative(subdirectory).begin() != "..",
+			""
+		);
+		boost::filesystem::create_directories(m_path / subdirectory);
+	}
+}
+
 TemporaryDirectory::~TemporaryDirectory()
 {
 	// A few paranoid sanity checks just to be extra sure we're not deleting someone's homework.
-	assert(m_path.string().find(fs::temp_directory_path().string()) == 0);
+	soltestAssert(m_path.string().find(fs::temp_directory_path().string()) == 0, "");
-	assert(!fs::equivalent(m_path, fs::temp_directory_path()));
+	soltestAssert(!fs::equivalent(m_path, fs::temp_directory_path()), "");
-	assert(!fs::equivalent(m_path, m_path.root_path()));
+	soltestAssert(!fs::equivalent(m_path, m_path.root_path()), "");
-	assert(!m_path.empty());
+	soltestAssert(!m_path.empty(), "");
 
 	boost::system::error_code errorCode;
 	uintmax_t numRemoved = fs::remove_all(m_path, errorCode);

test/TemporaryDirectory.h

@@ -25,6 +25,7 @@
 #include <boost/filesystem.hpp>
 
 #include <string>
+#include <vector>
 
 namespace solidity::test
 {
@@ -40,10 +41,15 @@ namespace solidity::test
 class TemporaryDirectory
 {
 public:
-	TemporaryDirectory(std::string const& _prefix = "solidity-test-");
+	TemporaryDirectory(std::string const& _prefix = "solidity-test");
+	TemporaryDirectory(
+		std::vector<boost::filesystem::path> const& _subdirectories,
+		std::string const& _prefix = "solidity-test"
+	);
 	~TemporaryDirectory();
 
 	boost::filesystem::path const& path() const { return m_path; }
+	operator boost::filesystem::path() const { return m_path; }
 
 private:
 	boost::filesystem::path m_path;
@@ -59,6 +65,7 @@ public:
 	~TemporaryWorkingDirectory();
 
 	boost::filesystem::path const& originalWorkingDirectory() const { return m_originalWorkingDirectory; }
+	operator boost::filesystem::path() const { return boost::filesystem::current_path(); }
 
 private:
 	boost::filesystem::path m_originalWorkingDirectory;

test/TemporaryDirectoryTest.cpp

@@ -18,6 +18,8 @@
 
 #include <test/TemporaryDirectory.h>
 
+#include <test/libsolidity/util/SoltestErrors.h>
+
 #include <boost/filesystem.hpp>
 #include <boost/test/unit_test.hpp>
 
@@ -26,8 +28,6 @@
 using namespace std;
 using namespace boost::test_tools;
 
-namespace fs = boost::filesystem;
-
 namespace solidity::test
 {
 
@@ -35,59 +35,72 @@ BOOST_AUTO_TEST_SUITE(TemporaryDirectoryTest)
 
 BOOST_AUTO_TEST_CASE(TemporaryDirectory_should_create_and_delete_a_unique_and_empty_directory)
 {
-	fs::path dirPath;
+	boost::filesystem::path dirPath;
 	{
-		TemporaryDirectory tempDir("temporary-directory-test-");
+		TemporaryDirectory tempDir("temporary-directory-test");
 		dirPath = tempDir.path();
 
-		BOOST_TEST(dirPath.stem().string().find("temporary-directory-test-") == 0);
+		BOOST_TEST(dirPath.stem().string().find("temporary-directory-test") == 0);
-		BOOST_TEST(fs::equivalent(dirPath.parent_path(), fs::temp_directory_path()));
+		BOOST_TEST(boost::filesystem::equivalent(dirPath.parent_path(), boost::filesystem::temp_directory_path()));
-		BOOST_TEST(fs::is_directory(dirPath));
+		BOOST_TEST(boost::filesystem::is_directory(dirPath));
-		BOOST_TEST(fs::is_empty(dirPath));
+		BOOST_TEST(boost::filesystem::is_empty(dirPath));
 	}
-	BOOST_TEST(!fs::exists(dirPath));
+	BOOST_TEST(!boost::filesystem::exists(dirPath));
 }
 
 BOOST_AUTO_TEST_CASE(TemporaryDirectory_should_delete_its_directory_even_if_not_empty)
 {
-	fs::path dirPath;
+	boost::filesystem::path dirPath;
 	{
-		TemporaryDirectory tempDir("temporary-directory-test-");
+		TemporaryDirectory tempDir("temporary-directory-test");
 		dirPath = tempDir.path();
 
-		BOOST_TEST(fs::is_directory(dirPath));
+		BOOST_TEST(boost::filesystem::is_directory(dirPath));
 
 		{
 			ofstream tmpFile((dirPath / "test-file.txt").string());
 			tmpFile << "Delete me!" << endl;
 		}
-		assert(fs::is_regular_file(dirPath / "test-file.txt"));
+		soltestAssert(boost::filesystem::is_regular_file(dirPath / "test-file.txt"), "");
+	}
+	BOOST_TEST(!boost::filesystem::exists(dirPath / "test-file.txt"));
+}
+
+BOOST_AUTO_TEST_CASE(TemporaryDirectory_should_create_subdirectories)
+{
+	boost::filesystem::path dirPath;
+	{
+		TemporaryDirectory tempDir({"a", "a/", "a/b/c", "x.y/z"}, "temporary-directory-test");
+		dirPath = tempDir.path();
+
+		BOOST_TEST(boost::filesystem::is_directory(dirPath / "a"));
+		BOOST_TEST(boost::filesystem::is_directory(dirPath / "a/b/c"));
+		BOOST_TEST(boost::filesystem::is_directory(dirPath / "x.y/z"));
 	}
-	BOOST_TEST(!fs::exists(dirPath / "test-file.txt"));
 }
 
 BOOST_AUTO_TEST_CASE(TemporaryWorkingDirectory_should_change_and_restore_working_directory)
 {
-	fs::path originalWorkingDirectory = fs::current_path();
+	boost::filesystem::path originalWorkingDirectory = boost::filesystem::current_path();
 
 	try
 	{
 		{
-			TemporaryDirectory tempDir("temporary-directory-test-");
+			TemporaryDirectory tempDir("temporary-directory-test");
-			assert(fs::equivalent(fs::current_path(), originalWorkingDirectory));
+			soltestAssert(boost::filesystem::equivalent(boost::filesystem::current_path(), originalWorkingDirectory), "");
-			assert(!fs::equivalent(tempDir.path(), originalWorkingDirectory));
+			soltestAssert(!boost::filesystem::equivalent(tempDir.path(), originalWorkingDirectory), "");
 
 			TemporaryWorkingDirectory tempWorkDir(tempDir.path());
 
-			BOOST_TEST(fs::equivalent(fs::current_path(), tempDir.path()));
+			BOOST_TEST(boost::filesystem::equivalent(boost::filesystem::current_path(), tempDir.path()));
 		}
-		BOOST_TEST(fs::equivalent(fs::current_path(), originalWorkingDirectory));
+		BOOST_TEST(boost::filesystem::equivalent(boost::filesystem::current_path(), originalWorkingDirectory));
 
-		fs::current_path(originalWorkingDirectory);
+		boost::filesystem::current_path(originalWorkingDirectory);
 	}
 	catch (...)
 	{
-		fs::current_path(originalWorkingDirectory);
+		boost::filesystem::current_path(originalWorkingDirectory);
 	}
 }
 

test/cmdlineTests/model_checker_solvers_smtlib2/err

@@ -1,3 +1,7 @@
+Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+
 Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
 
+Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+
 Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.

test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json

@@ -41,46 +41,6 @@ A.constructor()
 A.f(0)","severity":"warning","sourceLocation":{"end":231,"file":"Source","start":218},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
 Counterexample:
 
-y = 0
-
-Transaction trace:
-A.constructor()
-B.g(0)
- --> Source:5:7:
-  |
-5 | \t\t\t\t\t\tassert(y > 0);
-  | \t\t\t\t\t\t^^^^^^^^^^^^^
-
-","message":"CHC: Assertion violation happens here.
-Counterexample:
-
-y = 0
-
-Transaction trace:
-A.constructor()
-B.g(0)","severity":"warning","sourceLocation":{"end":137,"file":"Source","start":124},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
-Counterexample:
-
-x = 0
-
-Transaction trace:
-A.constructor()
-A.f(0)
-  --> Source:10:7:
-   |
-10 | \t\t\t\t\t\tassert(x > 0);
-   | \t\t\t\t\t\t^^^^^^^^^^^^^
-
-","message":"CHC: Assertion violation happens here.
-Counterexample:
-
-x = 0
-
-Transaction trace:
-A.constructor()
-A.f(0)","severity":"warning","sourceLocation":{"end":231,"file":"Source","start":218},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
-Counterexample:
-
 z = 0
 
 Transaction trace:

test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json

@@ -24,7 +24,7 @@
 (assert (= |EVALEXPR_0| x_3_0))
 (check-sat)
 (get-value (|EVALEXPR_0| ))
-","0xa51d18d2c7cb0481228dd7dd4e7debb5d54580595265d16f67b236faa98f4862":"(set-logic HORN)
+","0x4e70784a8a93c7429a716aa8b778f3de5d1f63b30158452534da5d44e5967d2b":"(set-logic HORN)
 
 (declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
 (declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
@@ -41,100 +41,116 @@
 
 
 (declare-fun |summary_3_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
+(declare-fun |summary_4_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
 (assert
 (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
-(=> (and (and (nondet_interface_1_C_14_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 x_3_0 state_2 x_3_1))) (nondet_interface_1_C_14_0 error_1 this_0 abi_0 crypto_0 state_0 state_2))))
+(=> (and (and (nondet_interface_1_C_14_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_4_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 x_3_0 state_2 x_3_1))) (nondet_interface_1_C_14_0 error_1 this_0 abi_0 crypto_0 state_0 state_2))))
 
 
-(declare-fun |block_4_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
+(declare-fun |block_5_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
-(declare-fun |block_5_f_12_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
+(declare-fun |block_6_f_12_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
 (assert
 (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
-(block_4_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))
+(block_5_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))
 
 
 (assert
 (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
-(=> (and (and (block_4_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true)) true) (block_5_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
+(=> (and (and (block_5_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true)) true) (block_6_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
 
 
-(declare-fun |block_6_return_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
+(declare-fun |block_7_return_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
-(declare-fun |block_7_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
+(declare-fun |block_8_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
 (assert
 (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
-(=> (and (and (block_5_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))))) (and (not expr_9_1) (= error_1 1))) (block_7_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
+(=> (and (and (block_6_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))))) (and (not expr_9_1) (= error_1 1))) (block_8_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
 
 
 (assert
 (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
-(=> (block_7_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
+(=> (block_8_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
 
 
 (assert
 (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
-(=> (and (and (block_5_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= error_1 error_0) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true)))))))) true) (block_6_return_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
+(=> (and (and (block_6_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= error_1 error_0) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true)))))))) true) (block_7_return_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
 
 
 (assert
 (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
-(=> (and (and (block_6_return_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) true) true) (summary_3_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
+(=> (and (and (block_7_return_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) true) true) (summary_3_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
+
+
+(declare-fun |block_9_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
+(assert
+(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
+(block_9_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)))
 
 
 (assert
-(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
+(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
-(=> (and (and (interface_0_C_14_0 this_0 abi_0 crypto_0 state_0) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (summary_3_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1))))
+(=> (and (and (block_9_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (summary_3_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 x_3_1 state_3 x_3_2) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= x_3_1 x_3_0))) true))))))) true) (summary_4_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_3 x_3_2))))
-
-
-(declare-fun |contract_initializer_8_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
-(declare-fun |contract_initializer_entry_9_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
-(assert
-(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
-(=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_9_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
-
-
-(declare-fun |contract_initializer_after_init_10_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
-(assert
-(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
-(=> (and (and (contract_initializer_entry_9_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_10_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
 
 
 (assert
-(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
+(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
-(=> (and (and (contract_initializer_after_init_10_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_8_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
+(=> (and (and (interface_0_C_14_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1))))
 
 
-(declare-fun |implicit_constructor_entry_11_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
+(declare-fun |contract_initializer_10_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
+(declare-fun |contract_initializer_entry_11_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
 (assert
-(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
+(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
-(=> (and (and (and (= state_1 state_0) (= error_0 0)) true) true) (implicit_constructor_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
+(=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
+
+
+(declare-fun |contract_initializer_after_init_12_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
+(assert
+(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
+(=> (and (and (contract_initializer_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_12_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
 
 
 (assert
-(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
+(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
-(=> (and (and (implicit_constructor_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_8_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2))))
+(=> (and (and (contract_initializer_after_init_12_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_10_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
+
+
+(declare-fun |implicit_constructor_entry_13_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
+(assert
+(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
+(=> (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
 
 
 (assert
-(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
+(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
-(=> (and (and (implicit_constructor_entry_11_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_8_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2))))
+(=> (and (and (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_10_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2))))
 
 
 (assert
-(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
+(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
+(=> (and (and (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_10_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2))))
+
+
+(assert
+(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
 (=> (and (and (summary_constructor_2_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_14_0 this_0 abi_0 crypto_0 state_1))))
 
 
-(declare-fun |error_target_2_0| () Bool)
+(declare-fun |error_target_3_0| () Bool)
 (assert
-(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
+(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
-(=> (and (and (interface_0_C_14_0 this_0 abi_0 crypto_0 state_0) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (summary_3_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1)) (= error_0 1))) error_target_2_0)))
+(=> (and (and (interface_0_C_14_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_f__13_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (= error_0 1))) error_target_3_0)))
 
 
 (assert
-(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
+(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
-(=> error_target_2_0 false)))
+(=> error_target_3_0 false)))
-(check-sat)"}},"errors":[{"component":"general","errorCode":"3996","formattedMessage":"Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
+(check-sat)"}},"errors":[{"component":"general","errorCode":"5840","formattedMessage":"Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
 
-","message":"CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"8084","formattedMessage":"Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.
+","message":"CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"3996","formattedMessage":"Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
+
+","message":"CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"2788","formattedMessage":"Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+
+","message":"BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"8084","formattedMessage":"Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.
 
 ","message":"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}

test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json

@@ -30,7 +30,7 @@
 
 (assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_14_1)))
 (check-sat)
-","0x7bc2dabee60a201f5515fdb8dd9d201cff4e984c3f7c74d87fbdb6e6070e6252":"(set-option :produce-models true)
+","0xa7b2de16abc4c0f0f9e2c540a576178d99cb73a01cf0d0d1d62d51735c6d3b44":"(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
 (declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
@@ -67,8 +67,8 @@
 (declare-fun |expr_26_1| () Int)
 (declare-fun |expr_28_0| () Int)
 (declare-fun |expr_29_0| () Int)
-(declare-fun |d_div_mod_10_0| () Int)
+(declare-fun |d_div_mod_11_0| () Int)
-(declare-fun |r_div_mod_10_0| () Int)
+(declare-fun |r_div_mod_11_0| () Int)
 (declare-fun |expr_30_1| () Int)
 (declare-fun |expr_32_0| () Int)
 (declare-fun |expr_35_0| () Int)
@@ -84,7 +84,7 @@
 (declare-fun |expr_50_0| () Int)
 (declare-fun |expr_51_1| () Int)
 
-(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (=> (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (=> (and true true) (and (>= expr_30_1 0) (<= expr_30_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_1 (ite (= expr_29_0 0) 0 d_div_mod_10_0)) (and (and (<= 0 r_div_mod_10_0) (or (= expr_29_0 0) (< r_div_mod_10_0 expr_29_0))) (and (= (+ (* d_div_mod_10_0 expr_29_0) r_div_mod_10_0) expr_28_0) (and (=> (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (=> (and true true) true) (and (= expr_28_0 2) (and (=> (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (=> (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (=> (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (=> (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_35_0)))
+(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (=> (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (=> (and true true) (and (>= expr_30_1 0) (<= expr_30_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_1 (ite (= expr_29_0 0) 0 d_div_mod_11_0)) (and (and (<= 0 r_div_mod_11_0) (or (= expr_29_0 0) (< r_div_mod_11_0 expr_29_0))) (and (= (+ (* d_div_mod_11_0 expr_29_0) r_div_mod_11_0) expr_28_0) (and (=> (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (=> (and true true) true) (and (= expr_28_0 2) (and (=> (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (=> (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (=> (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (=> (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_35_0)))
 (declare-const |EVALEXPR_0| Int)
 (assert (= |EVALEXPR_0| a_6_0))
 (declare-const |EVALEXPR_1| Int)

test/libsolidity/interface/FileReader.cpp

@@ -0,0 +1,447 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+/// Unit tests for libsolidity/interface/FileReader.h
+
+#include <libsolidity/interface/FileReader.h>
+
+#include <test/Common.h>
+#include <test/FilesystemUtils.h>
+#include <test/TemporaryDirectory.h>
+#include <test/libsolidity/util/SoltestErrors.h>
+
+#include <boost/filesystem.hpp>
+#include <boost/test/unit_test.hpp>
+
+using namespace std;
+using namespace solidity::test;
+
+#define TEST_CASE_NAME (boost::unit_test::framework::current_test_case().p_name)
+
+namespace solidity::frontend::test
+{
+
+BOOST_AUTO_TEST_SUITE(FileReaderTest)
+
+BOOST_AUTO_TEST_CASE(normalizeCLIPathForVFS_absolute_path)
+{
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/"), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/./"), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/./."), "/");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a"), "/a");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/"), "/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/."), "/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/./a"), "/a");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/./a/"), "/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/./a/."), "/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/b"), "/a/b");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/b/"), "/a/b/");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/./b/"), "/a/b/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/../a/b/"), "/a/b/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/b/c/.."), "/a/b");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/b/c/../"), "/a/b/");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/b/c/../../.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/b/c/../../../"), "/");
+}
+
+BOOST_AUTO_TEST_CASE(normalizeCLIPathForVFS_relative_path)
+{
+	TemporaryDirectory tempDir({"x/y/z"}, TEST_CASE_NAME);
+	TemporaryWorkingDirectory tempWorkDir(tempDir.path() / "x/y/z");
+
+	// NOTE: If path to work dir contains symlinks (often the case on macOS), boost might resolve
+	// them, making the path different from tempDirPath.
+	boost::filesystem::path expectedPrefix = boost::filesystem::current_path().parent_path().parent_path().parent_path();
+	// On Windows tempDir.path() normally contains the drive letter while the normalized path should not.
+	expectedPrefix = "/" / expectedPrefix.relative_path();
+	soltestAssert(expectedPrefix.is_absolute() || expectedPrefix.root_path() == "/", "");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("."), expectedPrefix / "x/y/z/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("./"), expectedPrefix / "x/y/z/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS(".//"), expectedPrefix / "x/y/z/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS(".."), expectedPrefix / "x/y");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../"), expectedPrefix / "x/y/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("..//"), expectedPrefix / "x/y/");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a"), expectedPrefix / "x/y/z/a");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/"), expectedPrefix / "x/y/z/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/."), expectedPrefix / "x/y/z/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("./a"), expectedPrefix / "x/y/z/a");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("./a/"), expectedPrefix / "x/y/z/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("./a/."), expectedPrefix / "x/y/z/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("./a/./"), expectedPrefix / "x/y/z/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("./a/.//"), expectedPrefix / "x/y/z/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("./a/./."), expectedPrefix / "x/y/z/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("./a/././"), expectedPrefix / "x/y/z/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("./a/././/"), expectedPrefix / "x/y/z/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/b"), expectedPrefix / "x/y/z/a/b");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/b/"), expectedPrefix / "x/y/z/a/b/");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../a/b"), expectedPrefix / "x/y/a/b");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../../a/b"), expectedPrefix / "x/a/b");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("./a/b"), expectedPrefix / "x/y/z/a/b");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("././a/b"), expectedPrefix / "x/y/z/a/b");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/./b/"), expectedPrefix / "x/y/z/a/b/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/../a/b/"), expectedPrefix / "x/y/z/a/b/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/b/c/.."), expectedPrefix / "x/y/z/a/b");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/b/c/../"), expectedPrefix / "x/y/z/a/b/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/b/c/..//"), expectedPrefix / "x/y/z/a/b/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/b/c/../.."), expectedPrefix / "x/y/z/a");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/b/c/../../"), expectedPrefix / "x/y/z/a/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/b/c/../..//"), expectedPrefix / "x/y/z/a/");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../../a/.././../p/../q/../a/b"), expectedPrefix / "a/b");
+}
+
+BOOST_AUTO_TEST_CASE(normalizeCLIPathForVFS_redundant_slashes)
+{
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("///"), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("////"), "/");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("////a/b/"), "/a/b/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a//b/"), "/a/b/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a////b/"), "/a/b/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/b//"), "/a/b/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/b////"), "/a/b/");
+}
+
+BOOST_AUTO_TEST_CASE(normalizeCLIPathForVFS_unc_path)
+{
+	TemporaryDirectory tempDir(TEST_CASE_NAME);
+	TemporaryWorkingDirectory tempWorkDir(tempDir);
+
+	// On Windows tempDir.path() normally contains the drive letter while the normalized path should not.
+	boost::filesystem::path expectedWorkDir = "/" / boost::filesystem::current_path().relative_path();
+	soltestAssert(expectedWorkDir.is_absolute() || expectedWorkDir.root_path() == "/", "");
+
+	// UNC paths start with // or \\ followed by a name. They are used for network shares on Windows.
+	// On UNIX systems they are not supported but still treated in a special way.
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("//host/"), "//host/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("//host/a/b"), "//host/a/b");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("//host/a/b/"), "//host/a/b/");
+
+#if defined(_WIN32)
+	// On Windows an UNC path can also start with \\ instead of //
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("\\\\host/"), "//host/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("\\\\host/a/b"), "//host/a/b");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("\\\\host/a/b/"), "//host/a/b/");
+#else
+	// On UNIX systems it's just a fancy relative path instead
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("\\\\host/"), expectedWorkDir / "\\\\host/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("\\\\host/a/b"), expectedWorkDir / "\\\\host/a/b");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("\\\\host/a/b/"), expectedWorkDir / "\\\\host/a/b/");
+#endif
+}
+
+BOOST_AUTO_TEST_CASE(normalizeCLIPathForVFS_root_name_only)
+{
+	TemporaryDirectory tempDir(TEST_CASE_NAME);
+	TemporaryWorkingDirectory tempWorkDir(tempDir);
+
+	boost::filesystem::path expectedWorkDir = "/" / boost::filesystem::current_path().relative_path();
+	soltestAssert(expectedWorkDir.is_absolute() || expectedWorkDir.root_path() == "/", "");
+
+	// A root **path** consists of a directory name (typically / or \) and the root name (drive
+	// letter (C:), UNC host name (//host), etc.). Either can be empty. Root path as a whole may be
+	// an absolute path but root name on its own is considered relative. For example on Windows
+	// C:\ represents the root directory of drive C: but C: on its own refers to the current working
+	// directory.
+
+	// UNC paths
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("//"), "//" / expectedWorkDir);
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("//host"), "//host" / expectedWorkDir);
+
+	// On UNIX systems root name is empty.
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS(""), expectedWorkDir);
+
+#if defined(_WIN32)
+	boost::filesystem::path driveLetter = boost::filesystem::current_path().root_name();
+	solAssert(!driveLetter.empty(), "");
+	solAssert(driveLetter.is_relative(), "");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS(driveLetter), expectedWorkDir);
+#endif
+}
+
+BOOST_AUTO_TEST_CASE(normalizeCLIPathForVFS_stripping_root_name)
+{
+	TemporaryDirectory tempDir(TEST_CASE_NAME);
+	TemporaryWorkingDirectory tempWorkDir(tempDir);
+
+	soltestAssert(boost::filesystem::current_path().is_absolute(), "");
+#if defined(_WIN32)
+	soltestAssert(!boost::filesystem::current_path().root_name().empty(), "");
+#endif
+
+	boost::filesystem::path normalizedPath = FileReader::normalizeCLIPathForVFS(boost::filesystem::current_path());
+	BOOST_CHECK_EQUAL(normalizedPath, "/" / boost::filesystem::current_path().relative_path());
+	BOOST_TEST(normalizedPath.root_name().empty());
+	BOOST_CHECK_EQUAL(normalizedPath.root_directory(), "/");
+}
+
+BOOST_AUTO_TEST_CASE(normalizeCLIPathForVFS_path_beyond_root)
+{
+	TemporaryWorkingDirectory tempWorkDir("/");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/../"), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/../."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/../.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/../a"), "/a");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/../a/.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/../a/../.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/../../a"), "/a");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/../../a/.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/../../a/../.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/../.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("/a/../../b/../.."), "/");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS(".."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../"), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../a"), "/a");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../a/.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../a/../.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../../a"), "/a");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../../a/.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("../../a/../.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/../.."), "/");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("a/../../b/../.."), "/");
+}
+
+BOOST_AUTO_TEST_CASE(normalizeCLIPathForVFS_case_sensitivity)
+{
+	TemporaryDirectory tempDir(TEST_CASE_NAME);
+	TemporaryWorkingDirectory tempWorkDir(tempDir);
+
+	boost::filesystem::path expectedPrefix = "/" / tempDir.path().relative_path();
+	soltestAssert(expectedPrefix.is_absolute() || expectedPrefix.root_path() == "/", "");
+
+	BOOST_TEST(FileReader::normalizeCLIPathForVFS(tempDir.path() / "abc") == expectedPrefix / "abc");
+	BOOST_TEST(FileReader::normalizeCLIPathForVFS(tempDir.path() / "abc") != expectedPrefix / "ABC");
+	BOOST_TEST(FileReader::normalizeCLIPathForVFS(tempDir.path() / "ABC") != expectedPrefix / "abc");
+	BOOST_TEST(FileReader::normalizeCLIPathForVFS(tempDir.path() / "ABC") == expectedPrefix / "ABC");
+}
+
+BOOST_AUTO_TEST_CASE(normalizeCLIPathForVFS_path_separators)
+{
+	// Even on Windows we want / as a separator.
+	BOOST_TEST((FileReader::normalizeCLIPathForVFS("/a/b/c").native() == boost::filesystem::path("/a/b/c").native()));
+}
+
+BOOST_AUTO_TEST_CASE(normalizeCLIPathForVFS_should_not_resolve_symlinks)
+{
+	TemporaryDirectory tempDir({"abc/"}, TEST_CASE_NAME);
+	soltestAssert(tempDir.path().is_absolute(), "");
+
+	if (!createSymlinkIfSupportedByFilesystem(tempDir.path() / "abc", tempDir.path() / "sym", true))
+		return;
+
+	boost::filesystem::path expectedPrefix = "/" / tempDir.path().relative_path();
+	soltestAssert(expectedPrefix.is_absolute() || expectedPrefix.root_path() == "/", "");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS(tempDir.path() / "sym/contract.sol"), expectedPrefix / "sym/contract.sol");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS(tempDir.path() / "abc/contract.sol"), expectedPrefix / "abc/contract.sol");
+}
+
+BOOST_AUTO_TEST_CASE(normalizeCLIPathForVFS_should_resolve_symlinks_in_workdir_when_path_is_relative)
+{
+	TemporaryDirectory tempDir({"abc/"}, TEST_CASE_NAME);
+	soltestAssert(tempDir.path().is_absolute(), "");
+
+	if (!createSymlinkIfSupportedByFilesystem(tempDir.path() / "abc", tempDir.path() / "sym", true))
+		return;
+
+	TemporaryWorkingDirectory tempWorkDir(tempDir.path() / "sym");
+	boost::filesystem::path expectedWorkDir = "/" / boost::filesystem::weakly_canonical(boost::filesystem::current_path()).relative_path();
+	soltestAssert(expectedWorkDir.is_absolute() || expectedWorkDir.root_path() == "/", "");
+
+	boost::filesystem::path expectedPrefix = "/" / tempDir.path().relative_path();
+	soltestAssert(expectedPrefix.is_absolute() || expectedPrefix.root_path() == "/", "");
+
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS("contract.sol"), expectedWorkDir / "contract.sol");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS(tempDir.path() / "sym/contract.sol"), expectedPrefix / "sym/contract.sol");
+	BOOST_CHECK_EQUAL(FileReader::normalizeCLIPathForVFS(tempDir.path() / "abc/contract.sol"), expectedPrefix / "abc/contract.sol");
+}
+
+BOOST_AUTO_TEST_CASE(isPathPrefix_file_prefix)
+{
+	BOOST_TEST(FileReader::isPathPrefix("/", "/contract.sol"));
+	BOOST_TEST(FileReader::isPathPrefix("/contract.sol", "/contract.sol"));
+	BOOST_TEST(FileReader::isPathPrefix("/contract.sol/", "/contract.sol"));
+	BOOST_TEST(FileReader::isPathPrefix("/contract.sol/.", "/contract.sol"));
+
+	BOOST_TEST(FileReader::isPathPrefix("/", "/a/bc/def/contract.sol"));
+	BOOST_TEST(FileReader::isPathPrefix("/a", "/a/bc/def/contract.sol"));
+	BOOST_TEST(FileReader::isPathPrefix("/a/", "/a/bc/def/contract.sol"));
+	BOOST_TEST(FileReader::isPathPrefix("/a/bc", "/a/bc/def/contract.sol"));
+	BOOST_TEST(FileReader::isPathPrefix("/a/bc/def/contract.sol", "/a/bc/def/contract.sol"));
+
+	BOOST_TEST(FileReader::isPathPrefix("/", "/a/bc/def/contract.sol"));
+	BOOST_TEST(FileReader::isPathPrefix("/a", "/a/bc/def/contract.sol"));
+	BOOST_TEST(FileReader::isPathPrefix("/a/", "/a/bc/def/contract.sol"));
+	BOOST_TEST(FileReader::isPathPrefix("/a/bc", "/a/bc/def/contract.sol"));
+	BOOST_TEST(FileReader::isPathPrefix("/a/bc/def/contract.sol", "/a/bc/def/contract.sol"));
+
+	BOOST_TEST(!FileReader::isPathPrefix("/contract.sol", "/token.sol"));
+	BOOST_TEST(!FileReader::isPathPrefix("/contract", "/contract.sol"));
+	BOOST_TEST(!FileReader::isPathPrefix("/contract.sol", "/contract"));
+	BOOST_TEST(!FileReader::isPathPrefix("/contract.so", "/contract.sol"));
+	BOOST_TEST(!FileReader::isPathPrefix("/contract.sol", "/contract.so"));
+
+	BOOST_TEST(!FileReader::isPathPrefix("/a/b/c/contract.sol", "/a/b/contract.sol"));
+	BOOST_TEST(!FileReader::isPathPrefix("/a/b/contract.sol", "/a/b/c/contract.sol"));
+	BOOST_TEST(!FileReader::isPathPrefix("/a/b/c/contract.sol", "/a/b/c/d/contract.sol"));
+	BOOST_TEST(!FileReader::isPathPrefix("/a/b/c/d/contract.sol", "/a/b/c/contract.sol"));
+	BOOST_TEST(!FileReader::isPathPrefix("/a/b/c/contract.sol", "/contract.sol"));
+}
+
+BOOST_AUTO_TEST_CASE(isPathPrefix_directory_prefix)
+{
+	BOOST_TEST(FileReader::isPathPrefix("/", "/"));
+	BOOST_TEST(!FileReader::isPathPrefix("/a/b/c/", "/"));
+	BOOST_TEST(!FileReader::isPathPrefix("/a/b/c", "/"));
+
+	BOOST_TEST(FileReader::isPathPrefix("/", "/a/bc/"));
+	BOOST_TEST(FileReader::isPathPrefix("/a", "/a/bc/"));
+	BOOST_TEST(FileReader::isPathPrefix("/a/", "/a/bc/"));
+	BOOST_TEST(FileReader::isPathPrefix("/a/bc", "/a/bc/"));
+	BOOST_TEST(FileReader::isPathPrefix("/a/bc/", "/a/bc/"));
+
+	BOOST_TEST(!FileReader::isPathPrefix("/a", "/b/"));
+	BOOST_TEST(!FileReader::isPathPrefix("/a/", "/b/"));
+	BOOST_TEST(!FileReader::isPathPrefix("/a/contract.sol", "/a/b/"));
+
+	BOOST_TEST(!FileReader::isPathPrefix("/a/b/c/", "/a/b/"));
+	BOOST_TEST(!FileReader::isPathPrefix("/a/b/c", "/a/b/"));
+}
+
+BOOST_AUTO_TEST_CASE(isPathPrefix_unc_path)
+{
+	BOOST_TEST(FileReader::isPathPrefix("//host/a/b/", "//host/a/b/"));
+	BOOST_TEST(FileReader::isPathPrefix("//host/a/b", "//host/a/b/"));
+	BOOST_TEST(FileReader::isPathPrefix("//host/a/", "//host/a/b/"));
+	BOOST_TEST(FileReader::isPathPrefix("//host/a", "//host/a/b/"));
+	BOOST_TEST(FileReader::isPathPrefix("//host/", "//host/a/b/"));
+
+	// NOTE: //host and // cannot be passed to isPathPrefix() because they are considered relative.
+
+	BOOST_TEST(!FileReader::isPathPrefix("//host1/", "//host2/"));
+	BOOST_TEST(!FileReader::isPathPrefix("//host1/a/b/", "//host2/a/b/"));
+
+	BOOST_TEST(!FileReader::isPathPrefix("/a/b/c/", "//a/b/c/"));
+	BOOST_TEST(!FileReader::isPathPrefix("//a/b/c/", "/a/b/c/"));
+}
+
+BOOST_AUTO_TEST_CASE(isPathPrefix_case_sensitivity)
+{
+	BOOST_TEST(!FileReader::isPathPrefix("/a.sol", "/A.sol"));
+	BOOST_TEST(!FileReader::isPathPrefix("/A.sol", "/a.sol"));
+	BOOST_TEST(!FileReader::isPathPrefix("/A/", "/a/"));
+	BOOST_TEST(!FileReader::isPathPrefix("/a/", "/A/"));
+	BOOST_TEST(!FileReader::isPathPrefix("/a/BC/def/", "/a/bc/def/contract.sol"));
+}
+
+BOOST_AUTO_TEST_CASE(stripPrefixIfPresent_file_prefix)
+{
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/", "/contract.sol"), "contract.sol");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/contract.sol", "/contract.sol"), ".");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/contract.sol/", "/contract.sol"), ".");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/contract.sol/.", "/contract.sol"), ".");
+
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/", "/a/bc/def/contract.sol"), "a/bc/def/contract.sol");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a", "/a/bc/def/contract.sol"), "bc/def/contract.sol");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a/", "/a/bc/def/contract.sol"), "bc/def/contract.sol");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a/bc", "/a/bc/def/contract.sol"), "def/contract.sol");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a/bc/def/", "/a/bc/def/contract.sol"), "contract.sol");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a/bc/def/contract.sol", "/a/bc/def/contract.sol"), ".");
+
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/contract.sol", "/token.sol"), "/token.sol");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/contract", "/contract.sol"), "/contract.sol");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/contract.sol", "/contract"), "/contract");
+
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a/b/c/contract.sol", "/a/b/contract.sol"), "/a/b/contract.sol");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a/b/contract.sol", "/a/b/c/contract.sol"), "/a/b/c/contract.sol");
+}
+
+BOOST_AUTO_TEST_CASE(stripPrefixIfPresent_directory_prefix)
+{
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/", "/"), ".");
+
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/", "/a/bc/def/"), "a/bc/def/");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a", "/a/bc/def/"), "bc/def/");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a/", "/a/bc/def/"), "bc/def/");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a/bc", "/a/bc/def/"), "def/");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a/bc/def/", "/a/bc/def/"), ".");
+
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a", "/b/"), "/b/");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a/", "/b/"), "/b/");
+
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a/b/c/", "/a/b/"), "/a/b/");
+	BOOST_CHECK_EQUAL(FileReader::stripPrefixIfPresent("/a/b/c", "/a/b/"), "/a/b/");
+}
+
+BOOST_AUTO_TEST_CASE(isUNCPath)
+{
+	BOOST_TEST(FileReader::isUNCPath("//"));
+	BOOST_TEST(FileReader::isUNCPath("//root"));
+	BOOST_TEST(FileReader::isUNCPath("//root/"));
+
+#if defined(_WIN32)
+	// On Windows boost sees these as ///, which is equivalent to /
+	BOOST_TEST(!FileReader::isUNCPath("//\\"));
+	BOOST_TEST(!FileReader::isUNCPath("\\\\/"));
+	BOOST_TEST(!FileReader::isUNCPath("\\/\\"));
+
+	BOOST_TEST(FileReader::isUNCPath("\\\\"));
+	BOOST_TEST(FileReader::isUNCPath("\\\\root"));
+	BOOST_TEST(FileReader::isUNCPath("\\\\root/"));
+#else
+	// On UNIX it's actually an UNC path
+	BOOST_TEST(FileReader::isUNCPath("//\\"));
+
+	// On UNIX these are just weird relative directory names consisting only of backslashes.
+	BOOST_TEST(!FileReader::isUNCPath("\\\\/"));
+	BOOST_TEST(!FileReader::isUNCPath("\\/\\"));
+
+	BOOST_TEST(!FileReader::isUNCPath("\\\\"));
+	BOOST_TEST(!FileReader::isUNCPath("\\\\root"));
+	BOOST_TEST(!FileReader::isUNCPath("\\\\root/"));
+#endif
+
+	BOOST_TEST(!FileReader::isUNCPath("\\/"));
+	BOOST_TEST(!FileReader::isUNCPath("/\\"));
+
+	BOOST_TEST(!FileReader::isUNCPath(""));
+	BOOST_TEST(!FileReader::isUNCPath("."));
+	BOOST_TEST(!FileReader::isUNCPath(".."));
+	BOOST_TEST(!FileReader::isUNCPath("/"));
+	BOOST_TEST(!FileReader::isUNCPath("a"));
+	BOOST_TEST(!FileReader::isUNCPath("a/b/c"));
+	BOOST_TEST(!FileReader::isUNCPath("contract.sol"));
+}
+
+BOOST_AUTO_TEST_SUITE_END()
+
+} // namespace solidity::frontend::test

test/libsolidity/smtCheckerTests/abi/abi_decode_1_tuple.sol

@@ -8,5 +8,3 @@ contract C {
 // ----
 // Warning 8364: (116-125): Assertion checker does not yet implement type type(uint256[] memory)
 // Warning 8364: (115-126): Assertion checker does not yet implement type type(uint256[] memory)
-// Warning 8364: (116-125): Assertion checker does not yet implement type type(uint256[] memory)
-// Warning 8364: (115-126): Assertion checker does not yet implement type type(uint256[] memory)

test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol

@@ -30,6 +30,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 8364: (162-168): Assertion checker does not yet implement type type(uint256[] memory)
 // Warning 8364: (170-176): Assertion checker does not yet implement type type(uint256[] memory)
@@ -45,6 +46,9 @@ contract C {
 // Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
 // Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
 // Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)
+// Warning 1218: (1009-1037): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (1056-1084): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (1103-1131): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (182-210): CHC: Assertion violation happens here.
 // Warning 6328: (335-363): CHC: Assertion violation happens here.
 // Warning 6328: (414-442): CHC: Assertion violation happens here.
@@ -52,20 +56,9 @@ contract C {
 // Warning 6328: (607-635): CHC: Assertion violation happens here.
 // Warning 6328: (654-682): CHC: Assertion violation happens here.
 // Warning 6328: (879-916): CHC: Assertion violation happens here.
-// Warning 6328: (1009-1037): CHC: Assertion violation happens here.
+// Warning 6328: (1009-1037): CHC: Assertion violation might happen here.
-// Warning 6328: (1056-1084): CHC: Assertion violation happens here.
+// Warning 6328: (1056-1084): CHC: Assertion violation might happen here.
-// Warning 6328: (1103-1131): CHC: Assertion violation happens here.
+// Warning 6328: (1103-1131): CHC: Assertion violation might happen here.
-// Warning 8364: (162-168): Assertion checker does not yet implement type type(uint256[] memory)
+// Warning 4661: (1009-1037): BMC: Assertion violation happens here.
-// Warning 8364: (170-176): Assertion checker does not yet implement type type(uint256[] memory)
+// Warning 4661: (1056-1084): BMC: Assertion violation happens here.
-// Warning 8364: (283-289): Assertion checker does not yet implement type type(uint256[] memory)
+// Warning 4661: (1103-1131): BMC: Assertion violation happens here.
-// Warning 8364: (291-297): Assertion checker does not yet implement type type(uint256[] memory)
-// Warning 8364: (532-538): Assertion checker does not yet implement type type(uint256[] memory)
-// Warning 8364: (540-546): Assertion checker does not yet implement type type(uint256[] memory)
-// Warning 8364: (548-554): Assertion checker does not yet implement type type(uint256[] memory)
-// Warning 8364: (769-775): Assertion checker does not yet implement type type(uint256[] memory)
-// Warning 8364: (769-777): Assertion checker does not yet implement type type(uint256[] memory[] memory)
-// Warning 8364: (779-785): Assertion checker does not yet implement type type(uint256[] memory)
-// Warning 8364: (779-787): Assertion checker does not yet implement type type(uint256[] memory[] memory)
-// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
-// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
-// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)

test/libsolidity/smtCheckerTests/abi/abi_decode_simple.sol

@@ -21,10 +21,14 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 1218: (505-519): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (538-552): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (209-223): CHC: Assertion violation happens here.
 // Warning 6328: (260-274): CHC: Assertion violation happens here.
 // Warning 6328: (359-373): CHC: Assertion violation happens here.
 // Warning 6328: (392-406): CHC: Assertion violation happens here.
 // Warning 6328: (425-434): CHC: Assertion violation happens here.
-// Warning 6328: (505-519): CHC: Assertion violation happens here.
+// Warning 6328: (505-519): CHC: Assertion violation might happen here.
-// Warning 6328: (538-552): CHC: Assertion violation happens here.
+// Warning 6328: (538-552): CHC: Assertion violation might happen here.
+// Warning 4661: (505-519): BMC: Assertion violation happens here.
+// Warning 4661: (538-552): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_function.sol

@@ -7,4 +7,3 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6031: (54-60): Internal error: Expression undefined for SMT solver.
-// Warning 6031: (54-60): Internal error: Expression undefined for SMT solver.

test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol

@@ -23,7 +23,15 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (322-352): CHC: Assertion violation happens here.
+// Warning 1218: (322-352): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (419-449): CHC: Assertion violation happens here.
+// Warning 1218: (419-449): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (528-558): CHC: Assertion violation happens here.
+// Warning 1218: (528-558): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (577-607): CHC: Assertion violation happens here.
+// Warning 1218: (577-607): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (322-352): CHC: Assertion violation might happen here.
+// Warning 6328: (419-449): CHC: Assertion violation might happen here.
+// Warning 6328: (528-558): CHC: Assertion violation might happen here.
+// Warning 6328: (577-607): CHC: Assertion violation might happen here.
+// Warning 4661: (322-352): BMC: Assertion violation happens here.
+// Warning 4661: (419-449): BMC: Assertion violation happens here.
+// Warning 4661: (528-558): BMC: Assertion violation happens here.
+// Warning 4661: (577-607): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol

@@ -22,15 +22,17 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (226-256): CHC: Assertion violation happens here.
+// Warning 6328: (226-256): CHC: Assertion violation might happen here.
 // Warning 6328: (310-340): CHC: Assertion violation might happen here.
 // Warning 6328: (483-513): CHC: Assertion violation might happen here.
 // Warning 6328: (568-598): CHC: Assertion violation might happen here.
 // Warning 6328: (654-684): CHC: Assertion violation might happen here.
+// Warning 4661: (226-256): BMC: Assertion violation happens here.
 // Warning 4661: (310-340): BMC: Assertion violation happens here.
 // Warning 4661: (483-513): BMC: Assertion violation happens here.
 // Warning 4661: (568-598): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol

@@ -23,12 +23,13 @@ contract C {
 // SMTEngine: all
 // SMTShowUnproved: no
 // ----
+// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (226-256): CHC: Assertion violation happens here.
+// Warning 5840: CHC: 5 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
-// Warning 5840: CHC: 4 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+// Warning 4661: (226-256): BMC: Assertion violation happens here.
 // Warning 4661: (310-340): BMC: Assertion violation happens here.
 // Warning 4661: (483-513): BMC: Assertion violation happens here.
 // Warning 4661: (568-598): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol

@@ -20,6 +20,12 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (298-328): CHC: Assertion violation happens here.
+// Warning 1218: (298-328): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (389-419): CHC: Assertion violation happens here.
+// Warning 1218: (389-419): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (492-522): CHC: Assertion violation happens here.
+// Warning 1218: (492-522): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (298-328): CHC: Assertion violation might happen here.
+// Warning 6328: (389-419): CHC: Assertion violation might happen here.
+// Warning 6328: (492-522): CHC: Assertion violation might happen here.
+// Warning 4661: (298-328): BMC: Assertion violation happens here.
+// Warning 4661: (389-419): BMC: Assertion violation happens here.
+// Warning 4661: (492-522): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol

@@ -19,13 +19,15 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (208-238): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (208-238): CHC: Assertion violation happens here.
+// Warning 6328: (208-238): CHC: Assertion violation might happen here.
 // Warning 6328: (286-316): CHC: Assertion violation might happen here.
 // Warning 6328: (453-483): CHC: Assertion violation might happen here.
 // Warning 6328: (532-562): CHC: Assertion violation might happen here.
+// Warning 4661: (208-238): BMC: Assertion violation happens here.
 // Warning 4661: (286-316): BMC: Assertion violation happens here.
 // Warning 4661: (453-483): BMC: Assertion violation happens here.
 // Warning 4661: (532-562): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol

@@ -24,15 +24,18 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
+// Warning 1218: (578-608): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (325-355): CHC: Assertion violation happens here.
-// Warning 6328: (578-608): CHC: Assertion violation happens here.
+// Warning 6328: (578-608): CHC: Assertion violation might happen here.
 // Warning 6328: (691-721): CHC: Assertion violation might happen here.
 // Warning 6328: (959-989): CHC: Assertion violation might happen here.
 // Warning 6328: (1079-1109): CHC: Assertion violation might happen here.
+// Warning 4661: (578-608): BMC: Assertion violation happens here.
 // Warning 4661: (691-721): BMC: Assertion violation happens here.
 // Warning 4661: (959-989): BMC: Assertion violation happens here.
 // Warning 4661: (1079-1109): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol

@@ -25,14 +25,16 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (579-609): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (326-356): CHC: Assertion violation happens here.
-// Warning 6328: (579-609): CHC: Assertion violation happens here.
+// Warning 6328: (579-609): CHC: Assertion violation might happen here.
 // Warning 6328: (692-722): CHC: Assertion violation might happen here.
 // Warning 6328: (960-990): CHC: Assertion violation might happen here.
 // Warning 6328: (1080-1110): CHC: Assertion violation might happen here.
+// Warning 4661: (579-609): BMC: Assertion violation happens here.
 // Warning 4661: (692-722): BMC: Assertion violation happens here.
 // Warning 4661: (960-990): BMC: Assertion violation happens here.
 // Warning 4661: (1080-1110): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_simple.sol

@@ -23,9 +23,12 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 5667: (100-115): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 1218: (855-885): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (571-601): CHC: Assertion violation happens here.
 // Warning 6328: (691-721): CHC: Assertion violation happens here.
 // Warning 6328: (740-770): CHC: Assertion violation happens here.
-// Warning 6328: (855-885): CHC: Assertion violation happens here.
+// Warning 6328: (855-885): CHC: Assertion violation might happen here.
+// Warning 4661: (855-885): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol

@@ -22,15 +22,17 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (252-282): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (347-377): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (531-561): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (627-657): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (746-776): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (252-282): CHC: Assertion violation happens here.
+// Warning 6328: (252-282): CHC: Assertion violation might happen here.
 // Warning 6328: (347-377): CHC: Assertion violation might happen here.
 // Warning 6328: (531-561): CHC: Assertion violation might happen here.
 // Warning 6328: (627-657): CHC: Assertion violation might happen here.
 // Warning 6328: (746-776): CHC: Assertion violation might happen here.
+// Warning 4661: (252-282): BMC: Assertion violation happens here.
 // Warning 4661: (347-377): BMC: Assertion violation happens here.
 // Warning 4661: (531-561): BMC: Assertion violation happens here.
 // Warning 4661: (627-657): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol

@@ -25,14 +25,16 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (588-618): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (702-732): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (334-364): CHC: Assertion violation happens here.
-// Warning 6328: (588-618): CHC: Assertion violation happens here.
+// Warning 6328: (588-618): CHC: Assertion violation might happen here.
 // Warning 6328: (702-732): CHC: Assertion violation might happen here.
 // Warning 6328: (971-1001): CHC: Assertion violation might happen here.
 // Warning 6328: (1086-1116): CHC: Assertion violation might happen here.
+// Warning 4661: (588-618): BMC: Assertion violation happens here.
 // Warning 4661: (702-732): BMC: Assertion violation happens here.
 // Warning 4661: (971-1001): BMC: Assertion violation happens here.
 // Warning 4661: (1086-1116): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol

@@ -25,14 +25,16 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (589-619): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (703-733): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (335-365): CHC: Assertion violation happens here.
-// Warning 6328: (589-619): CHC: Assertion violation happens here.
+// Warning 6328: (589-619): CHC: Assertion violation might happen here.
 // Warning 6328: (703-733): CHC: Assertion violation might happen here.
 // Warning 6328: (972-1002): CHC: Assertion violation might happen here.
 // Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
+// Warning 4661: (589-619): BMC: Assertion violation happens here.
 // Warning 4661: (703-733): BMC: Assertion violation happens here.
 // Warning 4661: (972-1002): BMC: Assertion violation happens here.
 // Warning 4661: (1087-1117): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol

@@ -24,7 +24,9 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 5667: (107-122): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 1218: (824-854): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (543-573): CHC: Assertion violation happens here.
 // Warning 6328: (664-694): CHC: Assertion violation happens here.
 // Warning 6328: (713-743): CHC: Assertion violation happens here.
-// Warning 6328: (824-854): CHC: Assertion violation happens here.
+// Warning 6328: (824-854): CHC: Assertion violation might happen here.
+// Warning 4661: (824-854): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol

@@ -22,15 +22,17 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (261-291): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (357-387): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (542-572): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (639-669): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (753-783): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (261-291): CHC: Assertion violation happens here.
+// Warning 6328: (261-291): CHC: Assertion violation might happen here.
 // Warning 6328: (357-387): CHC: Assertion violation might happen here.
 // Warning 6328: (542-572): CHC: Assertion violation might happen here.
 // Warning 6328: (639-669): CHC: Assertion violation might happen here.
 // Warning 6328: (753-783): CHC: Assertion violation might happen here.
+// Warning 4661: (261-291): BMC: Assertion violation happens here.
 // Warning 4661: (357-387): BMC: Assertion violation happens here.
 // Warning 4661: (542-572): BMC: Assertion violation happens here.
 // Warning 4661: (639-669): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol

@@ -14,5 +14,5 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (139-161): CHC: Assertion violation happens here.\nCounterexample:\ndata = [98]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()
+// Warning 6328: (139-161): CHC: Assertion violation happens here.
 // Warning 6328: (263-290): CHC: Assertion violation happens here.\nCounterexample:\ndata = [1]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol

@@ -21,4 +21,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (362-420): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g()
+// Warning 6328: (362-420): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol

@@ -13,4 +13,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (204-230): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
+// Warning 6328: (204-230): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol

@@ -13,4 +13,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (203-244): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
+// Warning 6328: (203-244): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol

@@ -19,4 +19,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (265-310): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\none = 1\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()
+// Warning 6328: (265-310): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol

@@ -23,4 +23,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (435-508): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\nval = 2\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g()
+// Warning 6328: (435-508): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_function_return_value.sol

@@ -0,0 +1,20 @@
+contract C {
+	bytes x;
+
+	function getX() internal view returns (bytes storage) {
+		return x;
+	}
+
+	function s() public {
+		require(x.length == 0);
+		getX().push("a");
+		assert(x.length == 1); // should hold but knowledge is erased due to pushing a reference
+		assert(x.length == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (168-189): CHC: Assertion violation happens here.
+// Warning 6328: (259-280): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol

@@ -12,5 +12,5 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (90-116): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
-// Warning 6328: (170-186): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
+// Warning 6328: (170-186): CHC: Assertion violation happens here.
-// Warning 6328: (190-246): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
+// Warning 6328: (190-246): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol

@@ -14,5 +14,5 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6368: (188-192): CHC: Out of bounds access happens here.\nCounterexample:\na = []\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
-// Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [25, 25, 25, 25, 25, 25, 25, 25], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15]]\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
+// Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
 // Warning 6328: (181-202): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol

@@ -15,5 +15,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (152-181): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[], [], []]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()\n    C.s() -- internal call
+// Warning 6368: (159-169): CHC: Out of bounds access happens here.
+// Warning 6328: (152-181): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero.sol

@@ -0,0 +1,11 @@
+contract C {
+	constructor() payable {
+		assert(address(this).balance == 0); // should fail
+		assert(address(this).balance > 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (40-74): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (93-126): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()

test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol

@@ -0,0 +1,13 @@
+contract C {
+	constructor() payable {
+		require(msg.value > 100);
+	}
+	function f() public view {
+		assert(address(this).balance > 100); // should hold
+		assert(address(this).balance > 200); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (153-188): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ value: 101 }\nC.f()

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol

@@ -0,0 +1,18 @@
+contract C {
+	uint prevBalance;
+	constructor() payable {
+		prevBalance = address(this).balance;
+	}
+	function f() public payable {
+		assert(address(this).balance == prevBalance + msg.value); // should fail because there might be funds from selfdestruct/block.coinbase
+		assert(address(this).balance < prevBalance + msg.value); // should fail
+		assert(address(this).balance >= prevBalance + msg.value); // should hold
+		prevBalance = address(this).balance;
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (132-188): CHC: Assertion violation happens here.
+// Warning 6328: (269-324): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol

@@ -0,0 +1,19 @@
+contract C {
+	uint x;
+	bool once;
+	constructor() payable {
+		x = address(this).balance;
+	}
+	function f() public payable {
+		require(!once);
+		once = true;
+		require(msg.value > 0);
+		assert(address(this).balance > x); // should hold
+		assert(address(this).balance > x + 10); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4984: (266-272): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = true\n\nTransaction trace:\nC.constructor(){ value: 28100 }\nState: x = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = false\nC.f(){ value: 8 }
+// Warning 6328: (235-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, once = true\n\nTransaction trace:\nC.constructor()\nState: x = 0, once = false\nC.f(){ value: 8 }

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_3.sol

@@ -0,0 +1,9 @@
+contract C {
+	constructor() payable {
+		assert(address(this).balance == msg.value); // should fail because there might be funds from before deployment
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (40-82): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol

@@ -0,0 +1,21 @@
+contract C {
+	uint c;
+	function f() public payable {
+		require(msg.value > 10);
+		++c;
+	}
+	function inv() public view {
+		assert(address(this).balance >= c * 11); // should hold
+		assert(address(this).balance >= c * 12); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// 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(){ value: 11 }\nState: c = 1\nC.inv()
+// 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.

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol

@@ -0,0 +1,14 @@
+contract C {
+	uint sum = msg.value;
+	function f() public payable {
+		sum += msg.value;
+	}
+	function inv() public view {
+		assert(address(this).balance == sum); // should fail
+		assert(address(this).balance >= sum); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (122-158): CHC: Assertion violation happens here.\nCounterexample:\nsum = 0\n\nTransaction trace:\nC.constructor()\nState: sum = 0\nC.inv()

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol

@@ -0,0 +1,26 @@
+contract C {
+	bool once;
+	function f() public payable {
+		require(!once);
+		once = true;
+		require(msg.value == 10);
+		assert(address(this).balance >= 10); // should hold
+		assert(address(this).balance >= 20); // should fail
+		g();
+	}
+	function g() internal view {
+		assert(address(this).balance >= 10); // should hold
+		assert(address(this).balance >= 20); // should fail
+		h();
+	}
+	function h() internal view {
+		assert(address(this).balance >= 10); // should hold
+		assert(address(this).balance >= 20); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (173-208): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ value: 10 }
+// Warning 6328: (321-356): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ value: 10 }\n    C.g(){ value: 10 } -- internal call
+// Warning 6328: (469-504): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ value: 10 }\n    C.g(){ value: 10 } -- internal call\n        C.h(){ value: 10 } -- internal call

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol

@@ -0,0 +1,18 @@
+interface I {
+	function ext() external;
+}
+
+contract C {
+	function f(I _i) public {
+		uint x = address(this).balance;
+		_i.ext();
+		assert(address(this).balance == x); // should fail
+		assert(address(this).balance >= x); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (131-165): CHC: Assertion violation might happen here.
+// Warning 4661: (131-165): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol

@@ -0,0 +1,14 @@
+contract C {
+	function f(address _a) public {
+		uint x = address(this).balance;
+		_a.call("");
+		assert(address(this).balance == x); // should fail
+		assert(address(this).balance >= x); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 9302: (82-93): Return value of low-level calls not used.
+// Warning 6328: (97-131): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol

@@ -0,0 +1,24 @@
+interface I {
+	function ext() external;
+}
+
+contract C {
+	bool lock;
+	modifier mutex {
+		require(!lock);
+		lock = true;
+		_;
+		lock = false;
+	}
+	function f(I _i) public mutex {
+		uint x = address(this).balance;
+		_i.ext();
+		assert(address(this).balance == x); // should hold
+		assert(address(this).balance < x); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (277-310): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol

@@ -0,0 +1,22 @@
+contract C {
+	constructor() payable {
+		require(msg.value > 100);
+	}
+	uint c;
+	function f(address payable _a, uint _v) public {
+		require(_v < 10);
+		require(c < 2);
+		++c;
+		_a.transfer(_v);
+	}
+	function inv() public view {
+		assert(address(this).balance > 80); // should hold
+		assert(address(this).balance > 90); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (280-314): CHC: Assertion violation happens here.
+// Warning 1236: (175-190): BMC: Insufficient funds happens here.

test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol

@@ -0,0 +1,24 @@
+contract C {
+	constructor() payable {
+		require(msg.value > 100);
+	}
+	function f(address payable _a, uint _v) public {
+		require(_v < 10);
+		_a.transfer(_v);
+	}
+	function inv() public view {
+		assert(address(this).balance > 0); // should fail
+		assert(address(this).balance > 80); // should fail
+		assert(address(this).balance > 90); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 1218: (193-226): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (193-226): CHC: Assertion violation might happen here.
+// Warning 6328: (245-279): CHC: Assertion violation happens here.
+// Warning 6328: (298-332): CHC: Assertion violation happens here.
+// Warning 1236: (141-156): BMC: Insufficient funds happens here.
+// Warning 4661: (193-226): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/blockchain_state/balance_zero.sol

@@ -0,0 +1,11 @@
+contract C {
+	constructor() {
+		assert(address(this).balance == 0); // should fail because there might be funds from before deployment
+		assert(address(this).balance > 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (32-66): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (137-170): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()

test/libsolidity/smtCheckerTests/blockchain_state/balance_zero_2.sol

@@ -0,0 +1,11 @@
+contract C {
+	function f() public view {
+		assert(address(this).balance == 0); // should fail because there might be funds from before deployment
+		assert(address(this).balance > 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (43-77): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (148-181): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/blockchain_state/balance_zero_3.sol

@@ -0,0 +1,18 @@
+contract C {
+	uint x = address(this).balance;
+	constructor() {
+		assert(x == 0); // should fail because there might be funds from before deployment
+		assert(x > 0); // should fail
+	}
+	function f() public view {
+		assert(x == 0); // should fail because there might be funds from before deployment
+		assert(x > 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (65-79): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (150-163): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (213-227): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.f()
+// Warning 6328: (298-311): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

test/libsolidity/smtCheckerTests/blockchain_state/balance_zero_4.sol

@@ -0,0 +1,21 @@
+contract C {
+	uint x = g();
+	function g() internal view returns (uint) {
+		return address(this).balance;
+	}
+	constructor() {
+		assert(x == 0); // should fail because there might be funds from before deployment
+		assert(x > 0); // should fail
+	}
+	function f() public view {
+		assert(x == 0); // should fail because there might be funds from before deployment
+		assert(x > 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (127-141): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (212-225): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (275-289): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.f()
+// Warning 6328: (360-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol

@@ -7,10 +7,11 @@ contract C {
 	function f(address payable a) public payable {
 		require(msg.value > 1);
 		uint b1 = address(this).balance;
+		require(a != address(this));
 		l(a);
 		uint b2 = address(this).balance;
 		assert(b1 == b2); // should fail
-		assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet
+		assert(b1 == b2 + 1); // should hold
 		assert(x == 0); // should hold
 	}
 }
@@ -18,7 +19,5 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (227-243): CHC: Assertion violation happens here.
+// Warning 6328: (258-274): CHC: Assertion violation happens here.
-// Warning 3944: (275-281): CHC: Underflow (resulting value less than 0) happens here.
-// Warning 6328: (262-282): CHC: Assertion violation happens here.
 // Warning 1236: (33-46): BMC: Insufficient funds happens here.

test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol

@@ -1,5 +1,6 @@
 library L {
 	function l(address payable a) internal {
+		require(a != address(this));
 		a.transfer(1);
 	}
 }
@@ -13,15 +14,13 @@ contract C {
 		a.l();
 		uint b2 = address(this).balance;
 		assert(b1 == b2); // should fail
-		assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet
+		assert(b1 == b2 + 1); // should hold
 		assert(x == 0); // should hold
 	}
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (284-300): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 21238\nb1 = 8856\nb2 = 8855\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(21238){ value: 11799 }\n    L.l(21238){ value: 11799 } -- internal call
+// Warning 6328: (315-331): CHC: Assertion violation happens here.
-// Warning 3944: (332-338): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\na = 38\nb1 = 1\nb2 = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(38){ value: 21240 }\n    L.l(38){ value: 21240 } -- internal call
+// Warning 1236: (87-100): BMC: Insufficient funds happens here.
-// Warning 6328: (319-339): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 21238\nb1 = 40\nb2 = 39\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(21238){ value: 8857 }\n    L.l(21238){ value: 8857 } -- internal call
-// Warning 1236: (56-69): BMC: Insufficient funds happens here.
-// Warning 1236: (56-69): BMC: Insufficient funds happens here.

test/libsolidity/smtCheckerTests/blockchain_state/library_public_1.sol

@@ -16,8 +16,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.
-// Warning 6328: (263-279): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\nb1 = 7720\nb2 = 7719\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0){ value: 5855 }
+// Warning 6328: (263-279): CHC: Assertion violation happens here.
-// Warning 6328: (359-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\nb1 = 39\nb2 = 38\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0){ value: 21240 }
+// Warning 6328: (359-373): CHC: Assertion violation happens here.
-// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol

@@ -24,4 +24,3 @@ contract C {
 // Warning 6328: (282-298): CHC: Assertion violation happens here.
 // Warning 6328: (317-331): CHC: Assertion violation happens here.
 // Warning 1236: (54-67): BMC: Insufficient funds happens here.
-// Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/blockchain_state/library_public_3.sol

@@ -26,4 +26,3 @@ contract C {
 // Warning 6328: (309-325): CHC: Assertion violation happens here.
 // Warning 6328: (405-419): CHC: Assertion violation happens here.
 // Warning 6328: (464-486): CHC: Assertion violation happens here.
-// Warning 4588: (265-270): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/blockchain_state/library_public_4.sol

@@ -27,4 +27,3 @@ contract C {
 // Warning 6328: (316-332): CHC: Assertion violation happens here.
 // Warning 6328: (412-426): CHC: Assertion violation happens here.
 // Warning 6328: (471-494): CHC: Assertion violation happens here.
-// Warning 4588: (272-277): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/bmc_coverage/unchecked_function_call_with_unchecked_block.sol

@@ -13,4 +13,3 @@ contract C {
 // SMTEngine: bmc
 // ----
 // Warning 4661: (85-98): BMC: Assertion violation happens here.
-// Warning 4661: (85-98): BMC: Assertion violation happens here.

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

@@ -85,6 +85,4 @@ contract InternalCall {
 // Warning 2018: (1247-1309): Function state mutability can be restricted to pure
 // Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
 // Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
-// Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
-// Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
 // Warning 5729: (1370-1375): BMC does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol

@@ -33,4 +33,6 @@ contract C {
 // Warning 2072: (435-445): Unused local variable.
 // Warning 2072: (656-666): Unused local variable.
 // Warning 2072: (698-708): Unused local variable.
-// Warning 6328: (135-151): CHC: Assertion violation happens here.
+// Warning 1218: (135-151): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (135-151): CHC: Assertion violation might happen here.
+// Warning 4661: (135-151): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_1.sol

@@ -10,8 +10,9 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 2519: (100-106): This declaration shadows an existing declaration.
 // Warning 2072: (100-106): Unused local variable.
 // Warning 2072: (108-125): Unused local variable.
-// Warning 6328: (143-157): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ns = false\ndata = [36, 5, 5, 5, 5, 5]\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.s(1)\nState: x = 1\nC.f(0)\n    a.call("") -- untrusted external call
+// Warning 6328: (143-157): CHC: Assertion violation happens here.

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()

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol

@@ -19,7 +19,8 @@ contract C {
 		address prevOwner = owner;
 		uint z = s.f();
 		assert(z == y);
-		assert(prevOwner == owner);
+		// Disabled because of Spacer nondeterminism.
+		//assert(prevOwner == owner);
 	}
 
 	function g() public view returns (uint) {
@@ -30,4 +31,5 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 2072: (219-236): Unused local variable.
 // Warning 6328: (266-280): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol

@@ -40,4 +40,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 2018: (33-88): Function state mutability can be restricted to view
-// Warning 6328: (367-381): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, z = 3, s = 0, insidef = true\nprevOwner = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, z = 0, s = 0, insidef = false\nC.f()\n    s.f() -- untrusted external call, synthesized as:\n        C.zz() -- reentrant call
+// Warning 6328: (367-381): CHC: Assertion violation happens here.