Merge pull request #9834 from ethereum/develop

Merge develop into breaking.

.circleci/build_win.ps1

@@ -0,0 +1,13 @@
+cd "$PSScriptRoot\.."
+
+if ("$Env:FORCE_RELEASE") {
+	New-Item prerelease.txt -type file
+	Write-Host "Building release version."
+}
+
+mkdir build
+cd build
+$boost_dir=(Resolve-Path $PSScriptRoot\..\deps\boost\lib\cmake\Boost-*)
+..\deps\cmake\bin\cmake -G "Visual Studio 16 2019" -DBoost_DIR="$boost_dir\" -DCMAKE_MSVC_RUNTIME_LIBRARY=MultiThreaded -DCMAKE_INSTALL_PREFIX="$PSScriptRoot\..\upload" ..
+msbuild solidity.sln /p:Configuration=Release /m:5 /v:minimal
+..\deps\cmake\bin\cmake --build . -j 5 --target install --config Release

.circleci/config.yml

@@ -27,6 +27,9 @@ parameters:
     type: string
     default: "solbuildpackpusher/solidity-buildpack-deps@sha256:23dad3b34deae8107c8551804ef299f6a89c23ed506e8118fac151e2bdc9018c"
 
+orbs:
+  win: circleci/windows@2.2.0
+
 defaults:
 
   # --------------------------------------------------------------------------
@@ -64,6 +67,10 @@ defaults:
       path: build/solc/solc
       destination: solc
 
+  # windows artifacts
+  - artifact_solc_windows: &artifact_solc_windows
+      path: upload/
+
   # compiled tool executable target
   - artifacts_tools: &artifacts_tools
       path: build/tools/solidity-upgrade
@@ -876,6 +883,35 @@ jobs:
       - run: *gitter_notify_failure
       - run: *gitter_notify_success
 
+  b_win: &b_win
+    executor:
+      name: win/default
+      shell: powershell.exe
+    steps:
+      - checkout
+      - restore_cache:
+          keys:
+            - dependencies-win-{{ checksum "scripts/install_deps.ps1" }}
+      - run:
+          name: "Installing dependencies"
+          command: if ( -not (Test-Path .\deps\boost) ) { .\scripts\install_deps.ps1 }
+      - save_cache:
+          key: dependencies-win-{{ checksum "scripts/install_deps.ps1" }}
+          paths:
+            - .\deps\boost
+            - .\deps\cmake
+      - run:
+          name: "Building solidity"
+          command: .circleci/build_win.ps1
+      - store_artifacts: *artifact_solc_windows
+      - persist_to_workspace: *artifacts_build_dir
+
+  b_win_release:
+    <<: *b_win
+    environment:
+      FORCE_RELEASE: ON
+
+
 workflows:
   version: 2
 
@@ -927,6 +963,10 @@ workflows:
       - t_ems_compile_ext_gnosis: *workflow_emscripten
       - t_ems_compile_ext_zeppelin: *workflow_emscripten
 
+      # Windows build and tests
+      - b_win: *workflow_trigger_on_tags
+      - b_win_release: *workflow_trigger_on_tags
+
   nightly:
 
     triggers:

ReleaseChecklist.md

@@ -25,7 +25,8 @@
  - [ ] Create a pull request from ``develop`` to ``release``, wait for the tests, then merge it.
  - [ ] Make a final check that there are no platform-dependency issues in the ``solidity-test-bytecode`` repository.
  - [ ] Wait for the tests for the commit on ``release``, create a release in Github, creating the tag (click the `PUBLISH RELEASE` button on the release page.)
- - [ ] Wait for the CI runs on the tag itself (travis and appveyor should push artifacts onto the Github release page).
+ - [ ] Wait for the CI runs on the tag itself (travis should push artifacts onto the Github release page).
+ - [ ] Take the ``solc.exe`` binary from the ``b_win_release`` run of the released commit in circle-ci and add it to the release page as ``solc-windows.exe``.
  - [ ] Run ``scripts/create_source_tarball.sh`` while being on the tag to create the source tarball. Make sure to create ``prerelease.txt`` before: (``echo -n > prerelease.txt``). This will create the tarball in a directory called ``upload``.
  - [ ] Take the tarball from the upload directory (its name should be ``solidity_x.x.x.tar.gz``, otherwise ``prerelease.txt`` was missing in the step before) and upload the source tarball to the release page.
 

appveyor.yml

@@ -59,7 +59,7 @@ install:
 before_build:
     - if not exist build mkdir build
     - cd build
-    - cmake -G "Visual Studio 15 2017 Win64" .. -DTESTS=On
+    - cmake -G "Visual Studio 15 2017 Win64" .. -DTESTS=On -DBoost_USE_STATIC_RUNTIME=OFF
 build_script:
     - msbuild solidity.sln /p:Configuration=%CONFIGURATION% /m:%NUMBER_OF_PROCESSORS% /v:minimal
     - cd %APPVEYOR_BUILD_FOLDER%

cmake/EthDependencies.cmake

@@ -25,6 +25,9 @@ set(ETH_SCRIPTS_DIR ${ETH_CMAKE_DIR}/scripts)
 ## use multithreaded boost libraries, with -mt suffix
 set(Boost_USE_MULTITHREADED ON)
 option(Boost_USE_STATIC_LIBS "Link Boost statically" ON)
+if(WIN32)
+	option(Boost_USE_STATIC_RUNTIME "Link Boost against static C++ runtime libraries" ON)
+endif()
 
 set(BOOST_COMPONENTS "filesystem;unit_test_framework;program_options;system")
 

cmake/EthPolicy.cmake

@@ -15,5 +15,9 @@ macro (eth_policy)
 		# do not interpret if() arguments as variables!
 		cmake_policy(SET CMP0054 NEW)
 	endif()
-endmacro()
 
+	if (POLICY CMP0091)
+		# Allow selecting MSVC runtime library using CMAKE_MSVC_RUNTIME_LIBRARY.
+		cmake_policy(SET CMP0091 NEW)
+	endif()
+endmacro()

cmake/jsoncpp.cmake

@@ -34,6 +34,12 @@ if(CMAKE_VERSION VERSION_GREATER 3.1)
     set(byproducts BUILD_BYPRODUCTS "${JSONCPP_LIBRARY}")
 endif()
 
+# Propagate CMAKE_MSVC_RUNTIME_LIBRARY on Windows builds, if set.
+if (WIN32 AND POLICY CMP0091 AND CMAKE_MSVC_RUNTIME_LIBRARY)
+    list(APPEND JSONCPP_CMAKE_ARGS "-DCMAKE_POLICY_DEFAULT_CMP0091:STRING=NEW")
+    list(APPEND JSONCPP_CMAKE_ARGS "-DCMAKE_MSVC_RUNTIME_LIBRARY=${CMAKE_MSVC_RUNTIME_LIBRARY}")
+endif()
+
 ExternalProject_Add(jsoncpp-project
     PREFIX "${prefix}"
     DOWNLOAD_DIR "${CMAKE_SOURCE_DIR}/deps/downloads"
@@ -51,6 +57,7 @@ ExternalProject_Add(jsoncpp-project
                -DJSONCPP_WITH_PKGCONFIG_SUPPORT=OFF
                -DCMAKE_CXX_FLAGS=${JSONCPP_CXX_FLAGS}
                -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE}
+               ${JSONCPP_CMAKE_ARGS}
     ${byproducts}
 )
 

docs/brand-guide.rst

@@ -70,6 +70,8 @@ Solidity Logo Guidelines
 .. image:: logo.svg
   :width: 256
 
+*(Right click on the logo to download it.)*
+
 Please do not:
 
 - Change the ratio of the logo (do not stretch it or cut it).

docs/contributing.rst

@@ -2,22 +2,25 @@
 Contributing
 ############
 
-Help is always appreciated!
+Help is always welcome and there are plenty of options how you can contribute to Solidity.
 
-To get started, you can try :ref:`building-from-source` in order to familiarize
+In particular, we appreciate support in the following areas:
-yourself with the components of Solidity and the build process. Also, it may be
-useful to become well-versed at writing smart-contracts in Solidity.
 
-In particular, we need help in the following areas:
+* Reporting issues.
-
-* Improving the documentation
-* Responding to questions from other users on `StackExchange
-  <https://ethereum.stackexchange.com>`_ and the `Solidity Gitter
-  <https://gitter.im/ethereum/solidity>`_
 * Fixing and responding to `Solidity's GitHub issues
   <https://github.com/ethereum/solidity/issues>`_, especially those tagged as
   `good first issue <https://github.com/ethereum/solidity/labels/good%20first%20issue>`_ which are
   meant as introductory issues for external contributors.
+* Improving the documentation.
+* Translating the documentation into more languages.
+* Responding to questions from other users on `StackExchange
+  <https://ethereum.stackexchange.com>`_ and the `Solidity Gitter Chat
+  <https://gitter.im/ethereum/solidity>`_.
+* Getting involved in the language design process by joining language design calls, proposing language changes or new features and providing feedback.
+
+To get started, you can try :ref:`building-from-source` in order to familiarize
+yourself with the components of Solidity and the build process. Also, it may be
+useful to become well-versed at writing smart-contracts in Solidity.
 
 Please note that this project is released with a `Contributor Code of Conduct <https://raw.githubusercontent.com/ethereum/solidity/develop/CODE_OF_CONDUCT.md>`_. By participating in this project - in the issues, pull requests, or Gitter channels - you agree to abide by its terms.
 
@@ -27,8 +30,8 @@ Team Calls
 If you have issues or pull requests to discuss, or are interested in hearing what
 the team and contributors are working on, you can join our public team calls:
 
-- Mondays at 12pm CET/CEST
+- Mondays at 12pm CET/CEST.
-- Wednesdays at 2pm CET/CEST
+- Wednesdays at 2pm CET/CEST.
 
 Both calls take place on `Google Meet <https://meet.google.com/mrq-kbwv-edg>`_.
 
@@ -39,12 +42,12 @@ To report an issue, please use the
 `GitHub issues tracker <https://github.com/ethereum/solidity/issues>`_. When
 reporting issues, please mention the following details:
 
-* Which version of Solidity you are using
+* Which version of Solidity you are using.
-* What was the source code (if applicable)
+* What was the source code (if applicable).
-* Which platform are you running on
+* Which platform are you running on.
-* How to reproduce the issue
+* How to reproduce the issue.
-* What was the result of the issue
+* What was the result of the issue.
-* What the expected behaviour is
+* What the expected behaviour is.
 
 Reducing the source code that caused the issue to a bare minimum is always
 very helpful and sometimes even clarifies a misunderstanding.
@@ -66,7 +69,7 @@ test cases under ``test/`` (see below).
 
 However, if you are making a larger change, please consult with the `Solidity Development Gitter channel
 <https://gitter.im/ethereum/solidity-dev>`_ (different from the one mentioned above, this one is
-focused on compiler and language development instead of language use) first.
+focused on compiler and language development instead of language usage) first.
 
 New features and bugfixes should be added to the ``Changelog.md`` file: please
 follow the style of previous entries, when applicable.
@@ -78,7 +81,7 @@ ensure that it builds locally before submitting a pull request.
 
 Thank you for your help!
 
-Running the compiler tests
+Running the Compiler Tests
 ==========================
 
 Prerequisites
@@ -91,7 +94,7 @@ in the current directory, installed on the system level, or the ``deps`` folder
 in the project top level. The required file is called ``libevmone.so`` on Linux
 systems, ``evmone.dll`` on Windows systems and ``libevmone.dylib`` on macOS.
 
-Running the tests
+Running the Tests
 -----------------
 
 Solidity includes different types of tests, most of them bundled into the
@@ -155,7 +158,7 @@ you have access to functions and variables in which you can break or print with.
 The CI runs additional tests (including ``solc-js`` and testing third party Solidity
 frameworks) that require compiling the Emscripten target.
 
-Writing and running syntax tests
+Writing and Running Syntax Tests
 --------------------------------
 
 Syntax tests check that the compiler generates the correct error messages for invalid code
@@ -366,7 +369,7 @@ the string parameter ``name`` is non-empty.
 Documentation Style Guide
 =========================
 
-The following are style recommendations specifically for documentation
+In the following section you find style recommendations specifically focusing on documentation
 contributions to Solidity.
 
 English Language
@@ -394,10 +397,10 @@ title.
 
 For example, the following are all correct:
 
-* Title Case for Headings
+* Title Case for Headings.
-* For Headings Use Title Case
+* For Headings Use Title Case.
-* Local and State Variable Names
+* Local and State Variable Names.
-* Order of Layout
+* Order of Layout.
 
 Expand Contractions
 -------------------
@@ -450,3 +453,21 @@ Running Documentation Tests
 
 Make sure your contributions pass our documentation tests by running ``./scripts/docs.sh`` that installs dependencies
 needed for documentation and checks for any problems such as broken links or syntax issues.
+
+Solidity Language Design
+========================
+
+If you want to get involved in the language design process and share your ideas, please join the `solidity-users forum <https://groups.google.com/g/solidity-users>`_,
+where existing properties of the language and proposals for new features can be discussed.
+
+We regularly host language design discussion calls, in which selected topics, issues or feature implementations are debated in detail. The invitation
+to those calls is shared via the aforementioned forum. We are also sharing feedback surveys and other language design relevant content in this forum.
+
+For ad-hoc cases and questions you can reach out to us via the `Solidity-dev Gitter channel <https://gitter.im/ethereum/solidity-dev>`_, a
+dedicated chatroom for conversations around the Solidity compiler and language development.
+
+You can follow the implementation status of new features in the `Solidity Github project <https://github.com/ethereum/solidity/projects/43>`_.
+Issues in the design backlog need further specification and will either be discussed in a language design call or in a regular team call. You can
+see the upcoming changes for the next breaking release by changing from the default branch (`develop`) to the `breaking branch <https://github.com/ethereum/solidity/tree/breaking>`_.
+
+We are happy to hear your thoughts on how we can improve the language design process to be even more collaborative and transparent.

docs/installing-solidity.rst

@@ -230,7 +230,7 @@ The following C++ compilers and their minimum versions can build the Solidity co
 
 - `GCC <https://gcc.gnu.org>`_, version 5+
 - `Clang <https://clang.llvm.org/>`_, version 3.4+
-- `MSVC <https://docs.microsoft.com/en-us/cpp/?view=vs-2019>`_, version 2017+
+- `MSVC <https://visualstudio.microsoft.com/vs/>`_, version 2019+
 
 Prerequisites - macOS
 ---------------------
@@ -262,29 +262,29 @@ You need to install the following dependencies for Windows builds of Solidity:
 +-----------------------------------+-------------------------------------------------------+
 | Software                          | Notes                                                 |
 +===================================+=======================================================+
-| `Visual Studio 2017 Build Tools`_ | C++ compiler                                          |
+| `Visual Studio 2019 Build Tools`_ | C++ compiler                                          |
 +-----------------------------------+-------------------------------------------------------+
-| `Visual Studio 2017`_  (Optional) | C++ compiler and dev environment.                     |
+| `Visual Studio 2019`_  (Optional) | C++ compiler and dev environment.                     |
 +-----------------------------------+-------------------------------------------------------+
 
 If you already have one IDE and only need the compiler and libraries,
-you could install Visual Studio 2017 Build Tools.
+you could install Visual Studio 2019 Build Tools.
 
-Visual Studio 2017 provides both IDE and necessary compiler and libraries.
+Visual Studio 2019 provides both IDE and necessary compiler and libraries.
-So if you have not got an IDE and prefer to develop solidity, Visual Studio 2017
+So if you have not got an IDE and prefer to develop solidity, Visual Studio 2019
 may be a choice for you to get everything setup easily.
 
 Here is the list of components that should be installed
-in Visual Studio 2017 Build Tools or Visual Studio 2017:
+in Visual Studio 2019 Build Tools or Visual Studio 2019:
 
 * Visual Studio C++ core features
-* VC++ 2017 v141 toolset (x86,x64)
+* VC++ 2019 v141 toolset (x86,x64)
 * Windows Universal CRT SDK
 * Windows 8.1 SDK
 * C++/CLI support
 
-.. _Visual Studio 2017: https://www.visualstudio.com/vs/
+.. _Visual Studio 2019: https://www.visualstudio.com/vs/
-.. _Visual Studio 2017 Build Tools: https://www.visualstudio.com/downloads/#build-tools-for-visual-studio-2017
+.. _Visual Studio 2019 Build Tools: https://www.visualstudio.com/downloads/#build-tools-for-visual-studio-2019
 
 Dependencies Helper Script
 --------------------------
@@ -300,7 +300,10 @@ Or, on Windows:
 
 .. code-block:: bat
 
-    scripts\install_deps.bat
+    scripts\install_deps.ps1
+
+Note that the latter command will install ``boost`` and ``cmake`` to the ``deps`` subdirectory, while the former command
+will attempt to install the dependencies globally.
 
 Clone the Repository
 --------------------
@@ -362,11 +365,14 @@ And for Windows:
 
     mkdir build
     cd build
-    cmake -G "Visual Studio 15 2017 Win64" ..
+    cmake -G "Visual Studio 16 2019 Win64" ..
 
-This latter set of instructions should result in the creation of
+In case you want to use the version of boost installed by ``./scripts/install_deps.ps1``, you will
-**solidity.sln** in that build directory.  Double-clicking on that file
+additionally need to pass ``-DBoost_DIR="..\deps\boost\lib\cmake\Boost-*"`` and ``-DCMAKE_MSVC_RUNTIME_LIBRARY=MultiThreaded``
-should result in Visual Studio firing up.  We suggest building
+as arguments to the call to ``cmake``.
+
+This should result in the creation of **solidity.sln** in that build directory.
+Double-clicking on that file should result in Visual Studio firing up.  We suggest building
 **Release** configuration, but all others work.
 
 Alternatively, you can build for Windows on the command-line, like so:

libsmtutil/Helpers.h

@@ -25,7 +25,7 @@ namespace solidity::smtutil
 
 /// Signed division in SMTLIB2 rounds differently than EVM.
 /// This does not check for division by zero!
-inline Expression signedDivision(Expression _left, Expression _right)
+inline Expression signedDivisionEVM(Expression _left, Expression _right)
 {
 	return Expression::ite(
 		_left >= 0,
@@ -42,7 +42,7 @@ inline Expression abs(Expression _value)
 /// Signed modulo in SMTLIB2 behaves differently with regards
 /// to the sign than EVM.
 /// This does not check for modulo by zero!
-inline Expression signedModulo(Expression _left, Expression _right)
+inline Expression signedModuloEVM(Expression _left, Expression _right)
 {
 	return Expression::ite(
 		_left >= 0,

libsolidity/formal/SMTEncoder.cpp

@@ -1506,7 +1506,7 @@ smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Exp
 {
 	// Signed division in SMTLIB2 rounds differently for negative division.
 	if (_type.isSigned())
-		return signedDivision(_left, _right);
+		return signedDivisionEVM(_left, _right);
 	else
 		return _left / _right;
 }

libyul/optimiser/ReasoningBasedSimplifier.cpp

@@ -176,12 +176,11 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
 			// No `wrap()` needed here, because -2**255 / -1 results
 			// in 2**255 which is "converted" to its two's complement
 			// representation 2**255 in `signedToUnsigned`
-			signedToUnsigned(smtutil::signedDivision(
+			signedToUnsigned(smtutil::signedDivisionEVM(
 				unsignedToSigned(arguments.at(0)),
 				unsignedToSigned(arguments.at(1))
 			))
 		);
-		break;
 	case evmasm::Instruction::MOD:
 		return smtutil::Expression::ite(
 			arguments.at(1) == constantValue(0),
@@ -192,12 +191,11 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
 		return smtutil::Expression::ite(
 			arguments.at(1) == constantValue(0),
 			constantValue(0),
-			signedToUnsigned(signedModulo(
+			signedToUnsigned(signedModuloEVM(
 				unsignedToSigned(arguments.at(0)),
 				unsignedToSigned(arguments.at(1))
 			))
 		);
-		break;
 	case evmasm::Instruction::LT:
 		return booleanValue(arguments.at(0) < arguments.at(1));
 	case evmasm::Instruction::SLT:

scripts/install_deps.ps1

@@ -0,0 +1,15 @@
+# Needed for Invoke-WebRequest to work via CI.
+$progressPreference = "silentlyContinue"
+
+New-Item -ItemType Directory -Force -Path "$PSScriptRoot\..\deps"
+
+Invoke-WebRequest -URI "https://github.com/Kitware/CMake/releases/download/v3.18.2/cmake-3.18.2-win64-x64.zip" -OutFile cmake.zip
+tar -xf cmake.zip
+mv cmake-3.18.2-win64-x64 "$PSScriptRoot\..\deps\cmake"
+
+Invoke-WebRequest -URI "https://dl.bintray.com/boostorg/release/1.74.0/source/boost_1_74_0.zip" -OutFile boost.zip
+tar -xf boost.zip
+cd boost_1_74_0
+.\bootstrap.bat
+.\b2 -j4 -d0 link=static runtime-link=static variant=release threading=multi address-model=64 --with-filesystem --with-system --with-program_options --with-test --prefix="$PSScriptRoot\..\deps\boost" install
+cd ..

scripts/release.bat

@@ -1,38 +0,0 @@
-@ECHO OFF
-
-REM ---------------------------------------------------------------------------
-REM Batch file for implementing release flow for solidity for Windows.
-REM
-REM The documentation for solidity is hosted at:
-REM
-REM     https://solidity.readthedocs.org
-REM
-REM ---------------------------------------------------------------------------
-REM This file is part of solidity.
-REM
-REM solidity is free software: you can redistribute it and/or modify
-REM it under the terms of the GNU General Public License as published by
-REM the Free Software Foundation, either version 3 of the License, or
-REM (at your option) any later version.
-REM
-REM solidity is distributed in the hope that it will be useful,
-REM but WITHOUT ANY WARRANTY; without even the implied warranty of
-REM MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-REM GNU General Public License for more details.
-REM
-REM You should have received a copy of the GNU General Public License
-REM along with solidity.  If not, see <http://www.gnu.org/licenses/>
-REM
-REM Copyright (c) 2016 solidity contributors.
-REM ---------------------------------------------------------------------------
-
-set CONFIGURATION=%1
-set VERSION=%2
-
-set "DLLS=MSVC_DLLS_NOT_FOUND"
-FOR /d %%d IN ("C:\Program Files (x86)\Microsoft Visual Studio\2017\BuildTools\VC\Redist\MSVC\*"
-    "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Redist\MSVC\*") DO set "DLLS=%%d\x86\Microsoft.VC141.CRT\msvc*.dll"
-
-7z a solidity-windows.zip ^
-    .\build\solc\%CONFIGURATION%\solc.exe .\build\test\%CONFIGURATION%\soltest.exe ^
-    "%DLLS%"

test/formal/exp_to_shl.py

@@ -0,0 +1,34 @@
+from rule import Rule
+from opcodes import *
+from util import *
+
+"""
+Checking conversion of exp(2, X) to shl(X, 1)
+"""
+
+rule = Rule()
+n_bits = 256
+
+# Proof of exp(2, X) = shl(X, 1) by induction:
+#
+# Base case: X = 0, exp(2, 0) = 1 = 1 = shl(0, 1)
+# Inductive step: assuming exp(2, X) = shl(X, 1) for X <= N
+#                 to prove: exp(2, N + 1) = shl(N + 1, 1)
+#
+# Notice that exp(2, N + 1) = 2 * exp(2, N) mod 2**256
+# since exp(2, N) = shl(N, 1), it is enough to show that
+# 2 * shl(N, 1) mod 2**256 = shl(N + 1, 1)
+#
+# Also note that N + 1 < 2**256
+
+N = BitVec('N', n_bits)
+inductive_step = 2 * SHL(N, 1)
+
+rule.check(
+    inductive_step,
+    If(
+        N == 2**256 - 1,
+        0,
+        SHL(N + 1, 1)
+    )
+)

test/libyul/YulOptimizerTest.cpp

@@ -103,7 +103,10 @@ YulOptimizerTest::YulOptimizerTest(string const& _filename):
 		BOOST_THROW_EXCEPTION(runtime_error("Filename path has to contain a directory: \"" + _filename + "\"."));
 	m_optimizerStep = std::prev(std::prev(path.end()))->string();
 
-	if (m_optimizerStep == "reasoningBasedSimplifier" && solidity::test::CommonOptions::get().disableSMT)
+	if (m_optimizerStep == "reasoningBasedSimplifier" && (
+		solidity::test::CommonOptions::get().disableSMT ||
+		ReasoningBasedSimplifier::invalidInCurrentEnvironment()
+	))
 		m_shouldRun = false;
 
 	m_source = m_reader.source();