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

Merge pull request #9542 from ethereum/smt_add_test

Browse Source 
[SMTChecker] Add test from Aon blog post
This commit is contained in:
Alex Beregszaszi 2020-08-05 13:24:16 +01:00 committed by GitHub
commit dec0f86b83
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 47 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

47
test/libsolidity/smtCheckerTests/invariants/aon_blog_post.sol Normal file
View File

@ -0,0 +1,47 @@
pragma experimental SMTChecker;
contract C {
bool a;
bool b;
bool c;
bool d;
bool e;
bool f;
function press_A() public {
if(e) { a = true; } else { reset(); }
}
function press_B() public {
if(c) { b = true; } else { reset(); }
}
function press_C() public {
if(a) { c = true; } else { reset(); }
}
function press_D() public {
d = true;
}
function press_E() public {
if(d) { e = true; } else { reset(); }
}
function press_F() public {
if(b) { f = true; } else { reset(); }
}
function is_not_solved() view public {
// f = true can be reached by calling the functions
// press_D()
// press_E()
// press_A()
// press_C()
// press_B()
// press_F()
assert(!f);
}
function reset() internal {
a = false;
b = false;
c = false;
d = false;
e = false;
f = false;
}
}
// ----
// Warning 6328: (689-699): Assertion violation happens here