From 937af7d72242adf8f83cfe979aa83923f505e912 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Thu, 12 Aug 2021 21:48:01 +0200 Subject: [PATCH] Fix SMT test --- .../external_calls/external_call_from_constructor_1.sol | 5 +++-- .../external_call_from_constructor_reentrancy_1.sol | 4 +++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol index 693f11d89..e02533bc1 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol @@ -14,6 +14,7 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // ---- -// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100) -// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f() +// Warning 6328: (69-85): CHC: Assertion violation happens here. +// Warning 6328: (177-191): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_reentrancy_1.sol index add1fc158..5dbdaae27 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_reentrancy_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_reentrancy_1.sol @@ -11,5 +11,7 @@ contract C { assert(a == 2); // should fail } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (253-267): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\nd = 0\na = 3\n\nTransaction trace:\nC.constructor(0) +// Warning 6328: (253-267): CHC: Assertion violation happens here.