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 #12722 from ethereum/smt_fix_nondet

Browse Source 
Ignore cex in SMT test
This commit is contained in:
chriseth 2022-03-01 12:26:48 +01:00 committed by GitHub
commit 5369bdc8fb
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
test/libsolidity/smtCheckerTests/userTypes/multisource_module.sol
View File

@ -16,6 +16,7 @@ contract C {
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// SMTIgnoreCex: yes
// ----
// Warning 6328: (s2.sol:259-292): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h()\n C.f(5) -- internal call\n C.f(5) -- internal call
// Warning 6328: (s2.sol:346-377): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h()\n C.f(5) -- internal call\n C.f(5) -- internal call\n C.g(1) -- internal call\n C.g(1) -- internal call
// Warning 6328: (s2.sol:259-292): CHC: Assertion violation happens here.
// Warning 6328: (s2.sol:346-377): CHC: Assertion violation happens here.