From ecded11833835955723d965d3f02a252022d0353 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Thu, 27 Jul 2023 17:21:20 +0200 Subject: [PATCH] Tests: Disable checking CEX 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. --- test/libsolidity/smtCheckerTests/functions/getters/array_2.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol index 2d92413d5..bf57291b9 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol @@ -17,7 +17,7 @@ contract C { } // ==== // 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() // Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.