From 799f418befbaec8cb7580e5e6cc416f6b5f8f1b2 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Thu, 27 Jul 2023 16:22:55 +0200 Subject: [PATCH] Make counterexample deterministic --- .../smtCheckerTests/external_calls/call_mutex_unsafe.sol | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol index e8c17d3eb..6c7e7ac59 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol @@ -14,6 +14,7 @@ contract C { } function f(address _a) public { + require(x == 0); uint y = x; _a.call("aaaaa"); assert(y == x); // should fail @@ -23,5 +24,5 @@ contract C { // SMTEngine: all // SMTIgnoreCex: no // ---- -// Warning 9302: (212-228): Return value of low-level calls not used. -// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, lock = false\n_a = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.set(1)\nState: x = 1, lock = false\nC.f(0x0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(0) -- reentrant call +// Warning 9302: (231-247): Return value of low-level calls not used. +// Warning 6328: (251-265): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0x0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0x0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(1) -- reentrant call