From 3217b6a8c612c60fa21fa80ba11349826756669c Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Mon, 19 Oct 2020 17:54:20 +0200
Subject: [PATCH 01/10] Build release build on tags.

---
 scripts/travis-emscripten/build_emscripten.sh | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/scripts/travis-emscripten/build_emscripten.sh b/scripts/travis-emscripten/build_emscripten.sh
index 3162e13b6..e40ba3a89 100755
--- a/scripts/travis-emscripten/build_emscripten.sh
+++ b/scripts/travis-emscripten/build_emscripten.sh
@@ -42,8 +42,18 @@ fi
 
 WORKSPACE=/root/project
 
-echo -en 'travis_fold:start:compiling_solidity\\r'
 cd $WORKSPACE
+
+# shellcheck disable=SC2166
+if [[ "$CIRCLE_BRANCH" = release || -n "$CIRCLE_TAG" || -n "$FORCE_RELEASE" || "$(git tag --points-at HEAD 2>/dev/null)" == v* ]]
+then
+  echo -n >prerelease.txt
+fi
+if [ -n "$CIRCLE_SHA1" ]
+then
+  echo -n "$CIRCLE_SHA1" >commit_hash.txt
+fi
+
 mkdir -p $BUILD_DIR
 cd $BUILD_DIR
 cmake \
@@ -67,5 +77,3 @@ cp $BUILD_DIR/libsolc/soljson.js ./
 OUTPUT_SIZE=`ls -la soljson.js`
 
 echo "Emscripten output size: $OUTPUT_SIZE"
-
-echo -en 'travis_fold:end:compiling_solidity\\r'

From 3654dccb965e59d6c3cb26acc1fbe9498837906a Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Mon, 19 Oct 2020 17:57:22 +0200
Subject: [PATCH 02/10] Disable travis.

---
 .circleci/config.yml                          |   2 +-
 .travis.yml                                   | 250 ------------------
 scripts/build_emscripten.sh                   |   2 +-
 scripts/chk_shellscripts/ignore.txt           |   4 +-
 .../build_emscripten.sh                       |   0
 scripts/docker_build.sh                       |  12 -
 scripts/docker_deploy.sh                      |  29 --
 scripts/release_emscripten.sh                 |  33 ---
 scripts/travis-emscripten/deploy_key.enc      | Bin 1680 -> 0 bytes
 scripts/travis-emscripten/publish_binary.sh   |  99 -------
 .../docker-scripts/rebuild_current.sh         |   2 +-
 11 files changed, 4 insertions(+), 429 deletions(-)
 delete mode 100644 .travis.yml
 rename scripts/{travis-emscripten => ci}/build_emscripten.sh (100%)
 delete mode 100755 scripts/docker_build.sh
 delete mode 100755 scripts/docker_deploy.sh
 delete mode 100755 scripts/release_emscripten.sh
 delete mode 100644 scripts/travis-emscripten/deploy_key.enc
 delete mode 100755 scripts/travis-emscripten/publish_binary.sh

diff --git a/.circleci/config.yml b/.circleci/config.yml
index f939586ae..ee85d2e25 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -657,7 +657,7 @@ jobs:
       - run:
           name: Build
           command: |
-            scripts/travis-emscripten/build_emscripten.sh
+            scripts/ci/build_emscripten.sh
       - store_artifacts:
           path: emscripten_build/libsolc/soljson.js
           destination: soljson.js
diff --git a/.travis.yml b/.travis.yml
deleted file mode 100644
index f9105e246..000000000
--- a/.travis.yml
+++ /dev/null
@@ -1,250 +0,0 @@
-#------------------------------------------------------------------------------
-# TravisCI configuration file for solidity.
-#
-# The documentation for solidity is hosted at:
-#
-# http://solidity.readthedocs.org
-#
-# ------------------------------------------------------------------------------
-# This file is part of solidity.
-#
-# solidity is free software: you can redistribute it and/or modify
-# it under the terms of the GNU General Public License as published by
-# the Free Software Foundation, either version 3 of the License, or
-# (at your option) any later version.
-#
-# solidity is distributed in the hope that it will be useful,
-# but WITHOUT ANY WARRANTY; without even the implied warranty of
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-# GNU General Public License for more details.
-#
-# You should have received a copy of the GNU General Public License
-# along with solidity.  If not, see <http://www.gnu.org/licenses/>
-#
-# (c) 2016-2017 solidity contributors.
-#------------------------------------------------------------------------------
-
-language: cpp
-
-branches:
-    # We need to whitelist the branches which we want to have "push" automation,
-    # this includes tags (which are treated as branches by travis).
-    # Pull request automation is not constrained to this set of branches.
-    only:
-        - develop
-        - release
-        - /^v[0-9]/
-
-env:
-    global:
-        - ENCRYPTION_LABEL="6d4541b72666"
-        - SOLC_BUILD_TYPE=RelWithDebInfo
-        - SOLC_EMSCRIPTEN=Off
-        # FIXME: Pushing solcjson.js to solc-bin disabled until we fix the cause of #9261
-        - SOLC_PUBLISH_EMSCRIPTEN=Off
-        - SOLC_INSTALL_DEPS_TRAVIS=On
-        - SOLC_RELEASE=On
-        - SOLC_TESTS=On
-        - SOLC_STOREBYTECODE=Off
-        - SOLC_DOCKER=Off
-        - MAKEFLAGS="-j 4"
-
-matrix:
-    include:
-        - os: linux
-          dist: trusty
-          sudo: required
-          compiler: gcc
-          env:
-              - ZIP_SUFFIX=ubuntu-trusty
-              - SOLC_STOREBYTECODE=On
-          before_install:
-              - sudo add-apt-repository -y ppa:ubuntu-toolchain-r/test
-              - sudo add-apt-repository -y ppa:mhier/libboost-latest
-              - sudo apt-get update -qq
-          install:
-              - sudo apt-get install -qq g++-8 gcc-8
-              - sudo apt-get install -qq libboost1.67-dev
-              - sudo apt-get install -qq libleveldb1
-              - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-8 90
-              - sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-8 90
-
-        - os: linux
-          dist: trusty
-          sudo: required
-          compiler: clang
-          env:
-              - ZIP_SUFFIX=ubuntu-trusty-clang
-              - SOLC_STOREBYTECODE=On
-          before_install:
-              - sudo add-apt-repository -y ppa:ubuntu-toolchain-r/test
-              - sudo add-apt-repository -y ppa:mhier/libboost-latest
-              - sudo apt-get update -qq
-          install:
-              - sudo apt-get install -qq g++-8 gcc-8
-              - sudo apt-get install -qq libboost1.67-dev
-              - sudo apt-get install -qq libleveldb1
-              - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-8 90
-              - sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-8 90
-
-        # Docker target, which generates a statically linked alpine image
-        - os: linux
-          dist: trusty
-          sudo: required
-          services:
-            - docker
-          env:
-            - SOLC_DOCKER=On
-            - SOLC_INSTALL_DEPS_TRAVIS=Off
-            - SOLC_RELEASE=Off
-            - SOLC_TESTS=Off
-
-        # Emscripten target, which compiles 'solc' to javascript and uploads the resulting .js
-        # files to https://github.com/ethereum/solc-bin.  These binaries are used in Browser-Solidity
-        # and in other Ethereum web-based development contexts.
-        - os: linux
-          dist: trusty
-          sudo: required
-          compiler: gcc
-          node_js:
-            - "10"
-          services:
-              - docker
-          before_install:
-              - nvm install 10
-              - nvm use 10
-              - docker pull solbuildpackpusher/solidity-buildpack-deps@sha256:23dad3b34deae8107c8551804ef299f6a89c23ed506e8118fac151e2bdc9018c
-          env:
-              - SOLC_EMSCRIPTEN=On
-              - SOLC_INSTALL_DEPS_TRAVIS=Off
-              - SOLC_RELEASE=Off
-              - SOLC_TESTS=Off
-              - ZIP_SUFFIX=emscripten
-              - SOLC_STOREBYTECODE=On
-              # Travis doesn't seem to support "dynamic" cache keys where we could include
-              # the hashes of certain files. Our CircleCI configuration contains the hash of
-              # relevant emscripten files.
-              #
-              # It is important to invalidate the cache with each emscripten update, because
-              # dependencies, such as boost, might be broken otherwise.
-              #
-              # This key here has no significant on anything, apart from caching. Please keep
-              # it in sync with the version above.
-              - EMSCRIPTEN_VERSION_KEY="1.39.3"
-
-        # OS X Mavericks (10.9)
-        # https://en.wikipedia.org/wiki/OS_X_Mavericks
-        #
-# Disabled because of problems on travis.
-#        - os: osx
-#          osx_image: beta-xcode6.2
-#          env:
-#              - ZIP_SUFFIX=osx-mavericks
-
-        # OS X Yosemite (10.10)
-        # https://en.wikipedia.org/wiki/OS_X_Yosemite
-        #
-#        - os: osx
-#          osx_image: xcode7.1
-#          env:
-#              # Workaround for "macOS - Yosemite, El Capitan and Sierra hanging?"
-#              # https://github.com/ethereum/solidity/issues/894
-#              - SOLC_TESTS=Off
-#              - ZIP_SUFFIX=osx-yosemite
-
-        # OS X El Capitan (10.11)
-        # https://en.wikipedia.org/wiki/OS_X_El_Capitan
-        #
-#        - os: osx
-#          osx_image: xcode7.3
-#          env:
-#              # The use of Debug config here ONLY for El Capitan is a workaround for "The Heisenbug"
-#              # See https://github.com/ethereum/webthree-umbrella/issues/565
-#              - SOLC_BUILD_TYPE=Debug
-#              # Workaround for "macOS - Yosemite, El Capitan and Sierra hanging?"
-#              # https://github.com/ethereum/solidity/issues/894
-#              - SOLC_TESTS=Off
-#              - ZIP_SUFFIX=osx-elcapitan
-
-        # macOS Sierra (10.12)
-        # https://en.wikipedia.org/wiki/MacOS_Sierra
-        #
-#       - os: osx
-#          osx_image: xcode8
-#          env:
-#              # Look like "The Heisenbug" is occurring here too, so we'll do the same workaround.
-#              # See https://travis-ci.org/ethereum/solidity/jobs/150240930
-#              - SOLC_BUILD_TYPE=Debug
-#              # Workaround for "macOS - Yosemite, El Capitan and Sierra hanging?"
-#              # https://github.com/ethereum/solidity/issues/894
-#              - SOLC_TESTS=Off
-#              - ZIP_SUFFIX=macos-sierra
-
-git:
-    depth: 2
-
-cache:
-    ccache: true
-    directories:
-        - boost_1_70_0_install
-        - $HOME/.local
-
-install:
-    - test $SOLC_INSTALL_DEPS_TRAVIS != On || (scripts/install_deps.sh)
-    - test "$TRAVIS_OS_NAME" != "linux" || (sudo scripts/install_cmake.sh)
-
-before_script:
-    # Disable tests unless run on the release branch, on tags or with daily cron
-    - if [ "$TRAVIS_BRANCH" != release -a -z "$TRAVIS_TAG" -a "$TRAVIS_EVENT_TYPE" != cron ]; then SOLC_TESTS=Off; fi
-    - if [ "$TRAVIS_BRANCH" = release -o -n "$TRAVIS_TAG" ]; then echo -n > prerelease.txt; else date -u +"nightly.%Y.%-m.%-d" > prerelease.txt; fi
-    - echo -n "$TRAVIS_COMMIT" > commit_hash.txt
-    - test $SOLC_EMSCRIPTEN != On || (scripts/build_emscripten.sh)
-    - test $SOLC_DOCKER != On || (scripts/docker_build.sh)
-    - test $SOLC_RELEASE != On || (scripts/build.sh $SOLC_BUILD_TYPE -DBoost_USE_STATIC_LIBS=OFF && scripts/create_source_tarball.sh)
-
-script:
-    - test $SOLC_EMSCRIPTEN != On -o $SOLC_TESTS != On || (scripts/test_emscripten.sh)
-    - test $SOLC_TESTS != On || (cd $TRAVIS_BUILD_DIR && scripts/tests.sh)
-    - test $SOLC_STOREBYTECODE != On || (cd $TRAVIS_BUILD_DIR && scripts/bytecodecompare/storebytecode.sh)
-
-deploy:
-    # This is the deploy target for the Emscripten build.
-    # It publishes the JS file which was compiled as part of the earlier 'build_emscripten.sh'
-    # step to https://github.com/ethereum/solc-bin/tree/gh-pages/bin.
-    # Both the build and deploy steps for Emscripten are only run within the Ubuntu
-    # configurations (not for macOS).  That is controlled by conditionals within the bash
-    # scripts because TravisCI doesn't provide much in the way of conditional logic.
-
-    - provider: script
-      script: test $SOLC_PUBLISH_EMSCRIPTEN != On || $SOLC_EMSCRIPTEN != On || (scripts/release_emscripten.sh)
-      skip_cleanup: true
-      on:
-          branch:
-            - develop
-            - release
-    # This is the deploy target for the dockerfile. If we are pushing into a develop branch, it will be tagged
-    # as a nightly and appended the commit of the branch it was pushed in. If we are pushing to master it will
-    # be tagged as "stable" and given the version tag as well.
-    - provider: script
-      script: test $SOLC_DOCKER != On || (scripts/docker_deploy.sh)
-      skip_cleanup: true
-      on:
-          branch:
-            - develop
-            - release
-            - /^v\d/
-    # This is the deploy target for the native build (Linux and macOS)
-    # which generates the source tarball.
-    #
-    # This runs for each tag that is created and adds the corresponding files.
-    - provider: releases
-      api_key:
-          secure: PWH37xVBCF0XiSjl+eH7XIdkrfxZXjzvqF4PiBOnD3VnFz+odrdnIwBmCeBYTHTWF8efpp8fmzWJk2UVq1JcpyZiC+SVxO8dx91W2ia1a+wKrEQuDgkUrZBkl5IQNCv0QS81DDQhliyZEaYh8wHO/7RReyMpGpw2U2u85WkFiZ+LdlHEZPfzUeh9lxQ9n8qwFL8Rja+Q05d4cQ8zaVEtofJJT4T6DUWhc3TzuxDYxOmjwg37rC9CkGSLn6VadSh8b3j5R0SZupFsAEvBL/imBLP9r9ewoo7o4p6By3jwiIgH9yNg7LM618xbffcNaYF/KtLBi9uPHfqF7hRD4PlECz+D0PR78nQItOX5HKm1QMg5kCnghRVCA0IVjpV5fiYQnMLM7dCRv34I5b3zLpa69wQ/GLYB2FViqNUfvPeiZTEeIJ2OmATlFx8AH2JoqpY1XJknWb35+vMfa8LSiJJW++SLWeV+ncC92hrvyZ1cy3trepRRZIfyYepxHifnfdWMkddQUJk5b2WS5Fy/TJLZNPeombnpvRhUC38dsYItarKeXTc6k4oADCEDZ2rgGIcEiqRxXV11Y5xHJekLDWzUs+YJNcCuL4pnAP//LOnbnH2w9rLpwhQYSl0anCd097NivAXQJXO2JI/byIYz1kiCVQWnW6EM8+72mLOklf/Qr8k=
-
-      overwrite: true
-      file_glob: true
-      file: $TRAVIS_BUILD_DIR/upload/*
-      skip_cleanup: true
-      on:
-          all_branches: true
-          tags: true
diff --git a/scripts/build_emscripten.sh b/scripts/build_emscripten.sh
index cdb07bfb4..c1845b1c6 100755
--- a/scripts/build_emscripten.sh
+++ b/scripts/build_emscripten.sh
@@ -36,4 +36,4 @@ fi
 
 docker run -v $(pwd):/root/project -w /root/project \
     solbuildpackpusher/solidity-buildpack-deps@sha256:23dad3b34deae8107c8551804ef299f6a89c23ed506e8118fac151e2bdc9018c\
-    ./scripts/travis-emscripten/build_emscripten.sh $BUILD_DIR
+    ./scripts/ci/build_emscripten.sh $BUILD_DIR
diff --git a/scripts/chk_shellscripts/ignore.txt b/scripts/chk_shellscripts/ignore.txt
index 098607764..220ed9f57 100644
--- a/scripts/chk_shellscripts/ignore.txt
+++ b/scripts/chk_shellscripts/ignore.txt
@@ -17,9 +17,7 @@
 ./scripts/wasm-rebuild/docker-scripts/patch.sh
 ./scripts/wasm-rebuild/rebuild.sh
 ./scripts/build_emscripten.sh
-./scripts/travis-emscripten/build_emscripten.sh
-./scripts/travis-emscripten/install_deps.sh
-./scripts/travis-emscripten/publish_binary.sh
+./scripts/ci/build_emscripten.sh
 ./scripts/docker_build.sh
 ./scripts/docs_version_pragma_check.sh
 ./scripts/uniqueErrors.sh
diff --git a/scripts/travis-emscripten/build_emscripten.sh b/scripts/ci/build_emscripten.sh
similarity index 100%
rename from scripts/travis-emscripten/build_emscripten.sh
rename to scripts/ci/build_emscripten.sh
diff --git a/scripts/docker_build.sh b/scripts/docker_build.sh
deleted file mode 100755
index 9eedec344..000000000
--- a/scripts/docker_build.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/usr/bin/env sh
-
-set -e
-
-# Scratch image
-docker build -t ethereum/solc:build -f scripts/Dockerfile .
-tmp_container=$(docker create ethereum/solc:build sh)
-mkdir -p upload
-docker cp ${tmp_container}:/usr/bin/solc upload/solc-static-linux
-
-# Alpine image
-docker build -t ethereum/solc:build-alpine -f scripts/Dockerfile_alpine .
diff --git a/scripts/docker_deploy.sh b/scripts/docker_deploy.sh
deleted file mode 100755
index 4672accce..000000000
--- a/scripts/docker_deploy.sh
+++ /dev/null
@@ -1,29 +0,0 @@
-#!/usr/bin/env sh
-
-set -e
-
-image="ethereum/solc"
-
-tag_and_push()
-{
-    docker tag "$image:$1" "$image:$2"
-    docker push "$image:$2"
-}
-
-echo "$DOCKER_PASSWORD" | docker login -u "$DOCKER_USERNAME" --password-stdin
-version=$($(dirname "$0")/get_version.sh)
-if [ "$TRAVIS_BRANCH" = "develop" ]
-then
-    tag_and_push build nightly
-    tag_and_push build nightly-"$version"-"$TRAVIS_COMMIT"
-    tag_and_push build-alpine nightly-alpine
-    tag_and_push build-alpine nightly-alpine-"$version"-"$TRAVIS_COMMIT"
-elif [ "$TRAVIS_TAG" = v"$version" ]
-then
-    tag_and_push build stable
-    tag_and_push build "$version"
-    tag_and_push build-alpine stable-alpine
-    tag_and_push build-alpine "$version"-alpine
-else
-    echo "Not publishing docker image from branch $TRAVIS_BRANCH or tag $TRAVIS_TAG"
-fi
diff --git a/scripts/release_emscripten.sh b/scripts/release_emscripten.sh
deleted file mode 100755
index 8db9a0494..000000000
--- a/scripts/release_emscripten.sh
+++ /dev/null
@@ -1,33 +0,0 @@
-#!/usr/bin/env bash
-
-#------------------------------------------------------------------------------
-# Bash script which calls the Emscripten "publish binary" script on Ubuntu
-# and does nothing on macOS.  We should probably merge these two scripts in
-# the near future.
-#
-# The documentation for solidity is hosted at:
-#
-#     https://solidity.readthedocs.org
-#
-# ------------------------------------------------------------------------------
-# This file is part of solidity.
-#
-# solidity is free software: you can redistribute it and/or modify
-# it under the terms of the GNU General Public License as published by
-# the Free Software Foundation, either version 3 of the License, or
-# (at your option) any later version.
-#
-# solidity is distributed in the hope that it will be useful,
-# but WITHOUT ANY WARRANTY; without even the implied warranty of
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-# GNU General Public License for more details.
-#
-# You should have received a copy of the GNU General Public License
-# along with solidity.  If not, see <http://www.gnu.org/licenses/>
-#
-# (c) 2016 solidity contributors.
-#------------------------------------------------------------------------------
-
-if [[ "$OSTYPE" != "darwin"* ]]; then
-    ./scripts/travis-emscripten/publish_binary.sh
-fi
diff --git a/scripts/travis-emscripten/deploy_key.enc b/scripts/travis-emscripten/deploy_key.enc
deleted file mode 100644
index e6e9e0e6972d4af5bce8593e7656f11d4541f3b7..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 1680
zcmV;B25<RRgi@c)RSX=d=i&%7=L6n->yw60sSw*6J>SOk()_<|>gm~DB0~~igea~m
zfEz#1ZCy22svGpSx$jnN@l@h~GW!(K@H&FKm6VbHiTwXZBy$IwfQ_y0b^*?+DgZk~
zW+`~c_V-d9Y{O>h2X$@c^<OW-e;;#Pt*F*A2$TMDkUp-i{c2vX!}-IRDx2)Ey^st;
ziv2VQ+aqnmP6|WQ&}KdRFJ_~DEpwAieX!?oBu+Sg6K}!(l2^R2^JiOM<N;`U>h#eC
z@XDjAqEPvvHMG%4*fVG`!!&5Iah8>k;_a6~uJpKb)oA9U(Y{{nz<<5HW9uMfvS*YH
zIx9fjvhgYc8Bd?*!)mDE$X|e+f=}6~V{!>~A9tMJs=^IS1{oJuisd@^WQ}OVq=JoT
zwtP~DFTdiuLHrZb6j^5G+#FCqO!&WB0JV-q$cx#Ks<34`+da6#H+9mGO>>dV;$_=O
z%|gvS2?@z;4}BhQmMx^+_^NZl!^v=aSSkn!Bc@dM1FaZbrd7!TzxVvBl%}^&Pv=0H
z*Na<x{rhhPe$x=yqE#vMN#sTro26ZRZ}p{bv98dq&9*YslkpX0`I5R<UmjzMyn}^=
zb%M0rdb~{v`b1ZLWQH^3XmHv%5T#`tyJ#E&!9w!9XqM1RMkyP+PF&zCPuUQ0&kWEP
zy+eHad5hwoI*^;y^;kF5xFyqvLajza5x-{u-7*fe^+<SkPG@S#whrqxjEy=CGVrb{
zv^QPOI&t>JnA)n$>((m<s`g3j$yLA?It<%Wn(Hl5XS>&7WIh%ZNW$R%M^)StQ*~NE
z`eI(m)kP9FhCM#zMEoI)X#A{?LE(fPz5jK(_w!^&TlcAir|d*^1otK1$`=&z8>_Gz
z3s?^|TckA8+V*mNG2}W9wMhNEwC#)DjK3nCT6Dy}=L`vXL>flDkbEnE6xxXDPobQ*
zNdDq?a)(?^nT<zLu^M7Rg?C8O()~ixWfCnGQ+NK1@6qn%d#wCq<O+La-+hS4Z3Sve
zCAS1*MsVF@LhO<+V$S9A=90nrNXhCp)K&2^&ZDXTGy&S-`ScPKe=4q<t^ijt>G(=%
z-1Ak!@Dv9%AY1o;0&_7u4)xE^Ek~8xgZUUn4Z}v3wy6<Rd9LIToWi)wEeUTrPqs_Y
zS$FiZXN(^mRnP!aJe%n4g4<v6yv%F4JrCf6r~Q+3AjS`K7LhP~5K{aG0Z>J*KC5bc
zLr?V%zfYhy;)|ezDEW{N_32zvSz5~i9zHf%;P>c^E&`$cQZN#s(z|VLKpbK{zyQLy
zu-|DZAW|$@{~oh@UZpYrf_>kw=R~rAX)@8~QtkbpvU!LXCfd*!#Dup3$<qJET!1YT
zS|Kv=(h8nhPEQ@HwT8}>e*arind+i5$GM2V$Rde*xT&*x_>+hm6CT=U;X(oO+e5XV
zZ2OmX&)BxQduAEZ9@8>Y5cN54ib-9K%bM5rkcuD(-PYg{Jpb8^$XJmZMV7c2DF1GW
zq~{~xUNh~pT6D{Z|Ib?{O3YHhnRvnTM1XRgGzDmd_oO(sw}?v}U%EZ6SOI1X_B==L
zPq-_T)Ju92S*a(hvm|fGh!JJL-P|{g(_5IYHYn}suS#@X2ra)N+%k8YXfN<_@(E{F
z>g|88G>4v5`LHfq#%(>uo2iJ{JyxM#<%MF*^x^!2!i48G0{R{;Vt@rvTRtEwO!_wi
z(bQlzU6ya$w>_0@6jmz@!)A?~qBgIT^<8%%qp2FB$~?&|%JR){@vMT^>10In&=U{C
z&Y*rA_dFJ4Z5EtnwFbv~rS|V`1U+(U1wGaE1cO^mbf9_Z{%+CpaN4xj7F?%ic(5dY
zvjxHFKi*S+Ya$ZSG)P(M-b6G!G$IS&L=Dcr^MJZPs|>W+MYEGt0{Ja&uK}g3T`HOs
zFjvArVeilYqUYY1fATOxeD#BuW2^J2y<KC7)mUTPU$+I_t$IQBok3(|?<l><ELd@s
zjBPykpZBXWDY@m>LxH<Jc_BL|y?kmIL&IYVJ`;GojE2{l7`8K40FN*SvI?)oIS*Ca
zzzuui3P(IAy`07VONC=kIH3%Dkr&1P`q_>UPD4E7cuvs^5`R~Tr9ct|698Ex!05|6
z`YrNtZl>{wNLqSxPr7*_OoRDWdoTRaA)`|09(ue*-)G9W2_<7AZRLalXLzsWlsXo*
aLV|wj-F@l8tkrS^WyVcW43N^C2UT@6Ia0I$

diff --git a/scripts/travis-emscripten/publish_binary.sh b/scripts/travis-emscripten/publish_binary.sh
deleted file mode 100755
index eba3cdac5..000000000
--- a/scripts/travis-emscripten/publish_binary.sh
+++ /dev/null
@@ -1,99 +0,0 @@
-#!/usr/bin/env bash
-
-#------------------------------------------------------------------------------
-# Bash script for publishing Solidity Emscripten binaries to Github.
-#
-# The results are committed to https://github.com/ethereum/solc-bin.
-#
-# The documentation for solidity is hosted at:
-#
-# http://solidity.readthedocs.io/
-#
-# ------------------------------------------------------------------------------
-# This file is part of solidity.
-#
-# solidity is free software: you can redistribute it and/or modify
-# it under the terms of the GNU General Public License as published by
-# the Free Software Foundation, either version 3 of the License, or
-# (at your option) any later version.
-#
-# solidity is distributed in the hope that it will be useful,
-# but WITHOUT ANY WARRANTY; without even the implied warranty of
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-# GNU General Public License for more details.
-#
-# You should have received a copy of the GNU General Public License
-# along with solidity.  If not, see <http://www.gnu.org/licenses/>
-#
-# (c) 2016 solidity contributors.
-#------------------------------------------------------------------------------
-
-set -e
-
-VER=$(cat CMakeLists.txt | grep 'set(PROJECT_VERSION' | sed -e 's/.*set(PROJECT_VERSION "\(.*\)".*/\1/')
-test -n "$VER"
-VER="v$VER"
-COMMIT=$(git rev-parse --short=8 HEAD)
-DATE=$(date --date="$(git log -1 --date=iso --format=%ad HEAD)" --utc +%Y.%-m.%-d)
-
-ENCRYPTED_KEY_VAR="encrypted_${ENCRYPTION_LABEL}_key"
-ENCRYPTED_IV_VAR="encrypted_${ENCRYPTION_LABEL}_iv"
-ENCRYPTED_KEY=${!ENCRYPTED_KEY_VAR}
-ENCRYPTED_IV=${!ENCRYPTED_IV_VAR}
-openssl aes-256-cbc -K $ENCRYPTED_KEY -iv $ENCRYPTED_IV -in scripts/travis-emscripten/deploy_key.enc -out deploy_key -d
-chmod 600 deploy_key
-eval `ssh-agent -s`
-ssh-add deploy_key
-
-git clone --depth 2 git@github.com:ethereum/solc-bin.git
-cd solc-bin
-git config user.name "travis"
-git config user.email "chris@ethereum.org"
-git checkout -B gh-pages origin/gh-pages
-git clean -f -d -x
-
-
-FULLVERSION=INVALID
-if [ "$TRAVIS_BRANCH" = release ]
-then
-    # We only want one file with this version
-    if ls ./bin/soljson-"$VER+"*.js
-    then
-      echo "Not publishing, we already published this version."
-      exit 0
-    fi
-    FULLVERSION="$VER+commit.$COMMIT"
-elif [ "$TRAVIS_BRANCH" = develop ]
-then
-    # We only want one release per day and we do not want to push the same commit twice.
-    if ls ./bin/soljson-"$VER-nightly.$DATE"*.js || ls ./bin/soljson-*"commit.$COMMIT.js"
-    then
-      echo "Not publishing, we already published this version today."
-      exit 0
-    fi
-    FULLVERSION="$VER-nightly.$DATE+commit.$COMMIT"
-else
-    echo "Not publishing, wrong branch."
-    exit 0
-fi
-
-
-NEWFILE="soljson-$FULLVERSION.js"
-
-# Prepare for update script
-npm install
-
-# This file is assumed to be the product of the build_emscripten.sh script.
-cp ../soljson.js ./bin/"$NEWFILE"
-
-# For releases, add a symlink to the wasm directory.
-[ "$TRAVIS_BRANCH" = release ] && ln -sf ../bin/"$NEWFILE" ./wasm/"$NEWFILE"
-
-# Run update script
-npm run update
-
-# Publish updates
-git add ./bin/"$NEWFILE"
-[ "$TRAVIS_BRANCH" = release ] && git add ./wasm/"$NEWFILE"
-git commit -a -m "Added compiler version $FULLVERSION"
-git push origin gh-pages
diff --git a/scripts/wasm-rebuild/docker-scripts/rebuild_current.sh b/scripts/wasm-rebuild/docker-scripts/rebuild_current.sh
index b48b37fc5..9a28ce30c 100755
--- a/scripts/wasm-rebuild/docker-scripts/rebuild_current.sh
+++ b/scripts/wasm-rebuild/docker-scripts/rebuild_current.sh
@@ -41,7 +41,7 @@ if [ -d jsoncpp ]; then
 fi
 
 set +e
-scripts/travis-emscripten/build_emscripten.sh
+scripts/*/build_emscripten.sh
 set -e
 
 mkdir -p upload

From cf35785328b477343b7c1b135b91c328cb220fce Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 19 Oct 2020 18:11:59 +0100
Subject: [PATCH 03/10] Add unknown message to all verification targets

---
 Changelog.md                                    |  4 ++++
 libsolidity/formal/CHC.cpp                      | 17 ++++++++++-------
 .../crypto/crypto_functions_fail.sol            |  3 +++
 ...s_same_input_over_state_same_output_fail.sol |  3 +++
 .../smtCheckerTests/imports/import_base.sol     |  1 +
 .../invariants/loop_nested_for.sol              |  1 +
 .../smtCheckerTests/loops/for_1_fail.sol        |  1 +
 .../loops/for_1_false_positive.sol              |  1 +
 ...hile_loop_array_assignment_memory_memory.sol |  1 +
 ...ile_loop_array_assignment_memory_storage.sol |  1 +
 ...le_loop_array_assignment_storage_storage.sol |  1 +
 .../operators/compound_bitwise_or_int_1.sol     |  1 +
 .../operators/compound_bitwise_or_uint_1.sol    |  1 +
 .../operators/compound_bitwise_or_uint_2.sol    |  1 +
 .../operators/compound_bitwise_or_uint_3.sol    |  1 +
 .../smtCheckerTests/operators/mod_signed.sol    |  1 +
 .../operators/slice_default_end.sol             |  3 +++
 .../operators/slice_default_start.sol           |  1 +
 18 files changed, 36 insertions(+), 7 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index cd3806d18..170b7d46e 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,6 +1,10 @@
 ### 0.7.5 (unreleased)
 
 
+Bugfixes:
+ * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.
+
+
 
 ### 0.7.4 (2020-10-19)
 
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index ea14bf12e..880e9c553 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -1215,22 +1215,25 @@ void CHC::checkVerificationTargets()
 				if (!intType)
 					intType = TypeProvider::uint256();
 
-				satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ") happens here.";
-				satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ") happens here.";
+				satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")";
+				satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")";
 				if (target.type == VerificationTarget::Type::Underflow)
 				{
-					satMsg = satMsgUnderflow;
+					satMsg = satMsgUnderflow + " happens here.";
+					unknownMsg = satMsgUnderflow + " might happen here.";
 					errorReporterId = underflowErrorId;
 				}
 				else if (target.type == VerificationTarget::Type::Overflow)
 				{
-					satMsg = satMsgOverflow;
+					satMsg = satMsgOverflow + " happens here.";
+					unknownMsg = satMsgOverflow + " might happen here.";
 					errorReporterId = overflowErrorId;
 				}
 			}
 			else if (target.type == VerificationTarget::Type::DivByZero)
 			{
 				satMsg = "Division by zero happens here.";
+				unknownMsg = "Division by zero might happen here.";
 				errorReporterId = 4281_error;
 			}
 			else
@@ -1246,12 +1249,12 @@ void CHC::checkVerificationTargets()
 			{
 				auto specificTarget = target;
 				specificTarget.type = VerificationTarget::Type::Underflow;
-				checkAndReportTarget(scope, specificTarget, errorId, underflowErrorId, satMsgUnderflow, unknownMsg);
+				checkAndReportTarget(scope, specificTarget, errorId, underflowErrorId, satMsgUnderflow + " happens here.", satMsgUnderflow + " might happen here.");
 
 				++it;
 				solAssert(it != m_errorIds.end(), "");
 				specificTarget.type = VerificationTarget::Type::Overflow;
-				checkAndReportTarget(scope, specificTarget, it->second, overflowErrorId, satMsgOverflow, unknownMsg);
+				checkAndReportTarget(scope, specificTarget, it->second, overflowErrorId, satMsgOverflow + " happens here.", satMsgOverflow + " might happen here.");
 			}
 		}
 	}
@@ -1267,7 +1270,7 @@ void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const&
 		solAssert(it != m_errorIds.end(), "");
 		unsigned errorId = it->second;
 
-		checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here.");
+		checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here.", "Assertion violation might happen here.");
 	}
 }
 
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
index 5f9a7f22e..36e34cc4d 100644
--- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
@@ -24,8 +24,11 @@ contract C {
 }
 // ----
 // Warning 1218: (168-184): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (168-184): CHC: Assertion violation might happen here.
 // Warning 1218: (305-321): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (305-321): CHC: Assertion violation might happen here.
 // Warning 1218: (448-464): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (448-464): CHC: Assertion violation might happen here.
 // Warning 6328: (673-689): CHC: Assertion violation happens here.
 // Warning 4661: (168-184): BMC: Assertion violation happens here.
 // Warning 4661: (305-321): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
index 9d8c98479..10c6ada8e 100644
--- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
@@ -46,8 +46,11 @@ contract C {
 }
 // ----
 // Warning 1218: (726-745): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (726-745): CHC: Assertion violation might happen here.
 // Warning 1218: (749-768): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (749-768): CHC: Assertion violation might happen here.
 // Warning 1218: (772-791): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (772-791): CHC: Assertion violation might happen here.
 // Warning 6328: (795-814): CHC: Assertion violation happens here.
 // Warning 4661: (726-745): BMC: Assertion violation happens here.
 // Warning 4661: (749-768): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/imports/import_base.sol b/test/libsolidity/smtCheckerTests/imports/import_base.sol
index eca0249c2..e7bf269be 100644
--- a/test/libsolidity/smtCheckerTests/imports/import_base.sol
+++ b/test/libsolidity/smtCheckerTests/imports/import_base.sol
@@ -18,6 +18,7 @@ contract Der is Base {
 	}
 }
 // ----
+// Warning 4984: (der:101-109): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (der:113-126): CHC: Assertion violation happens here.
 // Warning 2661: (base:100-103): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (der:101-109): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol b/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol
index 8365c0e4b..1b971795a 100644
--- a/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol
+++ b/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol
@@ -13,4 +13,5 @@ contract Simple {
 	}
 }
 // ----
+// Warning 6328: (187-201): CHC: Assertion violation might happen here.
 // Warning 4661: (187-201): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
index c05da9572..1135d12e7 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
@@ -14,5 +14,6 @@ contract C
 // ====
 // SMTSolvers: z3
 // ----
+// Warning 4984: (176-181): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (189-203): CHC: Assertion violation happens here.
 // Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
index f4176588e..29afb548f 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
@@ -14,4 +14,5 @@ contract C
 	}
 }
 // ----
+// Warning 4984: (176-181): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
index d540351a2..41d602961 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
@@ -20,5 +20,6 @@ contract LoopFor2 {
 // ====
 // SMTSolvers: z3
 // ----
+// Warning 4984: (244-249): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (373-392): CHC: Assertion violation happens here.
 // Warning 6328: (396-415): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
index 50a91d19b..29509fc5c 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
@@ -25,3 +25,4 @@ contract LoopFor2 {
 // ====
 // SMTSolvers: z3
 // ----
+// Warning 4984: (237-242): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
index 6bf40282a..44a94090b 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
@@ -20,5 +20,6 @@ contract LoopFor2 {
 	}
 }
 // ----
+// Warning 4984: (229-234): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (290-309): CHC: Assertion violation happens here.
 // Warning 6328: (313-332): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
index e25ae354d..7c198b24e 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
@@ -9,3 +9,4 @@ contract C {
     }
 }
 // ----
+// Warning 6328: (174-212): CHC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
index 790d30a76..7a3441661 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
@@ -9,3 +9,4 @@ contract C {
     }
 }
 // ----
+// Warning 6328: (166-183): CHC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
index 714c0df22..6e62d8148 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
@@ -11,4 +11,5 @@ contract C {
     }
 }
 // ----
+// Warning 6328: (173-192): CHC: Assertion violation might happen here.
 // Warning 7812: (173-192): BMC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
index 46311b750..b6e9af8a8 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
@@ -10,4 +10,5 @@ contract C {
     }
 }
 // ----
+// Warning 6328: (157-172): CHC: Assertion violation might happen here.
 // Warning 7812: (157-172): BMC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/operators/mod_signed.sol b/test/libsolidity/smtCheckerTests/operators/mod_signed.sol
index 552e304dd..8588fcf9a 100644
--- a/test/libsolidity/smtCheckerTests/operators/mod_signed.sol
+++ b/test/libsolidity/smtCheckerTests/operators/mod_signed.sol
@@ -10,3 +10,4 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (163-180): CHC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol b/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol
index 1681c0ca5..4cb63ac44 100644
--- a/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol
+++ b/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol
@@ -12,6 +12,9 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (221-253): CHC: Assertion violation might happen here.
+// Warning 6328: (257-289): CHC: Assertion violation might happen here.
+// Warning 6328: (293-326): CHC: Assertion violation might happen here.
 // Warning 4661: (221-253): BMC: Assertion violation happens here.
 // Warning 4661: (257-289): BMC: Assertion violation happens here.
 // Warning 4661: (293-326): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/slice_default_start.sol b/test/libsolidity/smtCheckerTests/operators/slice_default_start.sol
index 61aa3ba2a..79de4639c 100644
--- a/test/libsolidity/smtCheckerTests/operators/slice_default_start.sol
+++ b/test/libsolidity/smtCheckerTests/operators/slice_default_start.sol
@@ -9,5 +9,6 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (157-189): CHC: Assertion violation might happen here.
 // Warning 6328: (193-225): CHC: Assertion violation happens here.
 // Warning 4661: (157-189): BMC: Assertion violation happens here.

From e99146533659dd36acb1af45154c3b38b0048f1f Mon Sep 17 00:00:00 2001
From: Mathias Baumann <marenz@supradigital.org>
Date: Wed, 14 Oct 2020 12:42:44 +0200
Subject: [PATCH 04/10] Fix dependency tracking for abstract contracts

---
 Changelog.md                            |  2 +-
 libsolidity/interface/CompilerStack.cpp |  6 +++-
 test/libsolidity/StandardCompiler.cpp   | 40 +++++++++++++++++++++++++
 3 files changed, 46 insertions(+), 2 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index 170b7d46e..fee4eb648 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -3,7 +3,7 @@
 
 Bugfixes:
  * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.
-
+ * Code generator: Fix missing creation dependency tracking for abstract contracts.
 
 
 ### 0.7.4 (2020-10-19)
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index e57d7c823..dbe57764a 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -1160,11 +1160,15 @@ void CompilerStack::compileContract(
 	if (m_hasError)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Called compile with errors."));
 
-	if (_otherCompilers.count(&_contract) || !_contract.canBeDeployed())
+	if (_otherCompilers.count(&_contract))
 		return;
+
 	for (auto const* dependency: _contract.annotation().contractDependencies)
 		compileContract(*dependency, _otherCompilers);
 
+	if (!_contract.canBeDeployed())
+		return;
+
 	Contract& compiledContract = m_contracts.at(_contract.fullyQualifiedName());
 
 	shared_ptr<Compiler> compiler = make_shared<Compiler>(m_evmVersion, m_revertStrings, m_optimiserSettings);
diff --git a/test/libsolidity/StandardCompiler.cpp b/test/libsolidity/StandardCompiler.cpp
index 8ff8a85aa..de43bf9fa 100644
--- a/test/libsolidity/StandardCompiler.cpp
+++ b/test/libsolidity/StandardCompiler.cpp
@@ -1505,6 +1505,46 @@ BOOST_AUTO_TEST_CASE(stopAfter_ast_output)
 	BOOST_CHECK(result["sources"]["a.sol"]["ast"].isObject());
 }
 
+BOOST_AUTO_TEST_CASE(dependency_tracking_of_abstract_contract)
+{
+	char const* input = R"(
+	{
+		"language": "Solidity",
+		"sources": {
+			"BlockRewardAuRaBase.sol": {
+				"content": " contract Sacrifice { constructor() payable {} } abstract contract BlockRewardAuRaBase { function _transferNativeReward() internal { new Sacrifice(); } function _distributeTokenRewards() internal virtual; } "
+			},
+			"BlockRewardAuRaCoins.sol": {
+				"content": " import \"./BlockRewardAuRaBase.sol\"; contract BlockRewardAuRaCoins is BlockRewardAuRaBase { function transferReward() public { _transferNativeReward(); } function _distributeTokenRewards() internal override {} } "
+			}
+		},
+		"settings": {
+			"outputSelection": {
+				"BlockRewardAuRaCoins.sol": {
+					"BlockRewardAuRaCoins": ["evm.bytecode.sourceMap"]
+				}
+			}
+		}
+	}
+	)";
+
+	Json::Value parsedInput;
+	BOOST_REQUIRE(util::jsonParseStrict(input, parsedInput));
+
+	solidity::frontend::StandardCompiler compiler;
+	Json::Value result = compiler.compile(parsedInput);
+
+	BOOST_REQUIRE(result["contracts"].isObject());
+	BOOST_REQUIRE(result["contracts"].size() == 1);
+	BOOST_REQUIRE(result["contracts"]["BlockRewardAuRaCoins.sol"].isObject());
+	BOOST_REQUIRE(result["contracts"]["BlockRewardAuRaCoins.sol"].size() == 1);
+	BOOST_REQUIRE(result["contracts"]["BlockRewardAuRaCoins.sol"]["BlockRewardAuRaCoins"].isObject());
+	BOOST_REQUIRE(result["contracts"]["BlockRewardAuRaCoins.sol"]["BlockRewardAuRaCoins"]["evm"].isObject());
+	BOOST_REQUIRE(result["contracts"]["BlockRewardAuRaCoins.sol"]["BlockRewardAuRaCoins"]["evm"]["bytecode"].isObject());
+	BOOST_REQUIRE(result["sources"].isObject());
+	BOOST_REQUIRE(result["sources"].size() == 2);
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 } // end namespaces

From a4dc110b38e4a04140da8554abe41d678befda21 Mon Sep 17 00:00:00 2001
From: Mathias Baumann <marenz@supradigital.org>
Date: Wed, 14 Oct 2020 12:42:44 +0200
Subject: [PATCH 05/10] Fix dependency tracking for abstract contracts for Yul
 codegen

---
 libsolidity/codegen/ir/IRGenerator.cpp        |  4 +-
 libsolidity/codegen/ir/IRGenerator.h          |  4 +-
 libsolidity/interface/CompilerStack.cpp       | 16 +++---
 test/libsolidity/StandardCompiler.cpp         | 52 ++++++++++++++++++-
 .../freeFunctions/free_runtimecode.sol        |  2 +
 .../freeFunctions/new_operator.sol            |  2 +
 6 files changed, 67 insertions(+), 13 deletions(-)

diff --git a/libsolidity/codegen/ir/IRGenerator.cpp b/libsolidity/codegen/ir/IRGenerator.cpp
index 897e83290..46ae3381c 100644
--- a/libsolidity/codegen/ir/IRGenerator.cpp
+++ b/libsolidity/codegen/ir/IRGenerator.cpp
@@ -50,7 +50,7 @@ using namespace solidity::frontend;
 
 pair<string, string> IRGenerator::run(
 	ContractDefinition const& _contract,
-	map<ContractDefinition const*, string const> const& _otherYulSources
+	map<ContractDefinition const*, string_view const> const& _otherYulSources
 )
 {
 	string const ir = yul::reindent(generate(_contract, _otherYulSources));
@@ -78,7 +78,7 @@ pair<string, string> IRGenerator::run(
 
 string IRGenerator::generate(
 	ContractDefinition const& _contract,
-	map<ContractDefinition const*, string const> const& _otherYulSources
+	map<ContractDefinition const*, string_view const> const& _otherYulSources
 )
 {
 	auto subObjectSources = [&_otherYulSources](std::set<ContractDefinition const*, ASTNode::CompareByID> const& subObjects) -> string
diff --git a/libsolidity/codegen/ir/IRGenerator.h b/libsolidity/codegen/ir/IRGenerator.h
index 94433912d..cdb431e83 100644
--- a/libsolidity/codegen/ir/IRGenerator.h
+++ b/libsolidity/codegen/ir/IRGenerator.h
@@ -53,13 +53,13 @@ public:
 	/// (or just pretty-printed, depending on the optimizer settings).
 	std::pair<std::string, std::string> run(
 		ContractDefinition const& _contract,
-		std::map<ContractDefinition const*, std::string const> const& _otherYulSources
+		std::map<ContractDefinition const*, std::string_view const> const& _otherYulSources
 	);
 
 private:
 	std::string generate(
 		ContractDefinition const& _contract,
-		std::map<ContractDefinition const*, std::string const> const& _otherYulSources
+		std::map<ContractDefinition const*, std::string_view const> const& _otherYulSources
 	);
 	std::string generate(Block const& _block);
 
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index dbe57764a..119ea42b8 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -525,6 +525,7 @@ bool CompilerStack::compile(State _stopAfter)
 
 	// Only compile contracts individually which have been requested.
 	map<ContractDefinition const*, shared_ptr<Compiler const>> otherCompilers;
+
 	for (Source const* source: m_sourceOrder)
 		for (ASTPointer<ASTNode> const& node: source->ast->nodes())
 			if (auto contract = dynamic_cast<ContractDefinition const*>(node.get()))
@@ -1231,21 +1232,20 @@ void CompilerStack::generateIR(ContractDefinition const& _contract)
 	if (m_hasError)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Called generateIR with errors."));
 
-	if (!_contract.canBeDeployed())
-		return;
-
-	map<ContractDefinition const*, string const> otherYulSources;
-
 	Contract& compiledContract = m_contracts.at(_contract.fullyQualifiedName());
 	if (!compiledContract.yulIR.empty())
 		return;
 
 	string dependenciesSource;
 	for (auto const* dependency: _contract.annotation().contractDependencies)
-	{
 		generateIR(*dependency);
-		otherYulSources.emplace(dependency, m_contracts.at(dependency->fullyQualifiedName()).yulIR);
-	}
+
+	if (!_contract.canBeDeployed())
+		return;
+
+	map<ContractDefinition const*, string_view const> otherYulSources;
+	for (auto const& pair: m_contracts)
+		otherYulSources.emplace(pair.second.contract, pair.second.yulIR);
 
 	IRGenerator generator(m_evmVersion, m_revertStrings, m_optimiserSettings);
 	tie(compiledContract.yulIR, compiledContract.yulIROptimized) = generator.run(_contract, otherYulSources);
diff --git a/test/libsolidity/StandardCompiler.cpp b/test/libsolidity/StandardCompiler.cpp
index de43bf9fa..37539d712 100644
--- a/test/libsolidity/StandardCompiler.cpp
+++ b/test/libsolidity/StandardCompiler.cpp
@@ -1521,7 +1521,7 @@ BOOST_AUTO_TEST_CASE(dependency_tracking_of_abstract_contract)
 		"settings": {
 			"outputSelection": {
 				"BlockRewardAuRaCoins.sol": {
-					"BlockRewardAuRaCoins": ["evm.bytecode.sourceMap"]
+					"BlockRewardAuRaCoins": ["ir", "evm.bytecode.sourceMap"]
 				}
 			}
 		}
@@ -1540,11 +1540,61 @@ BOOST_AUTO_TEST_CASE(dependency_tracking_of_abstract_contract)
 	BOOST_REQUIRE(result["contracts"]["BlockRewardAuRaCoins.sol"].size() == 1);
 	BOOST_REQUIRE(result["contracts"]["BlockRewardAuRaCoins.sol"]["BlockRewardAuRaCoins"].isObject());
 	BOOST_REQUIRE(result["contracts"]["BlockRewardAuRaCoins.sol"]["BlockRewardAuRaCoins"]["evm"].isObject());
+	BOOST_REQUIRE(result["contracts"]["BlockRewardAuRaCoins.sol"]["BlockRewardAuRaCoins"]["ir"].isString());
 	BOOST_REQUIRE(result["contracts"]["BlockRewardAuRaCoins.sol"]["BlockRewardAuRaCoins"]["evm"]["bytecode"].isObject());
 	BOOST_REQUIRE(result["sources"].isObject());
 	BOOST_REQUIRE(result["sources"].size() == 2);
 }
 
+BOOST_AUTO_TEST_CASE(dependency_tracking_of_abstract_contract_yul)
+{
+	char const* input = R"(
+	{
+		"language": "Solidity",
+		"sources": {
+			"A.sol": {
+				"content": "contract A {} contract B {} contract C { constructor() { new B(); } } contract D {}"
+			}
+		},
+		"settings": {
+			"outputSelection": {
+				"A.sol": {
+					"C": ["ir"]
+				}
+			}
+		}
+	}
+	)";
+
+	Json::Value parsedInput;
+	BOOST_REQUIRE(util::jsonParseStrict(input, parsedInput));
+
+	solidity::frontend::StandardCompiler compiler;
+	Json::Value result = compiler.compile(parsedInput);
+
+	BOOST_REQUIRE(result["contracts"].isObject());
+	BOOST_REQUIRE(result["contracts"].size() == 1);
+	BOOST_REQUIRE(result["contracts"]["A.sol"].isObject());
+	BOOST_REQUIRE(result["contracts"]["A.sol"].size() == 1);
+	BOOST_REQUIRE(result["contracts"]["A.sol"]["C"].isObject());
+	BOOST_REQUIRE(result["contracts"]["A.sol"]["C"]["ir"].isString());
+
+	const string& irCode = result["contracts"]["A.sol"]["C"]["ir"].asString();
+
+	// Make sure C and B contracts are deployed
+	BOOST_REQUIRE(irCode.find("object \"C") != string::npos);
+	BOOST_REQUIRE(irCode.find("object \"B") != string::npos);
+
+	// Make sure A and D are NOT deployed as they were not requested and are not
+	// in any dependency
+	BOOST_REQUIRE(irCode.find("object \"A") == string::npos);
+	BOOST_REQUIRE(irCode.find("object \"D") == string::npos);
+
+
+	BOOST_REQUIRE(result["sources"].isObject());
+	BOOST_REQUIRE(result["sources"].size() == 1);
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 } // end namespaces
diff --git a/test/libsolidity/semanticTests/freeFunctions/free_runtimecode.sol b/test/libsolidity/semanticTests/freeFunctions/free_runtimecode.sol
index 7a05ff5d0..a79d68a3c 100644
--- a/test/libsolidity/semanticTests/freeFunctions/free_runtimecode.sol
+++ b/test/libsolidity/semanticTests/freeFunctions/free_runtimecode.sol
@@ -11,5 +11,7 @@ contract D {
     return test();
   }
 }
+// ====
+// compileViaYul: true
 // ----
 // f() -> true
diff --git a/test/libsolidity/semanticTests/freeFunctions/new_operator.sol b/test/libsolidity/semanticTests/freeFunctions/new_operator.sol
index e35f1c9ea..7a7e53759 100644
--- a/test/libsolidity/semanticTests/freeFunctions/new_operator.sol
+++ b/test/libsolidity/semanticTests/freeFunctions/new_operator.sol
@@ -11,5 +11,7 @@ contract D {
     return test();
   }
 }
+// ====
+// compileViaYul: true
 // ----
 // f() -> 2

From 53d6721e47f83f2909bb27a467235bc4fb4128d4 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Tue, 20 Oct 2020 17:29:11 +0200
Subject: [PATCH 06/10] Extract mask bytes function.

---
 libsolidity/codegen/YulUtilFunctions.cpp | 22 ++++++++++++++++++----
 libsolidity/codegen/YulUtilFunctions.h   |  5 +++++
 2 files changed, 23 insertions(+), 4 deletions(-)

diff --git a/libsolidity/codegen/YulUtilFunctions.cpp b/libsolidity/codegen/YulUtilFunctions.cpp
index 7884fcfa4..a4bd0a0aa 100644
--- a/libsolidity/codegen/YulUtilFunctions.cpp
+++ b/libsolidity/codegen/YulUtilFunctions.cpp
@@ -434,6 +434,21 @@ string YulUtilFunctions::updateByteSliceFunctionDynamic(size_t _numBytes)
 	});
 }
 
+string YulUtilFunctions::maskBytesFunctionDynamic()
+{
+	string functionName = "mask_bytes_dynamic";
+	return m_functionCollector.createFunction(functionName, [&]() {
+		return Whiskers(R"(
+			function <functionName>(data, bytes) -> result {
+				let mask := not(<shr>(mul(8, bytes), not(0)))
+				result := and(data, mask)
+			})")
+			("functionName", functionName)
+			("shr", shiftRightFunctionDynamic())
+			.render();
+	});
+}
+
 string YulUtilFunctions::roundUpFunction()
 {
 	string functionName = "round_up_to_mul_of_32";
@@ -1143,12 +1158,11 @@ string YulUtilFunctions::shortByteArrayEncodeUsedAreaSetLengthFunction()
 			function <functionName>(data, len) -> used {
 				// we want to save only elements that are part of the array after resizing
 				// others should be set to zero
-				let mask := <shl>(mul(8, sub(32, len)), <ones>)
-				used := or(and(data, mask), mul(2, len))
+				data := <maskBytes>(data, len)
+				used := or(data, mul(2, len))
 			})")
 			("functionName", functionName)
-			("shl", shiftLeftFunctionDynamic())
-			("ones", formatNumber((bigint(1) << 256) - 1))
+			("maskBytes", maskBytesFunctionDynamic())
 			.render();
 	});
 }
diff --git a/libsolidity/codegen/YulUtilFunctions.h b/libsolidity/codegen/YulUtilFunctions.h
index 69e510c48..a91eb525d 100644
--- a/libsolidity/codegen/YulUtilFunctions.h
+++ b/libsolidity/codegen/YulUtilFunctions.h
@@ -99,6 +99,11 @@ public:
 	/// signature: (value, shiftBytes, toInsert) -> result
 	std::string updateByteSliceFunctionDynamic(size_t _numBytes);
 
+	/// Function that sets all but the first ``bytes`` bytes of ``value`` to zero.
+	/// @note ``bytes`` has to be small enough not to overflo ``8 * bytes``.
+	/// signature: (value, bytes) -> result
+	std::string maskBytesFunctionDynamic();
+
 	/// @returns the name of a function that rounds its input to the next multiple
 	/// of 32 or the input if it is a multiple of 32.
 	/// signature: (value) -> result

From 3920f398aafa7375b5d6fb8911eb0600bff2d0b2 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Wed, 21 Oct 2020 09:48:22 +0200
Subject: [PATCH 07/10] Update libsolidity/codegen/YulUtilFunctions.h

Co-authored-by: Harikrishnan Mulackal <webmail.hari@gmail.com>
---
 libsolidity/codegen/YulUtilFunctions.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/libsolidity/codegen/YulUtilFunctions.h b/libsolidity/codegen/YulUtilFunctions.h
index a91eb525d..b84dad4f9 100644
--- a/libsolidity/codegen/YulUtilFunctions.h
+++ b/libsolidity/codegen/YulUtilFunctions.h
@@ -100,7 +100,7 @@ public:
 	std::string updateByteSliceFunctionDynamic(size_t _numBytes);
 
 	/// Function that sets all but the first ``bytes`` bytes of ``value`` to zero.
-	/// @note ``bytes`` has to be small enough not to overflo ``8 * bytes``.
+	/// @note ``bytes`` has to be small enough not to overflow ``8 * bytes``.
 	/// signature: (value, bytes) -> result
 	std::string maskBytesFunctionDynamic();
 

From f0d81601db495e6d2f23f41381e2e7a480837639 Mon Sep 17 00:00:00 2001
From: Martin Blicha <blichm@usi.ch>
Date: Mon, 19 Oct 2020 18:54:42 +0200
Subject: [PATCH 08/10] [SMTChecker] Adding division by zero checks in the CHC
 engine

---
 Changelog.md                                  |   2 +
 libsolidity/formal/BMC.cpp                    |   7 +
 libsolidity/formal/CHC.cpp                    | 205 ++++++++----------
 libsolidity/formal/CHC.h                      |  10 +-
 libsolidity/formal/SMTEncoder.cpp             |  13 +-
 scripts/error_codes.py                        |   4 +-
 .../smtCheckerTests/math/addmod_1.sol         |   5 +-
 .../math/addmod_mulmod_zero.sol               |   6 +-
 .../smtCheckerTests/math/mulmod_1.sol         |   5 +-
 .../smtCheckerTests/operators/div_zero.sol    |   2 +-
 .../smtCheckerTests/operators/division_1.sol  |   2 +-
 .../overflow/signed_div_overflow.sol          |   2 +-
 .../overflow/signed_mod_overflow.sol          |   2 +-
 .../overflow/unsigned_div_overflow.sol        |   2 +-
 .../overflow/unsigned_mod_overflow.sol        |   2 +-
 .../types/fixed_bytes_access_2.sol            |   2 +-
 16 files changed, 126 insertions(+), 145 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index fee4eb648..f02123341 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,7 @@
 ### 0.7.5 (unreleased)
 
+Compiler Features:
+ * SMTChecker: Add division by zero checks in the CHC engine.
 
 Bugfixes:
  * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index dc1a08472..e41c69cd2 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -716,6 +716,13 @@ void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression cons
 void BMC::checkDivByZero(BMCVerificationTarget& _target)
 {
 	solAssert(_target.type == VerificationTarget::Type::DivByZero, "");
+
+	if (
+		m_solvedTargets.count(_target.expression) &&
+		m_solvedTargets.at(_target.expression).count(VerificationTarget::Type::DivByZero)
+	)
+		return;
+
 	checkCondition(
 		_target.constraints && (_target.value == 0),
 		_target.callStack,
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 880e9c553..7bedc8a65 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -533,18 +533,9 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 
 void CHC::visitAddMulMod(FunctionCall const& _funCall)
 {
-	auto previousError = errorFlag().currentValue();
-	errorFlag().increaseIndex();
-
-	addVerificationTarget(
-		&_funCall,
-		VerificationTarget::Type::DivByZero,
-		errorFlag().currentValue()
-	);
-
 	solAssert(_funCall.arguments().at(2), "");
-	smtutil::Expression target = expr(*_funCall.arguments().at(2)) == 0 && errorFlag().currentValue() == newErrorId(_funCall);
-	m_context.addAssertion((errorFlag().currentValue() == previousError) || target);
+
+	addVerificationTarget(_funCall, VerificationTarget::Type::DivByZero, expr(*_funCall.arguments().at(2)) == 0);
 
 	SMTEncoder::visitAddMulMod(_funCall);
 }
@@ -643,13 +634,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
 	auto symbArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
 	solAssert(symbArray, "");
 
-	auto previousError = errorFlag().currentValue();
-	errorFlag().increaseIndex();
-
-	addVerificationTarget(&_arrayPop, VerificationTarget::Type::PopEmptyArray, errorFlag().currentValue());
-
-	smtutil::Expression target = (symbArray->length() <= 0) && (errorFlag().currentValue() == newErrorId(_arrayPop));
-	m_context.addAssertion((errorFlag().currentValue() == previousError) || target);
+	addVerificationTarget(_arrayPop, VerificationTarget::Type::PopEmptyArray, symbArray->length() <= 0);
 }
 
 pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
@@ -660,6 +645,9 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 	frontend::Expression const& _expression
 )
 {
+	if (_op == Token::Mod || _op == Token::Div)
+		addVerificationTarget(_expression, VerificationTarget::Type::DivByZero, _right == 0);
+
 	auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
 
 	IntegerType const* intType = nullptr;
@@ -673,46 +661,19 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 	if (_op == Token::Mod || (_op == Token::Div && !intType->isSigned()))
 		return values;
 
-	auto previousError = errorFlag().currentValue();
-	errorFlag().increaseIndex();
-
-	VerificationTarget::Type targetType;
-	unsigned errorId = newErrorId(_expression);
-
-	optional<smtutil::Expression> target;
 	if (_op == Token::Div)
-	{
-		targetType = VerificationTarget::Type::Overflow;
-		target = values.second > intType->maxValue() && errorFlag().currentValue() == errorId;
-	}
+		addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
 	else if (intType->isSigned())
 	{
-		unsigned secondErrorId = newErrorId(_expression);
-		targetType = VerificationTarget::Type::UnderOverflow;
-		target = (values.second < intType->minValue() && errorFlag().currentValue() == errorId) ||
-			(values.second > intType->maxValue() && errorFlag().currentValue() == secondErrorId);
+		addVerificationTarget(_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
+		addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
 	}
 	else if (_op == Token::Sub)
-	{
-		targetType = VerificationTarget::Type::Underflow;
-		target = values.second < intType->minValue() && errorFlag().currentValue() == errorId;
-	}
+		addVerificationTarget(_expression, VerificationTarget::Type::Underflow, values.second < intType->minValue());
 	else if (_op == Token::Add || _op == Token::Mul)
-	{
-		targetType = VerificationTarget::Type::Overflow;
-		target = values.second > intType->maxValue() && errorFlag().currentValue() == errorId;
-	}
+		addVerificationTarget(_expression, VerificationTarget::Type::Overflow, values.second > intType->maxValue());
 	else
 		solAssert(false, "");
-
-	addVerificationTarget(
-		&_expression,
-		targetType,
-		errorFlag().currentValue()
-	);
-
-	m_context.addAssertion((errorFlag().currentValue() == previousError) || *target);
-
 	return values;
 }
 
@@ -1158,7 +1119,7 @@ void CHC::addVerificationTarget(
 	if (!source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		return;
 
-	m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId});
+	m_verificationTargets[_scope].push_back(CHCVerificationTarget{{_type, _from, _constraints}, _errorId});
 }
 
 void CHC::addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _errorId)
@@ -1175,6 +1136,18 @@ void CHC::addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type
 	}
 }
 
+void CHC::addVerificationTarget(frontend::Expression const& _scope, VerificationTarget::Type _type, smtutil::Expression const& _target)
+{
+	auto previousError = errorFlag().currentValue();
+	errorFlag().increaseIndex();
+	addVerificationTarget(&_scope, _type, errorFlag().currentValue());
+
+	m_context.addAssertion(
+		errorFlag().currentValue() == previousError ||
+		(_target && errorFlag().currentValue() == newErrorId(_scope))
+	);
+}
+
 void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId)
 {
 	addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId);
@@ -1182,79 +1155,72 @@ void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression
 
 void CHC::checkVerificationTargets()
 {
-	for (auto const& [scope, target]: m_verificationTargets)
+	for (auto const& [scope, targets]: m_verificationTargets)
 	{
-		if (target.type == VerificationTarget::Type::Assert)
-			checkAssertTarget(scope, target);
-		else
+		for (size_t i = 0; i < targets.size(); ++i)
 		{
-			string satMsg;
-			string satMsgUnderflow;
-			string satMsgOverflow;
-			string unknownMsg;
-			ErrorId errorReporterId;
-			ErrorId underflowErrorId = 3944_error;
-			ErrorId overflowErrorId = 4984_error;
+			auto const& target = targets[i];
 
-			if (target.type == VerificationTarget::Type::PopEmptyArray)
-			{
-				solAssert(dynamic_cast<FunctionCall const*>(scope), "");
-				satMsg = "Empty array \"pop\" detected here.";
-				unknownMsg = "Empty array \"pop\" might happen here.";
-				errorReporterId = 2529_error;
-			}
-			else if (
-				target.type == VerificationTarget::Type::Underflow ||
-				target.type == VerificationTarget::Type::Overflow ||
-				target.type == VerificationTarget::Type::UnderOverflow
-			)
-			{
-				auto const* expr = dynamic_cast<Expression const*>(scope);
-				solAssert(expr, "");
-				auto const* intType = dynamic_cast<IntegerType const*>(expr->annotation().type);
-				if (!intType)
-					intType = TypeProvider::uint256();
-
-				satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")";
-				satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")";
-				if (target.type == VerificationTarget::Type::Underflow)
-				{
-					satMsg = satMsgUnderflow + " happens here.";
-					unknownMsg = satMsgUnderflow + " might happen here.";
-					errorReporterId = underflowErrorId;
-				}
-				else if (target.type == VerificationTarget::Type::Overflow)
-				{
-					satMsg = satMsgOverflow + " happens here.";
-					unknownMsg = satMsgOverflow + " might happen here.";
-					errorReporterId = overflowErrorId;
-				}
-			}
-			else if (target.type == VerificationTarget::Type::DivByZero)
-			{
-				satMsg = "Division by zero happens here.";
-				unknownMsg = "Division by zero might happen here.";
-				errorReporterId = 4281_error;
-			}
-			else
-				solAssert(false, "");
-
-			auto it = m_errorIds.find(scope->id());
-			solAssert(it != m_errorIds.end(), "");
-			unsigned errorId = it->second;
-
-			if (target.type != VerificationTarget::Type::UnderOverflow)
-				checkAndReportTarget(scope, target, errorId, errorReporterId, satMsg, unknownMsg);
+			if (target.type == VerificationTarget::Type::Assert)
+				checkAssertTarget(scope, target);
 			else
 			{
-				auto specificTarget = target;
-				specificTarget.type = VerificationTarget::Type::Underflow;
-				checkAndReportTarget(scope, specificTarget, errorId, underflowErrorId, satMsgUnderflow + " happens here.", satMsgUnderflow + " might happen here.");
+				string satMsg;
+				string satMsgUnderflow;
+				string satMsgOverflow;
+				string unknownMsg;
+				ErrorId errorReporterId;
+				ErrorId underflowErrorId = 3944_error;
+				ErrorId overflowErrorId = 4984_error;
 
-				++it;
+				if (target.type == VerificationTarget::Type::PopEmptyArray)
+				{
+					solAssert(dynamic_cast<FunctionCall const*>(scope), "");
+					satMsg = "Empty array \"pop\" detected here.";
+					unknownMsg = "Empty array \"pop\" might happen here.";
+					errorReporterId = 2529_error;
+				}
+				else if (
+					target.type == VerificationTarget::Type::Underflow ||
+					target.type == VerificationTarget::Type::Overflow
+				)
+				{
+					auto const* expr = dynamic_cast<Expression const*>(scope);
+					solAssert(expr, "");
+					auto const* intType = dynamic_cast<IntegerType const*>(expr->annotation().type);
+					if (!intType)
+						intType = TypeProvider::uint256();
+
+					satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")";
+					satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")";
+					if (target.type == VerificationTarget::Type::Underflow)
+					{
+						satMsg = satMsgUnderflow + " happens here.";
+						unknownMsg = satMsgUnderflow + " might happen here.";
+						errorReporterId = underflowErrorId;
+					}
+					else if (target.type == VerificationTarget::Type::Overflow)
+					{
+						satMsg = satMsgOverflow + " happens here.";
+						unknownMsg = satMsgOverflow + " might happen here.";
+						errorReporterId = overflowErrorId;
+					}
+				}
+				else if (target.type == VerificationTarget::Type::DivByZero)
+				{
+					satMsg = "Division by zero happens here.";
+					unknownMsg = "Division by zero might happen here.";
+					errorReporterId = 4281_error;
+				}
+				else
+					solAssert(false, "");
+
+				auto it = m_errorIds.find(scope->id());
 				solAssert(it != m_errorIds.end(), "");
-				specificTarget.type = VerificationTarget::Type::Overflow;
-				checkAndReportTarget(scope, specificTarget, it->second, overflowErrorId, satMsgOverflow + " happens here.", satMsgOverflow + " might happen here.");
+				solAssert(i < it->second.size(), "");
+				unsigned errorId = it->second[i];
+
+				checkAndReportTarget(scope, target, errorId, errorReporterId, satMsg, unknownMsg);
 			}
 		}
 	}
@@ -1268,7 +1234,8 @@ void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const&
 	{
 		auto it = m_errorIds.find(assertion->id());
 		solAssert(it != m_errorIds.end(), "");
-		unsigned errorId = it->second;
+		solAssert(!it->second.empty(), "");
+		unsigned errorId = it->second[0];
 
 		checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here.", "Assertion violation might happen here.");
 	}
@@ -1464,7 +1431,7 @@ unsigned CHC::newErrorId(frontend::Expression const& _expr)
 	// because error id zero actually means no error in the CHC encoding.
 	if (errorId == 0)
 		errorId = m_context.newUniqueId();
-	m_errorIds.emplace(_expr.id(), errorId);
+	m_errorIds[_expr.id()].push_back(errorId);
 	return errorId;
 }
 
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
index b47043781..0bae37084 100644
--- a/libsolidity/formal/CHC.h
+++ b/libsolidity/formal/CHC.h
@@ -183,6 +183,7 @@ private:
 
 	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
 	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _errorId);
+	void addVerificationTarget(frontend::Expression const& _scope, VerificationTarget::Type _type, smtutil::Expression const& _target);
 	void addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
 
 	void checkVerificationTargets();
@@ -277,7 +278,9 @@ private:
 		smtutil::Expression errorId;
 	};
 
-	std::map<ASTNode const*, CHCVerificationTarget, IdCompare> m_verificationTargets;
+	/// Verification targets corresponding to ASTNodes. There can be multiple targets for a single ASTNode,
+	/// e.g., divByZero and Overflow for signed division.
+	std::map<ASTNode const*, std::vector<CHCVerificationTarget>, IdCompare> m_verificationTargets;
 
 	/// Targets proven safe.
 	std::map<ASTNode const*, std::set<VerificationTarget::Type>> m_safeTargets;
@@ -294,9 +297,8 @@ private:
 	std::map<ASTNode const*, std::set<Expression const*>, IdCompare> m_functionAssertions;
 
 	/// Maps ASTNode ids to error ids.
-	/// A multimap is used instead of map anticipating the UnderOverflow
-	/// target which has 2 error ids.
-	std::multimap<unsigned, unsigned> m_errorIds;
+	/// There can be multiple errorIds associated with a single ASTNode.
+	std::map<unsigned, std::vector<unsigned>> m_errorIds;
 
 	/// The current block.
 	smtutil::Expression m_currentBlock = smtutil::Expression(true);
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 9092e417c..c114b75be 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -787,7 +787,6 @@ void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
 	auto x = expr(*args.at(0));
 	auto y = expr(*args.at(1));
 	auto k = expr(*args.at(2));
-	m_context.addAssertion(k != 0);
 	auto const& intType = dynamic_cast<IntegerType const&>(*_funCall.annotation().type);
 
 	if (kind == FunctionType::Kind::AddMod)
@@ -1532,8 +1531,6 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 
 	if (_op == Token::Div || _op == Token::Mod)
 	{
-		m_context.addAssertion(_right != 0);
-
 		// mod and unsigned division never underflow/overflow
 		if (_op == Token::Mod || !intType->isSigned())
 			return {valueUnbounded, valueUnbounded};
@@ -1744,13 +1741,15 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
 	m_context.addAssertion(((d.currentValue() * _right) + r.currentValue()) == _left);
 	if (_type.isSigned())
 		m_context.addAssertion(
-			(_left >= 0 && 0 <= r.currentValue() && r.currentValue() < smtutil::abs(_right)) ||
-			(_left < 0 && (0 - smtutil::abs(_right)) < r.currentValue() && r.currentValue() <= 0)
+			(_left >= 0 && 0 <= r.currentValue() && (_right == 0 || r.currentValue() < smtutil::abs(_right))) ||
+			(_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r.currentValue()) && r.currentValue() <= 0))
 		);
 	else // unsigned version
-		m_context.addAssertion(0 <= r.currentValue() && r.currentValue() < _right);
+		m_context.addAssertion(0 <= r.currentValue() && (_right == 0 || r.currentValue() < _right));
 
-	return {d.currentValue(), r.currentValue()};
+	auto divResult = smtutil::Expression::ite(_right == 0, 0, d.currentValue());
+	auto modResult = smtutil::Expression::ite(_right == 0, 0, r.currentValue());
+	return {divResult, modResult};
 }
 
 void SMTEncoder::assignment(
diff --git a/scripts/error_codes.py b/scripts/error_codes.py
index 100c0c0be..ad0374a76 100755
--- a/scripts/error_codes.py
+++ b/scripts/error_codes.py
@@ -222,10 +222,10 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
     old_source_only_ids = {
         "1123", "1133", "1218", "1220", "1584", "1823", "1950",
         "1988", "2418", "2461", "2512", "2592", "2657", "2800", "2842", "2856",
-        "3263", "3356", "3441", "3682", "3876",
+        "3046", "3263", "3356", "3441", "3682", "3876",
         "3893", "4010", "4281", "4802", "4805", "4828",
         "4904", "4990", "5052", "5073", "5170", "5188", "5272", "5347", "5473",
-        "5622", "6041", "6052", "6272", "6708", "6792", "6931", "7110", "7128", "7186",
+        "5622", "6041", "6052", "6084", "6272", "6708", "6792", "6931", "7110", "7128", "7186",
         "7589", "7593", "7653", "7812", "7885", "8065", "8084", "8140",
         "8261", "8312", "8592", "8758", "9011",
         "9085", "9390", "9440", "9547", "9551", "9615", "9980"
diff --git a/test/libsolidity/smtCheckerTests/math/addmod_1.sol b/test/libsolidity/smtCheckerTests/math/addmod_1.sol
index a4ebed099..ae669c90d 100644
--- a/test/libsolidity/smtCheckerTests/math/addmod_1.sol
+++ b/test/libsolidity/smtCheckerTests/math/addmod_1.sol
@@ -12,5 +12,6 @@ contract C {
 	}
 }
 // ----
-// Warning 3046: (141-166): BMC: Division by zero happens here.
-// Warning 3046: (263-278): BMC: Division by zero happens here.
+// Warning 4281: (141-166): CHC: Division by zero happens here.
+// Warning 6328: (170-184): CHC: Assertion violation happens here.
+// Warning 4281: (263-278): CHC: Division by zero happens here.
diff --git a/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol b/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol
index 84c6e4698..1d73d60f4 100644
--- a/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol
+++ b/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol
@@ -22,5 +22,7 @@ contract C {
 }
 // ----
 // Warning 6321: (253-260): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
-// Warning 3046: (94-109): BMC: Division by zero happens here.
-// Warning 3046: (180-195): BMC: Division by zero happens here.
+// Warning 4281: (94-109): CHC: Division by zero happens here.
+// Warning 6328: (113-126): CHC: Assertion violation happens here.
+// Warning 4281: (180-195): CHC: Division by zero happens here.
+// Warning 6328: (199-212): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/math/mulmod_1.sol b/test/libsolidity/smtCheckerTests/math/mulmod_1.sol
index d75e6d267..ce9efdce5 100644
--- a/test/libsolidity/smtCheckerTests/math/mulmod_1.sol
+++ b/test/libsolidity/smtCheckerTests/math/mulmod_1.sol
@@ -12,5 +12,6 @@ contract C {
 	}
 }
 // ----
-// Warning 3046: (141-166): BMC: Division by zero happens here.
-// Warning 3046: (263-278): BMC: Division by zero happens here.
+// Warning 4281: (141-166): CHC: Division by zero happens here.
+// Warning 6328: (170-184): CHC: Assertion violation happens here.
+// Warning 4281: (263-278): CHC: Division by zero happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/div_zero.sol b/test/libsolidity/smtCheckerTests/operators/div_zero.sol
index b11b82d0e..b6fb4ed19 100644
--- a/test/libsolidity/smtCheckerTests/operators/div_zero.sol
+++ b/test/libsolidity/smtCheckerTests/operators/div_zero.sol
@@ -5,4 +5,4 @@ contract C {
 	uint x = 2 / z;
 }
 // ----
-// Warning 6084: (69-74): BMC: Division by zero happens here.
+// Warning 4281: (69-74): CHC: Division by zero happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/division_1.sol b/test/libsolidity/smtCheckerTests/operators/division_1.sol
index 99b36e480..87455a4e5 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_1.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_1.sol
@@ -5,4 +5,4 @@ contract C {
 	}
 }
 // ----
-// Warning 3046: (111-116): BMC: Division by zero happens here.
+// Warning 4281: (111-116): CHC: Division by zero happens here.
diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
index a3ef63779..77d9a4847 100644
--- a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
@@ -6,5 +6,5 @@ contract C  {
 	}
 }
 // ----
+// Warning 4281: (110-115): CHC: Division by zero happens here.
 // Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
-// Warning 3046: (110-115): BMC: Division by zero happens here.
diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_mod_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_mod_overflow.sol
index df275044b..7cb939586 100644
--- a/test/libsolidity/smtCheckerTests/overflow/signed_mod_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/overflow/signed_mod_overflow.sol
@@ -6,4 +6,4 @@ contract C  {
 	}
 }
 // ----
-// Warning 3046: (110-115): BMC: Division by zero happens here.
+// Warning 4281: (110-115): CHC: Division by zero happens here.
diff --git a/test/libsolidity/smtCheckerTests/overflow/unsigned_div_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/unsigned_div_overflow.sol
index e8a5dc76a..7005fd1b5 100644
--- a/test/libsolidity/smtCheckerTests/overflow/unsigned_div_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/overflow/unsigned_div_overflow.sol
@@ -6,4 +6,4 @@ contract C  {
 	}
 }
 // ----
-// Warning 3046: (113-118): BMC: Division by zero happens here.
+// Warning 4281: (113-118): CHC: Division by zero happens here.
diff --git a/test/libsolidity/smtCheckerTests/overflow/unsigned_mod_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/unsigned_mod_overflow.sol
index 59bb034c5..3019baa6f 100644
--- a/test/libsolidity/smtCheckerTests/overflow/unsigned_mod_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/overflow/unsigned_mod_overflow.sol
@@ -6,4 +6,4 @@ contract C  {
 	}
 }
 // ----
-// Warning 3046: (113-118): BMC: Division by zero happens here.
+// Warning 4281: (113-118): CHC: Division by zero happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol
index ea645ccaf..add65c141 100644
--- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol
+++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol
@@ -6,4 +6,4 @@ contract C {
 	}
 }
 // ----
-// Warning 3046: (117-120): BMC: Division by zero happens here.
+// Warning 4281: (117-120): CHC: Division by zero happens here.

From b087fa975072bd214aba3b75b578092ebee39411 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 19 Oct 2020 21:46:15 +0100
Subject: [PATCH 09/10] [SMTChecker] Fix ICE implicit conversion string literal
 -> byte

---
 Changelog.md                                  |  1 +
 libsolidity/formal/SMTEncoder.cpp             | 28 ++++++++++++++-----
 libsolidity/formal/SMTEncoder.h               |  5 ++++
 .../smtCheckerTests/operators/slice_bytes.sol |  6 ++++
 .../implicit_cast_string_literal_byte.sol     | 16 +++++++++++
 ...string_literal_to_fixed_bytes_explicit.sol |  4 +++
 6 files changed, 53 insertions(+), 7 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/operators/slice_bytes.sol
 create mode 100644 test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol
 create mode 100644 test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_explicit.sol

diff --git a/Changelog.md b/Changelog.md
index f02123341..176137b31 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -5,6 +5,7 @@ Compiler Features:
 
 Bugfixes:
  * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.
+ * SMTChecker: Fix internal error on conversion from string literal to byte.
  * Code generator: Fix missing creation dependency tracking for abstract contracts.
 
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index c114b75be..4e338ab5d 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -878,10 +878,8 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
 	if (argSize == castSize)
 	{
 		// If sizes are the same, it's possible that the signs are different.
-		if (smt::isNumber(*funCallType))
+		if (smt::isNumber(*funCallType) && smt::isNumber(*argType))
 		{
-			solAssert(smt::isNumber(*argType), "");
-
 			// castIsSigned && !argIsSigned => might overflow if arg > castType.max
 			// !castIsSigned && argIsSigned => might underflow if arg < castType.min
 			// !castIsSigned && !argIsSigned => ok
@@ -1211,9 +1209,10 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 
 	auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
 	solAssert(arrayVar, "");
+	TypePointer baseType = _indexAccess.baseExpression().annotation().type;
 	defineExpr(_indexAccess, smtutil::Expression::select(
 		arrayVar->elements(),
-		expr(*_indexAccess.indexExpression())
+		expr(*_indexAccess.indexExpression(), keyType(baseType))
 	));
 	setSymbolicUnknownValue(
 		expr(_indexAccess),
@@ -1245,17 +1244,19 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
 			auto const& base = indexAccess->baseExpression();
 			if (dynamic_cast<Identifier const*>(&base))
 				base.accept(*this);
+
+			TypePointer baseType = base.annotation().type;
+			auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType));
 			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base));
 			solAssert(symbArray, "");
-			auto baseType = symbArray->type();
 			toStore = smtutil::Expression::tuple_constructor(
 				smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
-				{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
+				{smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()}
 			);
 			m_context.expression(*indexAccess)->increaseIndex();
 			defineExpr(*indexAccess, smtutil::Expression::select(
 				symbArray->elements(),
-				expr(*indexAccess->indexExpression())
+				indexExpr
 			));
 			lastExpr = &indexAccess->baseExpression();
 		}
@@ -2239,6 +2240,19 @@ Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
 	return base;
 }
 
+TypePointer SMTEncoder::keyType(TypePointer _type)
+{
+	if (auto const* mappingType = dynamic_cast<MappingType const*>(_type))
+		return mappingType->keyType();
+	if (
+		dynamic_cast<ArrayType const*>(_type) ||
+		dynamic_cast<ArraySliceType const*>(_type)
+	)
+		return TypeProvider::uint256();
+	else
+		solAssert(false, "");
+}
+
 Expression const* SMTEncoder::innermostTuple(Expression const& _expr)
 {
 	auto const* tuple = dynamic_cast<TupleExpression const*>(&_expr);
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 1fe4e1dcd..fb563412f 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -55,6 +55,11 @@ public:
 	/// @returns the leftmost identifier in a multi-d IndexAccess.
 	static Expression const* leftmostBase(IndexAccess const& _indexAccess);
 
+	/// @returns the key type in _type.
+	/// _type must allow IndexAccess, that is,
+	/// it must be either ArrayType or MappingType
+	static TypePointer keyType(TypePointer _type);
+
 	/// @returns the innermost element in a chain of 1-tuples if applicable,
 	/// otherwise _expr.
 	static Expression const* innermostTuple(Expression const& _expr);
diff --git a/test/libsolidity/smtCheckerTests/operators/slice_bytes.sol b/test/libsolidity/smtCheckerTests/operators/slice_bytes.sol
new file mode 100644
index 000000000..d52106e6b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/slice_bytes.sol
@@ -0,0 +1,6 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(bytes calldata b) external pure {
+		((b[:])[5]);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol b/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol
new file mode 100644
index 000000000..382078ea3
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol
@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (byte => uint) map;
+	function f() public {
+		map[""] = 2;
+		uint x = map[""];
+		g("");
+		byte b = "";
+		assert(x == map[b]);
+		assert(x == map["x"]);
+	}
+	function g(byte b) internal pure {}
+}
+// ----
+// Warning 6328: (182-203): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_explicit.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_explicit.sol
new file mode 100644
index 000000000..8c454474b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_explicit.sol
@@ -0,0 +1,4 @@
+pragma experimental SMTChecker;
+contract SMT {
+	bytes32 constant internal NULL_BYTES32 = bytes32('');
+}

From ade3b9951c4681e20d24bb3ed8f29dcab605ff6f Mon Sep 17 00:00:00 2001
From: Martin Blicha <blichm@usi.ch>
Date: Wed, 21 Oct 2020 17:57:34 +0200
Subject: [PATCH 10/10] [SMTChecker] Added support for selector when
 expression's value is known at compile time

---
 Changelog.md                                  |  2 +
 libsolidity/formal/SMTEncoder.cpp             | 10 ++++
 .../function_selector_via_contract_name.sol   | 20 ++++++++
 .../function_selector/function_types_sig.sol  | 31 +++++++++++++
 .../function_selector/homer.sol               | 46 +++++++++++++++++++
 .../function_selector/selector.sol            |  8 ++++
 .../function_selector/selector_2.sol          | 12 +++++
 .../function_selector/selector_3.sol          | 14 ++++++
 8 files changed, 143 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/function_selector/function_selector_via_contract_name.sol
 create mode 100644 test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol
 create mode 100644 test/libsolidity/smtCheckerTests/function_selector/homer.sol
 create mode 100644 test/libsolidity/smtCheckerTests/function_selector/selector.sol
 create mode 100644 test/libsolidity/smtCheckerTests/function_selector/selector_2.sol
 create mode 100644 test/libsolidity/smtCheckerTests/function_selector/selector_3.sol

diff --git a/Changelog.md b/Changelog.md
index 176137b31..9c5ea16ea 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -2,6 +2,8 @@
 
 Compiler Features:
  * SMTChecker: Add division by zero checks in the CHC engine.
+ * SMTChecker: Support ``selector`` for expressions with value known at compile-time.
+
 
 Bugfixes:
  * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 4e338ab5d..efd712644 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1145,6 +1145,16 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 		}
 		return false;
 	}
+	else if (
+		auto const* functionType = dynamic_cast<FunctionType const*>(exprType);
+		functionType &&
+		_memberAccess.memberName() == "selector" &&
+		functionType->hasDeclaration()
+	)
+	{
+		defineExpr(_memberAccess, functionType->externalIdentifier());
+		return false;
+	}
 	else
 		m_errorReporter.warning(
 			7650_error,
diff --git a/test/libsolidity/smtCheckerTests/function_selector/function_selector_via_contract_name.sol b/test/libsolidity/smtCheckerTests/function_selector/function_selector_via_contract_name.sol
new file mode 100644
index 000000000..a1690519d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/function_selector/function_selector_via_contract_name.sol
@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract A {
+    function f() external {}
+    function g(uint256) external {}
+}
+contract B {
+    function f() external returns (uint256) {}
+    function g(uint256) external returns (uint256) {}
+}
+contract C {
+    function test1() external pure returns(bytes4, bytes4, bytes4, bytes4) {
+        return (A.f.selector, A.g.selector, B.f.selector, B.g.selector);
+    }
+    function test2() external pure returns(bytes4, bytes4, bytes4, bytes4) {
+        A a; B b;
+        return (a.f.selector, a.g.selector, b.f.selector, b.g.selector);
+    }
+}
+// ====
diff --git a/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol b/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol
new file mode 100644
index 000000000..b49c3ac51
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol
@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+
+contract C {
+    uint256 public x;
+
+    function f() public pure returns (bytes4) {
+        return this.f.selector;
+    }
+
+    function g() public view returns (bytes4) {
+        function () pure external returns (bytes4) fun = this.f;
+        return fun.selector;
+    }
+
+    function i() public pure returns (bytes4) {
+        return this.x.selector;
+    }
+
+    function check() public view {
+        assert(f() == 0x26121ff0);
+        assert(g() == 0x26121ff0);
+        assert(i() == 0x0c55699c);
+        assert(i() == 0x26121ff0);
+    }
+}
+// ----
+// Warning 6328: (470-495): CHC: Assertion violation happens here.
+// Warning 6328: (540-565): CHC: Assertion violation happens here.
+// Warning 6031: (261-267): Internal error: Expression undefined for SMT solver.
+// Warning 7650: (284-296): Assertion checker does not yet support this expression.
+// Warning 7650: (284-296): Assertion checker does not yet support this expression.
diff --git a/test/libsolidity/smtCheckerTests/function_selector/homer.sol b/test/libsolidity/smtCheckerTests/function_selector/homer.sol
new file mode 100644
index 000000000..a858a7714
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/function_selector/homer.sol
@@ -0,0 +1,46 @@
+pragma experimental SMTChecker;
+
+interface ERC165 {
+    /// @notice Query if a contract implements an interface
+    /// @param interfaceID The interface identifier, as specified in ERC-165
+    /// @dev Interface identification is specified in ERC-165. This function
+    ///  uses less than 30,000 gas.
+    /// @return `true` if the contract implements `interfaceID` and
+    ///  `interfaceID` is not 0xffffffff, `false` otherwise
+    function supportsInterface(bytes4 interfaceID) external view returns (bool);
+}
+
+interface Simpson {
+    function is2D() external returns (bool);
+    function skinColor() external returns (string memory);
+}
+
+interface PeaceMaker {
+    function achieveWorldPeace() external;
+}
+
+contract Homer is ERC165, Simpson {
+    function supportsInterface(bytes4 interfaceID) public pure override returns (bool) {
+        return
+            interfaceID == this.supportsInterface.selector || // ERC165
+            interfaceID == this.is2D.selector ^ this.skinColor.selector; // Simpson
+    }
+
+    function is2D() external pure override returns (bool) {
+        return true;
+    }
+
+    function skinColor() external pure override returns (string memory) {
+        return "yellow";
+    }
+
+    function check() public pure {
+        assert(supportsInterface(type(Simpson).interfaceId));
+        assert(supportsInterface(type(ERC165).interfaceId));
+        assert(supportsInterface(type(PeaceMaker).interfaceId));
+    }
+}
+
+
+// ----
+// Warning 6328: (1373-1428): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/function_selector/selector.sol b/test/libsolidity/smtCheckerTests/function_selector/selector.sol
new file mode 100644
index 000000000..b1339ed54
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/function_selector/selector.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f() public pure {
+        assert(msg.sig == this.f.selector);
+    }
+}
+// ----
diff --git a/test/libsolidity/smtCheckerTests/function_selector/selector_2.sol b/test/libsolidity/smtCheckerTests/function_selector/selector_2.sol
new file mode 100644
index 000000000..beaf88465
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/function_selector/selector_2.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function g() external pure {
+    }
+
+    function f() public pure {
+        assert(msg.sig == this.g.selector);
+    }
+}
+// ----
+// Warning 6328: (125-159): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/function_selector/selector_3.sol b/test/libsolidity/smtCheckerTests/function_selector/selector_3.sol
new file mode 100644
index 000000000..072113553
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/function_selector/selector_3.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+
+contract C {
+    int public x;
+    int public y;
+
+    function f() public pure {
+        assert(this.x.selector != this.y.selector);
+        assert(this.x.selector == this.y.selector);
+    }
+}
+// ----
+// Warning 6328: (175-217): CHC: Assertion violation happens here.