From a2588533e504c2a46827fe3ed87362f2bd7c4f32 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Wed, 24 Nov 2021 11:38:22 +0100
Subject: [PATCH] macos nondeterminism

---
 .../array_members/length_1d_struct_array_2d_1.sol                | 1 +
 .../libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol | 1 +
 .../smtCheckerTests/blockchain_state/balance_receive_4.sol       | 1 +
 .../blockchain_state/balance_receive_ext_calls.sol               | 1 +
 .../branches_with_return/branches_in_modifiers_2.sol             | 1 +
 .../control_flow/branches_with_return/triple_nested_if.sol       | 1 +
 .../external_calls/external_call_with_value_3.sol                | 1 +
 .../external_hash_known_code_state_reentrancy_unsafe.sol         | 1 +
 .../operators/assignment_module_contract_member_variable.sol     | 1 +
 .../smtCheckerTests/operators/compound_add_array_index.sol       | 1 +
 .../smtCheckerTests/operators/compound_add_mapping.sol           | 1 +
 .../smtCheckerTests/operators/compound_assignment_division_3.sol | 1 +
 .../smtCheckerTests/operators/compound_bitwise_or_int_1.sol      | 1 +
 .../libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol | 1 +
 .../libsolidity/smtCheckerTests/userTypes/multisource_module.sol | 1 +
 15 files changed, 15 insertions(+)

diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol
index 71571d944..ddda215df 100644
--- a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol
@@ -20,5 +20,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Info 1180: Contract invariant(s) for :C:\n!(s1.arr.length <= 0)\n!(s2.arr.length <= 0)\n(((s2.arr[0].length + ((- 1) * s1.arr[0].length)) <= 0) && ((s1.arr[0].length + ((- 1) * s2.arr[0].length)) <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
index 5920a4e74..0d16306b7 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
@@ -17,5 +17,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
index 3e3e56431..4fa420ff1 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
@@ -11,6 +11,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 4984: (82-85): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4984: (154-160): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol
index 1ee90e41d..96223b7e9 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol
@@ -12,6 +12,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (131-165): CHC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol
index 4241fa9e2..f08a26bf7 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol
@@ -42,6 +42,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()\n    C.reset_if_overflow() -- internal call
 // Warning 6328: (502-519): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\noldx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n    C.reset_if_overflow() -- internal call
diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/triple_nested_if.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/triple_nested_if.sol
index 09ee2b2b2..472ef8785 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/triple_nested_if.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/triple_nested_if.sol
@@ -17,5 +17,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Info 1180: Contract invariant(s) for :C:\n((c <= 0) && (a <= 0) && (b <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol
index d0e4c84aa..2a535329a 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol
@@ -12,6 +12,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (150-183): CHC: Assertion violation might happen here.
 // Warning 6328: (202-236): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    i.f{value: 20}() -- untrusted external call
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol
index d871d6e13..b3b43980a 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol
@@ -34,6 +34,7 @@ contract C {
 // ====
 // SMTEngine: all
 // SMTIgnoreCex: yes
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (348-362): CHC: Assertion violation happens here.
 // Warning 6328: (366-392): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol
index 18869ee3a..781476de2 100644
--- a/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol
+++ b/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol
@@ -27,6 +27,7 @@ contract A {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (AASource:159-178): CHC: Assertion violation happens here.\nCounterexample:\nx = (- 1), y = (- 2)\n\nTransaction trace:\nA.constructor()\nState: x = 0, y = 0\nA.a()\nState: x = (- 2), y = (- 2)\nA.a()
 // Warning 6328: (AASource:370-386): CHC: Assertion violation happens here.\nCounterexample:\nx = 8, y = (- 2)\n\nTransaction trace:\nA.constructor()\nState: x = 0, y = 0\nA.a()
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol b/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol
index 424baf927..1c6e205d3 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol
@@ -18,5 +18,6 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [299, 0]\nx = 99\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(99, 0)
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol b/test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol
index 4169357d1..ab133cefc 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol
@@ -11,5 +11,6 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (165-185): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol
index e762eb4be..aa90aa252 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol
@@ -10,5 +10,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (162-181): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(2, 0)
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
index 8f7c69b2c..fdd8c55cc 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
@@ -9,6 +9,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6368: (76-81): CHC: Out of bounds access might happen here.
 // Warning 6368: (76-84): CHC: Out of bounds access might happen here.
diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol
index 4c3682c60..95e3390b4 100644
--- a/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol
+++ b/test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol
@@ -19,5 +19,6 @@ contract C {
 }
 // ====
 // SMTEngine: chc
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (343-377): CHC: Assertion violation happens here.\nCounterexample:\ngas = 0, origin = 0x52f7\n\nTransaction trace:\nC.constructor()\nState: gas = 0, origin = 0x0\nC.f(){ tx.gasprice: 0, tx.origin: 0x52f7 }\n    C.g() -- internal call
diff --git a/test/libsolidity/smtCheckerTests/userTypes/multisource_module.sol b/test/libsolidity/smtCheckerTests/userTypes/multisource_module.sol
index ee3277d1b..491b8600d 100644
--- a/test/libsolidity/smtCheckerTests/userTypes/multisource_module.sol
+++ b/test/libsolidity/smtCheckerTests/userTypes/multisource_module.sol
@@ -15,6 +15,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (s2.sol:259-292): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h()\n    C.f(5) -- internal call\n    C.f(5) -- internal call
 // Warning 6328: (s2.sol:346-377): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h()\n    C.f(5) -- internal call\n    C.f(5) -- internal call\n    C.g(1) -- internal call\n    C.g(1) -- internal call