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

Tests: Disable checking CEX

Browse Source 
In this case I observed brittle behaviour with Z3, which behaved
differently on two equivalent queries with only variables renamed.
The reason for different versions was that in isoltest, we add version
pragma to the source code and this changes the ids of AST nodes. These
are in turn used to generate uniques names for SMT variables.
This commit is contained in:
Martin Blicha 2023-07-27 17:21:20 +02:00
parent 799f418bef
commit ecded11833
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
View File

@ -17,7 +17,7 @@ contract C {
} }
// ==== // ====
// SMTEngine: all // SMTEngine: all
// SMTIgnoreCex: no // SMTIgnoreCex: yes
// ---- // ----
// Warning 6328: (242-256): CHC: Assertion violation happens here.\nCounterexample:\na = [[], [], [0, 0, 0, 0]]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [[], [], [0, 0, 0, 0]]\nC.f() // Warning 6328: (242-256): CHC: Assertion violation happens here.\nCounterexample:\na = [[], [], [0, 0, 0, 0]]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [[], [], [0, 0, 0, 0]]\nC.f()
// Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.