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

Disable non-deterministic counterexamples in some SMT tests

Browse Source 
- The counterexamples sometimes do appear and the tests fail.
This commit is contained in:
Kamil Śliwak 2022-05-10 12:43:27 +02:00
parent 463e417508
commit 0e0d1972f9
2 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
View File

@ -11,6 +11,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// SMTIgnoreOS: macos
// ----
// Warning 4984: (82-85): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

1
test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol
View File

@ -18,6 +18,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (407-457): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n(true || true || true)\nReentrancy property(ies) for :C:\n(((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(1))) == 1)\n<errorCode> = 2 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(2))) == 2)\n<errorCode> = 3 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 0xff)\n<errorCode> = 4 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 1)\n