diff --git a/.circleci/config.yml b/.circleci/config.yml
index e4b4d0654..f6346c2d1 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -292,13 +292,13 @@ jobs:
           command: codecov --flags all --gcov-root build
       - store_artifacts: *artifacts_test_results
 
-  # Builds in C++17 mode and uses debug build in order to speed up.
+  # Builds in C++20 mode and uses debug build in order to speed up.
   # Do *NOT* store any artifacts or workspace as we don't run tests on this build.
-  b_ubu_cxx17:
+  b_ubu_cxx20:
     <<: *build_ubuntu1904
     environment:
       CMAKE_BUILD_TYPE: Debug
-      CMAKE_OPTIONS: -DCMAKE_TOOLCHAIN_FILE=cmake/toolchains/cxx17.cmake -DUSE_CVC4=OFF
+      CMAKE_OPTIONS: -DCMAKE_TOOLCHAIN_FILE=cmake/toolchains/cxx20.cmake -DUSE_CVC4=OFF
     steps:
       - checkout
       - run: *run_build
@@ -612,7 +612,7 @@ workflows:
       # build-only
       - b_docs: *workflow_trigger_on_tags
       - b_archlinux: *workflow_trigger_on_tags
-      - b_ubu_cxx17: *workflow_trigger_on_tags
+      - b_ubu_cxx20: *workflow_trigger_on_tags
       - b_ubu_ossfuzz: *workflow_trigger_on_tags
 
       # OS/X build and tests
diff --git a/.travis.yml b/.travis.yml
index 7e1114974..5754fa0a9 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -188,7 +188,7 @@ cache:
 
 install:
     - test $SOLC_INSTALL_DEPS_TRAVIS != On || (scripts/install_deps.sh)
-    - test "$TRAVIS_OS_NAME" != "linux" || (scripts/install_cmake.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
diff --git a/CMakeLists.txt b/CMakeLists.txt
index f3d724d26..a1927bf33 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,4 +1,4 @@
-cmake_minimum_required(VERSION 3.5.0)
+cmake_minimum_required(VERSION 3.9.0)
 
 set(ETH_CMAKE_DIR   "${CMAKE_CURRENT_LIST_DIR}/cmake"   CACHE PATH "The the path to the cmake directory")
 list(APPEND CMAKE_MODULE_PATH ${ETH_CMAKE_DIR})
@@ -13,11 +13,6 @@ eth_policy()
 set(PROJECT_VERSION "0.5.12")
 project(solidity VERSION ${PROJECT_VERSION} LANGUAGES C CXX)
 
-if (${CMAKE_VERSION} VERSION_LESS "3.9.0")
-	# needed for the big endian test for older cmake versions
-	enable_language(C)
-endif()
-
 include(TestBigEndian)
 TEST_BIG_ENDIAN(IS_BIG_ENDIAN)
 if (IS_BIG_ENDIAN)
diff --git a/cmake/jsoncpp.cmake b/cmake/jsoncpp.cmake
index 4ca8581dc..48cec7318 100644
--- a/cmake/jsoncpp.cmake
+++ b/cmake/jsoncpp.cmake
@@ -15,9 +15,9 @@ set(JSONCPP_INCLUDE_DIR "${prefix}/include")
 # versions used in the CI runs.
 if(EMSCRIPTEN)
     # Do not include all flags in CMAKE_CXX_FLAGS for emscripten,
-    # but only use -std=c++14. Using all flags causes build failures
+    # but only use -std=c++17. Using all flags causes build failures
     # at the moment.
-    set(JSONCPP_CXX_FLAGS -std=c++14)
+    set(JSONCPP_CXX_FLAGS -std=c++17)
 else()
     set(JSONCPP_CXX_FLAGS ${CMAKE_CXX_FLAGS})
 endif()
diff --git a/cmake/toolchains/cxx17.cmake b/cmake/toolchains/cxx17.cmake
deleted file mode 100644
index 04a865ebd..000000000
--- a/cmake/toolchains/cxx17.cmake
+++ /dev/null
@@ -1,4 +0,0 @@
-# Require C++17.
-set(CMAKE_CXX_STANDARD 17)
-set(CMAKE_CXX_STANDARD_REQUIRED TRUE)
-set(CMAKE_CXX_EXTENSIONS OFF)
diff --git a/cmake/toolchains/cxx20.cmake b/cmake/toolchains/cxx20.cmake
new file mode 100644
index 000000000..ad34e5749
--- /dev/null
+++ b/cmake/toolchains/cxx20.cmake
@@ -0,0 +1,4 @@
+# Require C++20.
+set(CMAKE_CXX_STANDARD 20) # This requires at least CMake 3.12 to understand this C++20 flag
+set(CMAKE_CXX_STANDARD_REQUIRED TRUE)
+set(CMAKE_CXX_EXTENSIONS OFF)
diff --git a/cmake/toolchains/default.cmake b/cmake/toolchains/default.cmake
index baf859b70..07fc80e8e 100644
--- a/cmake/toolchains/default.cmake
+++ b/cmake/toolchains/default.cmake
@@ -1,4 +1,4 @@
-# Require C++14.
-set(CMAKE_CXX_STANDARD 14)
+# Require C++17.
+set(CMAKE_CXX_STANDARD 17) # This requires at least CMake 3.8 to accept this C++17 flag.
 set(CMAKE_CXX_STANDARD_REQUIRED TRUE)
 set(CMAKE_CXX_EXTENSIONS OFF)
diff --git a/docs/installing-solidity.rst b/docs/installing-solidity.rst
index 2d8f257d4..ade678087 100644
--- a/docs/installing-solidity.rst
+++ b/docs/installing-solidity.rst
@@ -184,7 +184,7 @@ The following are dependencies for all builds of Solidity:
 +-----------------------------------+-------------------------------------------------------+
 | Software                          | Notes                                                 |
 +===================================+=======================================================+
-| `CMake`_ (version 3.5+)           | Cross-platform build file generator.                  |
+| `CMake`_ (version 3.9+)           | Cross-platform build file generator.                  |
 +-----------------------------------+-------------------------------------------------------+
 | `Boost`_  (version 1.65+)         | C++ libraries.                                        |
 +-----------------------------------+-------------------------------------------------------+
diff --git a/libdevcore/CMakeLists.txt b/libdevcore/CMakeLists.txt
index a092e3140..8bc3bb525 100644
--- a/libdevcore/CMakeLists.txt
+++ b/libdevcore/CMakeLists.txt
@@ -34,6 +34,6 @@ set(sources
 )
 
 add_library(devcore ${sources})
-target_link_libraries(devcore PUBLIC jsoncpp Boost::boost Boost::filesystem Boost::regex Boost::system Threads::Threads)
+target_link_libraries(devcore PUBLIC jsoncpp Boost::boost Boost::filesystem Boost::regex Boost::system)
 target_include_directories(devcore PUBLIC "${CMAKE_SOURCE_DIR}")
 add_dependencies(devcore solidity_BuildInfo.h)
diff --git a/scripts/deps-ppa/static_z3.sh b/scripts/deps-ppa/static_z3.sh
new file mode 100755
index 000000000..b971fdd24
--- /dev/null
+++ b/scripts/deps-ppa/static_z3.sh
@@ -0,0 +1,229 @@
+#!/usr/bin/env bash
+##############################################################################
+## This is used to package .deb packages and upload them to the launchpad
+## ppa servers for building.
+##
+## The gnupg key for "builds@ethereum.org" has to be present in order to sign
+## the package.
+##
+## It will clone the Z3 git from github on the specified version tag,
+## create a source archive and push it to the ubuntu ppa servers.
+##
+## This requires the following entries in /etc/dput.cf:
+##
+##  [cpp-build-deps]
+##  fqdn			= ppa.launchpad.net
+##  method			= ftp
+##  incoming		= ~ethereum/cpp-build-deps
+##  login			= anonymous
+
+##
+##############################################################################
+
+set -ev
+
+keyid=70D110489D66E2F6
+email=builds@ethereum.org
+packagename=libz3-static-dev
+version=4.8.5
+
+DISTRIBUTIONS="bionic disco"
+
+for distribution in $DISTRIBUTIONS
+do
+cd /tmp/
+rm -rf $distribution
+mkdir $distribution
+cd $distribution
+
+pparepo=cpp-build-deps
+ppafilesurl=https://launchpad.net/~ethereum/+archive/ubuntu/${pparepo}/+files
+
+# Fetch source
+git clone --depth 1 --branch Z3-${version} https://github.com/Z3Prover/z3.git
+cd z3
+debversion="$version"
+
+CMAKE_OPTIONS="-DBUILD_LIBZ3_SHARED=OFF -DCMAKE_BUILD_TYPE=Release"
+
+# gzip will create different tars all the time and we are not allowed
+# to upload the same file twice with different contents, so we only
+# create it once.
+if [ ! -e /tmp/${packagename}_${debversion}.orig.tar.gz ]
+then
+    tar --exclude .git -czf /tmp/${packagename}_${debversion}.orig.tar.gz .
+fi
+cp /tmp/${packagename}_${debversion}.orig.tar.gz ../
+
+# Create debian package information
+
+mkdir debian
+echo 9 > debian/compat
+# TODO: the Z3 packages have different build dependencies
+cat <<EOF > debian/control
+Source: libz3-static-dev
+Section: science
+Priority: extra
+Maintainer: Daniel Kirchner <daniel@ekpyron.org>
+Build-Depends: debhelper (>= 9.0.0),
+               cmake,
+               g++,
+               git,
+               libgmp-dev,
+               dh-python,
+               python
+Standards-Version: 3.9.6
+Homepage: https://github.com/Z3Prover/z3
+Vcs-Git: git://github.com/Z3Prover/z3.git
+Vcs-Browser: https://github.com/Z3Prover/z3
+
+Package: libz3-static-dev
+Section: libdevel
+Architecture: any-i386 any-amd64
+Multi-Arch: same
+Depends: \${shlibs:Depends}, \${misc:Depends}
+Description: theorem prover from Microsoft Research - development files (static library)
+ Z3 is a state-of-the art theorem prover from Microsoft Research. It can be
+ used to check the satisfiability of logical formulas over one or more
+ theories. Z3 offers a compelling match for software analysis and verification
+ tools, since several common software constructs map directly into supported
+ theories.
+ .
+ This package can be used to invoke Z3 via its C++ API.
+EOF
+cat <<EOF > debian/rules
+#!/usr/bin/make -f
+# -*- makefile -*-
+# Sample debian/rules that uses debhelper.
+#
+# This file was originally written by Joey Hess and Craig Small.
+# As a special exception, when this file is copied by dh-make into a
+# dh-make output file, you may use that output file without restriction.
+# This special exception was added by Craig Small in version 0.37 of dh-make.
+#
+# Modified to make a template file for a multi-binary package with separated
+# build-arch and build-indep targets  by Bill Allombert 2001
+
+# Uncomment this to turn on verbose mode.
+export DH_VERBOSE=1
+
+# This has to be exported to make some magic below work.
+export DH_OPTIONS
+
+
+%:
+	dh \$@ --buildsystem=cmake
+
+override_dh_auto_test:
+
+override_dh_shlibdeps:
+	dh_shlibdeps --dpkg-shlibdeps-params=--ignore-missing-info
+
+override_dh_auto_configure:
+	dh_auto_configure -- ${CMAKE_OPTIONS}
+
+override_dh_auto_install:
+	dh_auto_install --destdir debian/tmp
+EOF
+cat <<EOF > debian/libz3-static-dev.install
+usr/include/*
+usr/lib/*/libz3.a
+usr/lib/*/cmake/z3/*
+EOF
+cat <<EOF > debian/copyright
+Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+Upstream-Name: z3
+Source: https://github.com/Z3Prover/z3
+
+Files: *
+Copyright: Microsoft Corporation
+License: Expat
+ Permission is hereby granted, free of charge, to any person obtaining a copy of
+ this software and associated documentation files (the "Software"), to deal in
+ the Software without restriction, including without limitation the rights to
+ use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ of the Software, and to permit persons to whom the Software is furnished to do
+ so, subject to the following conditions:
+ .
+ The above copyright notice and this permission notice shall be included in all
+ copies or substantial portions of the Software.
+ .
+ THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ SOFTWARE.
+
+Files: debian/*
+Copyright: 2019 Ethereum
+License: GPL-3.0+
+This program 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.
+ .
+ This package 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 this program. If not, see <http://www.gnu.org/licenses/>.
+ .
+ On Debian systems, the complete text of the GNU General
+ Public License version 3 can be found in "/usr/share/common-licenses/GPL-3".
+EOF
+cat <<EOF > debian/changelog
+libz3-static-dev (0.0.1-0ubuntu1) saucy; urgency=low
+
+  * Initial release.
+
+ -- Daniel <daniel@ekpyron.org>  Mon, 03 Jun 2019 14:50:20 +0000
+EOF
+mkdir debian/source
+echo "3.0 (quilt)" > debian/source/format
+chmod +x debian/rules
+
+versionsuffix=0ubuntu1~${distribution}
+EMAIL="$email" dch -v 1:${debversion}-${versionsuffix} "build of ${version}"
+
+# build source package
+# If packages is rejected because original source is already present, add
+# -sd to remove it from the .changes file
+# -d disables the build dependencies check
+debuild -S -d -sa -us -uc
+
+# prepare .changes file for Launchpad
+sed -i -e s/UNRELEASED/${distribution}/ -e s/urgency=medium/urgency=low/ ../*.changes
+
+# check if ubuntu already has the source tarball
+(
+cd ..
+orig=${packagename}_${debversion}.orig.tar.gz
+orig_size=$(ls -l $orig | cut -d ' ' -f 5)
+orig_sha1=$(sha1sum $orig | cut -d ' ' -f 1)
+orig_sha256=$(sha256sum $orig | cut -d ' ' -f 1)
+orig_md5=$(md5sum $orig | cut -d ' ' -f 1)
+
+if wget --quiet -O $orig-tmp "$ppafilesurl/$orig"
+then
+    echo "[WARN] Original tarball found in Ubuntu archive, using it instead"
+    mv $orig-tmp $orig
+    new_size=$(ls -l *.orig.tar.gz | cut -d ' ' -f 5)
+    new_sha1=$(sha1sum $orig | cut -d ' ' -f 1)
+    new_sha256=$(sha256sum $orig | cut -d ' ' -f 1)
+    new_md5=$(md5sum $orig | cut -d ' ' -f 1)
+    sed -i -e s,$orig_sha1,$new_sha1,g -e s,$orig_sha256,$new_sha256,g -e s,$orig_size,$new_size,g -e s,$orig_md5,$new_md5,g *.dsc
+    sed -i -e s,$orig_sha1,$new_sha1,g -e s,$orig_sha256,$new_sha256,g -e s,$orig_size,$new_size,g -e s,$orig_md5,$new_md5,g *.changes
+fi
+)
+
+# sign the package
+debsign --re-sign -k ${keyid} ../${packagename}_${debversion}-${versionsuffix}_source.changes
+
+# upload
+dput ${pparepo} ../${packagename}_${debversion}-${versionsuffix}_source.changes
+
+done
diff --git a/scripts/install_cmake.sh b/scripts/install_cmake.sh
index e334b2c90..134b86f09 100755
--- a/scripts/install_cmake.sh
+++ b/scripts/install_cmake.sh
@@ -6,16 +6,18 @@
 
 set -e
 
-VERSION=3.7.1
-PREFIX=~/.local
+VERSION_MAJOR=3
+VERSION_MINOR=15
+VERSION_MICRO=2
+VERSION=$VERSION_MAJOR.$VERSION_MINOR.$VERSION_MICRO
+PREFIX="/usr/local"
 
 OS=$(uname -s)
 case $OS in
-Linux)  SHA256=7b4b7a1d9f314f45722899c0521c261e4bfab4a6b532609e37fef391da6bade2;;
-Darwin) SHA256=1851d1448964893fdc5a8c05863326119f397a3790e0c84c40b83499c7960267;;
+Linux)  SHA256=f8cbec2abc433938bd9378b129d1d288bb33b8b5a277afe19644683af6e32a59;;
+Darwin) SHA256=7ec056d641b8cbea98b220efdcc99da1991758a370063dcac3a0cd388d6b30b6;;
 esac
 
-
 BIN=$PREFIX/bin
 
 PATH=$PREFIX/bin:$PATH
@@ -24,7 +26,7 @@ if test -f $BIN/cmake && ($BIN/cmake --version | grep -q "$VERSION"); then
     echo "CMake $VERSION already installed in $BIN"
 else
     FILE=cmake-$VERSION-$OS-x86_64.tar.gz
-    URL=https://cmake.org/files/v3.7/$FILE
+    URL=https://cmake.org/files/v$VERSION_MAJOR.$VERSION_MINOR/$FILE
     ERROR=0
     TMPFILE=$(mktemp --tmpdir cmake-$VERSION-$OS-x86_64.XXXXXXXX.tar.gz)
     echo "Downloading CMake ($URL)..."
diff --git a/scripts/install_static_z3.sh b/scripts/install_static_z3.sh
new file mode 100644
index 000000000..7748fb1f3
--- /dev/null
+++ b/scripts/install_static_z3.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+git clone --depth 1 --branch z3-4.8.1 https://github.com/Z3Prover/z3.git
+cd z3
+mkdir build
+cd build
+LDFLAGS="-static" cmake -DBUILD_LIBZ3_SHARED=OFF ..
+make -j 4
+make install
\ No newline at end of file
diff --git a/scripts/release_ppa.sh b/scripts/release_ppa.sh
index 74daaa0b5..78ea3118b 100755
--- a/scripts/release_ppa.sh
+++ b/scripts/release_ppa.sh
@@ -83,8 +83,15 @@ else
     else
         pparepo=ethereum-dev
     fi
-    SMTDEPENDENCY="libcvc4-dev,
+    if [ $distribution = disco ]
+    then
+        SMTDEPENDENCY="libz3-static-dev,
+               libcvc4-dev,
                "
+    else
+        SMTDEPENDENCY="libz3-static-dev,
+               "
+    fi
     CMAKE_OPTIONS=""
 fi
 ppafilesurl=https://launchpad.net/~ethereum/+archive/ubuntu/${pparepo}/+files