cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Update to Z3 4.8.7

Browse Source
This commit is contained in:
Leonardo Alt 2019-12-03 00:24:04 +01:00
parent 361801b94c
commit 5337f58767
5 changed files with 35 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.circleci/config.yml
View File

@ -9,7 +9,7 @@ version: 2.1
parameters:
docker-image-rev:
type: string
default: "2"
default: "3"
defaults:

2
.circleci/docker/Dockerfile.clang.ubuntu1904
View File

@ -62,7 +62,7 @@ RUN git clone --recursive -b boost-1.69.0 https://github.com/boostorg/boost.git
rm -rf /usr/src/boost
# Z3
RUN git clone --depth 1 -b z3-4.8.6 https://github.com/Z3Prover/z3.git \
RUN git clone --depth 1 -b z3-4.8.7 https://github.com/Z3Prover/z3.git \
/usr/src/z3; \
cd /usr/src/z3; \
python scripts/mk_make.py --prefix=/usr ; \

14
.circleci/osx_install_dependencies.sh
View File

@ -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.6/z3-4.8.6-x64-osx-10.14.6.zip
unzip z3-4.8.6-x64-osx-10.14.6.zip
rm -f z3-4.8.6-x64-osx-10.14.6.zip
cp z3-4.8.6-x64-osx-10.14.6/bin/libz3.a /usr/local/lib
cp z3-4.8.6-x64-osx-10.14.6/bin/z3 /usr/local/bin
cp z3-4.8.6-x64-osx-10.14.6/include/* /usr/local/include
rm -rf z3-4.8.6-x64-osx-10.14.6
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
# evmone
wget https://github.com/ethereum/evmone/releases/download/v0.3.0/evmone-0.3.0-darwin-x86_64.tar.gz

19
test/libsolidity/smtCheckerTests/invariants/loop_array.sol
View File

@ -1,19 +0,0 @@
pragma experimental SMTChecker;
contract Simple {
uint[] a;
function f(uint n) public {
uint i;
while (i < n)
{
a[i] = i;
++i;
}
require(n > 1);
// Assertion is safe but current solver version cannot solve it.
// Keep test for next solver release.
assert(a[n-1] > a[n-2]);
}
}
// ----
// Warning: (273-296): Assertion violation happens here

26
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol Normal file
View File

@ -0,0 +1,26 @@
pragma experimental SMTChecker;
contract LoopFor2 {
uint[] b;
uint[] c;
function testUnboundedForLoop(uint n) public {
b[0] = 900;
uint[] storage a = b;
require(n > 0 && n < 100);
uint i;
while (i < n) {
b[i] = i + 1;
c[i] = b[i];
++i;
}
// Fails as false positive.
assert(b[0] == c[0]);
assert(a[0] == 900);
assert(b[0] == 900);
}
}
// ----
// Warning: (296-316): Assertion violation happens here
// Warning: (320-339): Assertion violation happens here
// Warning: (343-362): Assertion violation happens here