From 7092caf6bf8741879d79acfd949cd4a865b3d4e4 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Tue, 15 Mar 2022 12:40:00 +0100
Subject: [PATCH] Adjust tests for nondeterminism

---
 .../external_call_from_constructor_1_trusted.sol               | 2 +-
 ...xternal_call_state_var_contract_inside_struct_trusted_2.sol | 1 +
 ...xternal_call_state_var_contract_inside_struct_trusted_3.sol | 3 ++-
 .../functions/getters/external_getter_this_1.sol               | 1 +
 .../functions/getters/external_getter_this_2.sol               | 1 +
 5 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol
index ef3b53a90..a9c45102a 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol
@@ -16,6 +16,6 @@ contract C {
 // SMTContract: C
 // SMTEngine: all
 // SMTExtCalls: trusted
+// SMTIgnoreInv: 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)
-// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_2.sol
index 731050262..59381960c 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_2.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_2.sol
@@ -19,5 +19,6 @@ contract C {
 // SMTEngine: chc
 // SMTExtCalls: trusted
 // SMTTargets: assert
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (179-199): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_3.sol
index 05425369f..06cd20cfe 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_3.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_struct_trusted_3.sol
@@ -22,5 +22,6 @@ contract C {
 // SMTEngine: chc
 // SMTExtCalls: trusted
 // SMTTargets: assert
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (205-227): CHC: Assertion violation happens here.\nCounterexample:\nt = {s: {d: 20819}}\n\nTransaction trace:\nC.constructor()\nState: t = {s: {d: 20819}}\nC.f()
+// Warning 6328: (205-227): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_1.sol
index 787f7f8a8..b7673203e 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_1.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_1.sol
@@ -13,5 +13,6 @@ contract C {
 // SMTEngine: chc
 // SMTExtCalls: trusted
 // SMTTargets: assert
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (127-141): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_2.sol
index 054c76082..b3dfe04ad 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_2.sol
@@ -14,5 +14,6 @@ contract C {
 // SMTEngine: chc
 // SMTExtCalls: trusted
 // SMTTargets: assert
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (138-152): CHC: Assertion violation happens here.