From a7f6a4bee644caee42780f55a9ee262c22bc3e11 Mon Sep 17 00:00:00 2001
From: Daniel Kirchner <daniel@ekpyron.org>
Date: Wed, 13 May 2020 18:09:48 +0200
Subject: [PATCH 1/4] Update PPA scripts.

---
 scripts/deps-ppa/static_z3.sh | 14 +++++---------
 scripts/release_ppa.sh        |  6 +++---
 2 files changed, 8 insertions(+), 12 deletions(-)

diff --git a/scripts/deps-ppa/static_z3.sh b/scripts/deps-ppa/static_z3.sh
index 7eb461821..c5f6d6ea4 100755
--- a/scripts/deps-ppa/static_z3.sh
+++ b/scripts/deps-ppa/static_z3.sh
@@ -25,11 +25,9 @@ set -ev
 keyid=70D110489D66E2F6
 email=builds@ethereum.org
 packagename=libz3-static-dev
-# On the next version the git cherry-pick below should be removed and the patch suffix removed from the version string.
-version=4.8.7
-version_patchsuffix=-1
+version=4.8.8
 
-DISTRIBUTIONS="bionic disco eoan focal"
+DISTRIBUTIONS="bionic eoan focal"
 
 for distribution in $DISTRIBUTIONS
 do
@@ -44,10 +42,8 @@ ppafilesurl=https://launchpad.net/~ethereum/+archive/ubuntu/${pparepo}/+files
 # Fetch source
 git clone --branch z3-${version} https://github.com/Z3Prover/z3.git
 cd z3
-# Patch build failure.
-git cherry-pick e212159f4e
 
-debversion="${version}${version_patchsuffix}"
+debversion="${version}"
 
 CMAKE_OPTIONS="-DZ3_BUILD_LIBZ3_SHARED=OFF -DCMAKE_BUILD_TYPE=Release"
 
@@ -181,7 +177,7 @@ This program is free software: you can redistribute it and/or modify
  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-2ubuntu0) saucy; urgency=low
+libz3-static-dev (0.0.1-1ubuntu0) saucy; urgency=low
 
   * Initial release.
 
@@ -191,7 +187,7 @@ mkdir debian/source
 echo "3.0 (quilt)" > debian/source/format
 chmod +x debian/rules
 
-versionsuffix=2ubuntu0~${distribution}
+versionsuffix=1ubuntu0~${distribution}
 EMAIL="$email" dch -v 1:${debversion}-${versionsuffix} "build of ${version}"
 
 # build source package
diff --git a/scripts/release_ppa.sh b/scripts/release_ppa.sh
index d84b3fd36..6d50e0066 100755
--- a/scripts/release_ppa.sh
+++ b/scripts/release_ppa.sh
@@ -55,9 +55,9 @@ keyid=70D110489D66E2F6
 email=builds@ethereum.org
 packagename=solc
 
-static_build_distribution=disco
+static_build_distribution=focal
 
-DISTRIBUTIONS="bionic disco eoan focal"
+DISTRIBUTIONS="bionic eoan focal"
 
 if is_release
 then
@@ -85,7 +85,7 @@ else
     fi
     if [ $distribution = focal ]
     then
-        SMTDEPENDENCY="libz3-dev,
+        SMTDEPENDENCY="libz3-static-dev,
             libcvc4-dev,
             "
     elif [ $distribution = disco ]

From b56536aeb27ed892ea9960e7264f16337a395be8 Mon Sep 17 00:00:00 2001
From: Daniel Kirchner <daniel@ekpyron.org>
Date: Wed, 13 May 2020 18:16:21 +0200
Subject: [PATCH 2/4] Update Docker images.

---
 .circleci/config.yml                         | 4 ++--
 .circleci/docker/Dockerfile.ubuntu2004       | 5 ++++-
 .circleci/docker/Dockerfile.ubuntu2004.clang | 7 +++++--
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 49f78fa19..0620cd667 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -12,10 +12,10 @@ parameters:
     default: "4"
   ubuntu-2004-docker-image-rev:
     type: string
-    default: "1"
+    default: "2"
   ubuntu-2004-clang-docker-image-rev:
     type: string
-    default: "1"
+    default: "2"
   ubuntu-1604-clang-ossfuzz-docker-image-rev:
     type: string
     default: "2"
diff --git a/.circleci/docker/Dockerfile.ubuntu2004 b/.circleci/docker/Dockerfile.ubuntu2004
index d39025809..a021b6533 100644
--- a/.circleci/docker/Dockerfile.ubuntu2004
+++ b/.circleci/docker/Dockerfile.ubuntu2004
@@ -26,6 +26,9 @@ FROM buildpack-deps:focal AS base
 ARG DEBIAN_FRONTEND=noninteractive
 
 RUN set -ex; \
+        dist=$(grep DISTRIB_CODENAME /etc/lsb-release | cut -d= -f2); \
+        echo "deb http://ppa.launchpad.net/ethereum/cpp-build-deps/ubuntu $dist main" >> /etc/apt/sources.list ; \
+        apt-key adv --keyserver keyserver.ubuntu.com --recv-keys 1c52189c923f6ca9 ; \
 	apt-get update; \
 	apt-get install -qqy --no-install-recommends \
 		build-essential \
@@ -33,7 +36,7 @@ RUN set -ex; \
 		cmake ninja-build \
 		libboost-filesystem-dev libboost-test-dev libboost-system-dev \
 		libboost-program-options-dev \
-		libcvc4-dev z3 libz3-dev \
+		libcvc4-dev libz3-static-dev \
 		; \
 	apt-get install -qy python3-pip python3-sphinx; \
 	pip3 install codecov; \
diff --git a/.circleci/docker/Dockerfile.ubuntu2004.clang b/.circleci/docker/Dockerfile.ubuntu2004.clang
index f436c34b7..c8d057eb1 100644
--- a/.circleci/docker/Dockerfile.ubuntu2004.clang
+++ b/.circleci/docker/Dockerfile.ubuntu2004.clang
@@ -26,6 +26,9 @@ FROM buildpack-deps:focal AS base
 ARG DEBIAN_FRONTEND=noninteractive
 
 RUN set -ex; \
+	dist=$(grep DISTRIB_CODENAME /etc/lsb-release | cut -d= -f2); \
+	echo "deb http://ppa.launchpad.net/ethereum/cpp-build-deps/ubuntu $dist main" >> /etc/apt/sources.list ; \
+	apt-key adv --keyserver keyserver.ubuntu.com --recv-keys 1c52189c923f6ca9 ; \
 	apt-get update; \
 	apt-get install -qqy --no-install-recommends \
 		build-essential \
@@ -33,8 +36,8 @@ RUN set -ex; \
 		cmake ninja-build \
 		libboost-filesystem-dev libboost-test-dev libboost-system-dev \
 		libboost-program-options-dev \
-		clang llvm-dev \
-		z3 libz3-dev \
+		clang \
+		libz3-static-dev \
 		; \
 	rm -rf /var/lib/apt/lists/*
 

From 030390217393dbac1e78664b6b3f54accda2dca6 Mon Sep 17 00:00:00 2001
From: Daniel Kirchner <daniel@ekpyron.org>
Date: Thu, 14 May 2020 14:09:27 +0200
Subject: [PATCH 3/4] Update smt test expectations.

---
 .../loops/for_loop_array_assignment_storage_memory.sol          | 1 -
 .../loops/for_loop_array_assignment_storage_storage.sol         | 1 -
 .../loops/while_loop_array_assignment_storage_storage.sol       | 1 -
 .../operators/compound_assignment_division_1.sol                | 2 ++
 .../operators/compound_assignment_division_2.sol                | 2 ++
 .../operators/compound_assignment_division_3.sol                | 2 ++
 .../smtCheckerTests/operators/delete_array_index_2d.sol         | 1 -
 .../operators/division_truncates_correctly_1.sol                | 2 ++
 .../operators/division_truncates_correctly_2.sol                | 2 ++
 .../operators/division_truncates_correctly_3.sol                | 2 ++
 .../operators/division_truncates_correctly_4.sol                | 2 ++
 .../operators/division_truncates_correctly_5.sol                | 2 ++
 test/libsolidity/smtCheckerTests/operators/mod.sol              | 2 ++
 test/libsolidity/smtCheckerTests/operators/mod_even.sol         | 2 ++
 test/libsolidity/smtCheckerTests/operators/mod_n.sol            | 2 ++
 test/libsolidity/smtCheckerTests/operators/mod_n_uint16.sol     | 2 ++
 16 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol
index 0b301505b..2466e1efd 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol
@@ -19,5 +19,4 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning: (316-336): Assertion violation happens here
 // Warning: (363-382): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol
index 333273781..a90053024 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol
@@ -19,6 +19,5 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning: (317-337): Assertion violation happens here
 // Warning: (341-360): Assertion violation happens here
 // Warning: (364-383): Assertion violation happens 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 92d1ded3e..96f171054 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
@@ -21,6 +21,5 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning: (296-316): Assertion violation happens here
 // Warning: (320-339): Assertion violation happens here
 // Warning: (343-362): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol
index 2e07fc9c1..e3a8ea1fb 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol
@@ -9,4 +9,6 @@ contract C {
 	}
 }
 // ----
+// Warning: (129-143): Error trying to invoke SMT solver.
+// Warning: (147-161): Error trying to invoke SMT solver.
 // Warning: (147-161): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol
index f7c347047..83bd7cb6b 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol
@@ -10,4 +10,6 @@ contract C {
 	}
 }
 // ----
+// Warning: (163-184): Error trying to invoke SMT solver.
+// Warning: (188-209): Error trying to invoke SMT solver.
 // Warning: (188-209): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol
index 5b466f173..b941a5767 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol
@@ -10,4 +10,6 @@ contract C {
 	}
 }
 // ----
+// Warning: (171-190): Error trying to invoke SMT solver.
+// Warning: (194-213): Error trying to invoke SMT solver.
 // Warning: (194-213): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol
index 8a1ba5e6e..a47763c03 100644
--- a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol
+++ b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol
@@ -16,4 +16,3 @@ contract C
 // ====
 // SMTSolvers: z3
 // ----
-// Warning: (174-194): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol
index 6bbc56a40..b0ea1e34d 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol
@@ -6,3 +6,5 @@ contract C {
 		assert(x / y == 3);
 	}
 }
+// ----
+// Warning: (107-125): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol
index 6478e3298..e8afbdf59 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol
@@ -6,3 +6,5 @@ contract C {
 		assert(x / y == 3);
 	}
 }
+// ----
+// Warning: (105-123): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol
index 1e58d709a..81ab88a4e 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol
@@ -6,3 +6,5 @@ contract C {
 		assert(x / y == -3);
 	}
 }
+// ----
+// Warning: (106-125): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol
index 9f8452bb2..f6e6b57d1 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol
@@ -6,3 +6,5 @@ contract C {
 		assert(x / y == -3);
 	}
 }
+// ----
+// Warning: (106-125): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol
index 2ac471156..d93a508f3 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol
@@ -6,3 +6,5 @@ contract C {
 		assert(x / y == 3);
 	}
 }
+// ----
+// Warning: (107-125): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/mod.sol b/test/libsolidity/smtCheckerTests/operators/mod.sol
index 6a0730c01..358b52df2 100644
--- a/test/libsolidity/smtCheckerTests/operators/mod.sol
+++ b/test/libsolidity/smtCheckerTests/operators/mod.sol
@@ -8,3 +8,5 @@ contract C {
 		assert(z1 == z2);
 	}
 }
+// ----
+// Warning: (166-182): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/mod_even.sol b/test/libsolidity/smtCheckerTests/operators/mod_even.sol
index 184653eac..1bbdc38b7 100644
--- a/test/libsolidity/smtCheckerTests/operators/mod_even.sol
+++ b/test/libsolidity/smtCheckerTests/operators/mod_even.sol
@@ -8,3 +8,5 @@ contract C
 		assert((y % 2) == 0);
 	}
 }
+// ----
+// Warning: (122-142): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/mod_n.sol b/test/libsolidity/smtCheckerTests/operators/mod_n.sol
index 8df3ac4be..f4b1ee3e8 100644
--- a/test/libsolidity/smtCheckerTests/operators/mod_n.sol
+++ b/test/libsolidity/smtCheckerTests/operators/mod_n.sol
@@ -8,3 +8,5 @@ contract C
 		assert(z < y);
 	}
 }
+// ----
+// Warning: (126-139): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/mod_n_uint16.sol b/test/libsolidity/smtCheckerTests/operators/mod_n_uint16.sol
index fc6c7a8d6..9c4241f0b 100644
--- a/test/libsolidity/smtCheckerTests/operators/mod_n_uint16.sol
+++ b/test/libsolidity/smtCheckerTests/operators/mod_n_uint16.sol
@@ -8,3 +8,5 @@ contract C
 		assert(z < 100_000);
 	}
 }
+// ----
+// Warning: (130-149): Error trying to invoke SMT solver.

From af87d39bd67c79f78fdb2aae62616867be68e521 Mon Sep 17 00:00:00 2001
From: Daniel Kirchner <daniel@ekpyron.org>
Date: Thu, 14 May 2020 14:53:38 +0200
Subject: [PATCH 4/4] Update osx deps script.

---
 .circleci/osx_install_dependencies.sh | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/.circleci/osx_install_dependencies.sh b/.circleci/osx_install_dependencies.sh
index 2409cbad7..064680139 100755
--- a/.circleci/osx_install_dependencies.sh
+++ b/.circleci/osx_install_dependencies.sh
@@ -43,13 +43,13 @@ then
   ./scripts/install_obsolete_jsoncpp_1_7_4.sh
 
   # z3
-  wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.7/z3-4.8.7-x64-osx-10.14.6.zip
-  unzip z3-4.8.7-x64-osx-10.14.6.zip
-  rm -f z3-4.8.7-x64-osx-10.14.6.zip
-  cp z3-4.8.7-x64-osx-10.14.6/bin/libz3.a /usr/local/lib
-  cp z3-4.8.7-x64-osx-10.14.6/bin/z3 /usr/local/bin
-  cp z3-4.8.7-x64-osx-10.14.6/include/* /usr/local/include
-  rm -rf z3-4.8.7-x64-osx-10.14.6
+  wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-osx-10.14.6.zip
+  unzip z3-4.8.8-x64-osx-10.14.6.zip
+  rm -f z3-4.8.8-x64-osx-10.14.6.zip
+  cp z3-4.8.8-x64-osx-10.14.6/bin/libz3.a /usr/local/lib
+  cp z3-4.8.8-x64-osx-10.14.6/bin/z3 /usr/local/bin
+  cp z3-4.8.8-x64-osx-10.14.6/include/* /usr/local/include
+  rm -rf z3-4.8.8-x64-osx-10.14.6
 
   # evmone
   wget https://github.com/ethereum/evmone/releases/download/v0.4.0/evmone-0.4.0-darwin-x86_64.tar.gz