From 0a160b1ba0e82a0d133fff3f2c7fb0a8fd34d655 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Tue, 11 Aug 2020 15:53:24 +0200
Subject: [PATCH] Update remaining tests

---
 .../array_members/pop_2d_unsafe.sol                |  2 +-
 .../array_members/push_2d_arg_1_unsafe.sol         |  2 +-
 .../push_storage_ref_safe_aliasing.sol             |  2 +-
 .../complex/slither/const_state_variables.sol      |  3 +--
 .../control_flow/short_circuit_and.sol             |  1 -
 .../control_flow/short_circuit_and_fail.sol        |  1 -
 .../short_circuit_and_inside_branch.sol            |  1 -
 .../control_flow/short_circuit_and_need_both.sol   |  1 -
 .../short_circuit_and_need_both_fail.sol           |  1 -
 .../control_flow/short_circuit_or.sol              |  1 -
 .../control_flow/short_circuit_or_fail.sol         |  1 -
 .../short_circuit_or_inside_branch.sol             |  1 -
 .../control_flow/short_circuit_or_need_both.sol    |  1 -
 .../short_circuit_or_need_both_fail.sol            |  1 -
 .../functions/constructor_hierarchy_3.sol          |  4 ++--
 .../functions/constructor_hierarchy_4.sol          |  6 +++---
 .../functions/constructor_hierarchy_diamond.sol    |  5 ++---
 .../functions/constructor_hierarchy_diamond_2.sol  |  5 ++---
 .../functions/constructor_hierarchy_diamond_3.sol  | 10 +++-------
 ...nstructor_hierarchy_mixed_chain_with_params.sol |  3 +--
 .../constructor_state_value_parameter.sol          |  2 +-
 .../functions/internal_call_state_var_init_2.sol   |  3 ---
 .../smtCheckerTests/functions/library_constant.sol |  5 ++---
 ...nstructor_hierarchy_mixed_chain_with_params.sol |  3 +--
 ...nstructor_state_variable_init_chain_run_all.sol | 14 ++++++--------
 ...tructor_state_variable_init_chain_run_all_2.sol | 11 +++++------
 .../smtCheckerTests/loops/do_while_1_fail.sol      |  4 +---
 .../loops/do_while_1_false_positives.sol           |  5 -----
 .../smtCheckerTests/loops/for_1_fail.sol           |  1 +
 .../while_loop_array_assignment_memory_memory.sol  |  1 +
 .../while_loop_array_assignment_memory_storage.sol |  1 +
 .../modifiers/modifier_code_after_placeholder.sol  |  2 +-
 .../modifiers/modifier_overflow.sol                |  1 -
 .../smtCheckerTests/operators/division_3.sol       |  1 +
 .../smtCheckerTests/operators/division_4.sol       |  2 ++
 .../smtCheckerTests/operators/division_5.sol       |  2 ++
 .../smtCheckerTests/operators/division_6.sol       |  2 ++
 .../operators/division_truncates_correctly_2.sol   |  1 +
 .../operators/division_truncates_correctly_3.sol   |  1 +
 .../operators/division_truncates_correctly_4.sol   |  1 +
 .../operators/division_truncates_correctly_5.sol   |  1 +
 .../smtCheckerTests/operators/fixed_point_add.sol  |  3 +--
 .../operators/fixed_point_compound_add.sol         |  2 --
 .../smtCheckerTests/operators/mod_even.sol         |  1 +
 test/libsolidity/smtCheckerTests/special/many.sol  |  2 +-
 .../smtCheckerTests/types/address_balance.sol      |  2 +-
 .../types/tuple_declarations_function_2.sol        |  2 +-
 47 files changed, 53 insertions(+), 75 deletions(-)

diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
index 5d4bd3a97..2795dfe51 100644
--- a/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (111-121): Empty array "pop" detected here
+// Warning 2529: (111-121): Empty array "pop" detected here.
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
index c409a0e09..866cfe1eb 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
@@ -10,5 +10,5 @@ contract C {
 	}
 }
 // ----
+// Warning 3944: (162-177): Underflow (resulting value less than 0) happens here
 // Warning 6328: (150-184): Assertion violation happens here
-// Warning 4144: (162-177): Underflow (resulting value less than 0) happens here
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol
index 8192f673d..5fa9ef7d9 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol
@@ -12,5 +12,5 @@ contract C {
 	}
 }
 // ----
+// Warning 3944: (217-232): Underflow (resulting value less than 0) happens here
 // Warning 6328: (205-239): Assertion violation happens here
-// Warning 4144: (217-232): Underflow (resulting value less than 0) happens here
diff --git a/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol b/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol
index 44808ce4c..4e92b34eb 100644
--- a/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol
+++ b/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol
@@ -53,5 +53,4 @@ contract MyConc{
 // ----
 // Warning 2519: (773-792): This declaration shadows an existing declaration.
 // Warning 2018: (1009-1086): Function state mutability can be restricted to view
-// Warning 6084: (985-1002): Underflow (resulting value less than 0) happens here.
-// Warning 6084: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4984: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and.sol
index e969e3c3d..66f262787 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and.sol
@@ -15,4 +15,3 @@ contract c {
 	}
 }
 // ----
-// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol
index 186a2e1a8..650bce10a 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol
@@ -16,4 +16,3 @@ contract c {
 }
 // ----
 // Warning 6328: (227-236): Assertion violation happens here
-// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol
index 1dd387cc9..77e2f247f 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol
@@ -19,4 +19,3 @@ contract c {
 // ----
 // Warning 6328: (202-218): Assertion violation happens here
 // Warning 6328: (242-252): Assertion violation happens here
-// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both.sol
index ff526db60..905964ed5 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both.sol
@@ -15,4 +15,3 @@ contract c {
 	}
 }
 // ----
-// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol
index 32fbccdd7..bc9c800af 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol
@@ -16,4 +16,3 @@ contract c {
 }
 // ----
 // Warning 6328: (225-235): Assertion violation happens here
-// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or.sol
index d6007e676..1a6cb909a 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or.sol
@@ -15,4 +15,3 @@ contract c {
 	}
 }
 // ----
-// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol
index edada1444..6640e399c 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol
@@ -16,4 +16,3 @@ contract c {
 }
 // ----
 // Warning 6328: (225-235): Assertion violation happens here
-// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol
index eb54e2236..77ec37ebd 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol
@@ -25,4 +25,3 @@ contract c {
 }
 // ----
 // Warning 6328: (360-370): Assertion violation happens here
-// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both.sol
index c585abdb4..c4a823dbc 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both.sol
@@ -15,4 +15,3 @@ contract c {
 	}
 }
 // ----
-// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol
index 1a055a9d7..6615651fd 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol
@@ -16,4 +16,3 @@ contract c {
 }
 // ----
 // Warning 6328: (225-235): Assertion violation happens here
-// Warning 2661: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol
index b50177619..789b98368 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol
@@ -19,6 +19,6 @@ contract A is B {
 	}
 }
 // ----
+// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (244-249): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 6328: (232-250): Assertion violation happens here
-// Warning 2661: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (244-249): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
index c2466c0d1..6e8c4fe95 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
@@ -18,6 +18,6 @@ contract A is B {
 	}
 }
 // ----
-// Warning 2661: (207-212): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (198-203): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (230-235): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (198-203): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (207-212): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (230-235): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol
index 29c2d41b2..e5c8d5b38 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol
@@ -25,7 +25,6 @@ contract A is B2, B1 {
 	}
 }
 // ----
+// Warning 4984: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 6328: (302-320): Assertion violation happens here
-// Warning 2661: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol
index 83cb5dc64..b09b836ec 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol
@@ -25,7 +25,6 @@ contract A is B2, B1 {
 	}
 }
 // ----
+// Warning 4984: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 6328: (302-320): Assertion violation happens here
-// Warning 2661: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (200-205): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (314-319): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
index cdd479268..f6bfc6d94 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
@@ -27,11 +27,7 @@ contract A is B2, B1 {
 	}
 }
 // ----
+// Warning 4984: (160-165): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (225-230): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (241-246): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 6328: (334-350): Assertion violation happens here
-// Warning 4144: (160-165): Underflow (resulting value less than 0) happens here
-// Warning 2661: (160-165): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (225-230): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (241-246): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (225-230): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (241-246): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (160-165): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol
index 223703be4..92e53f40c 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol
@@ -25,6 +25,5 @@ contract A is B {
 	}
 }
 // ----
+// Warning 4984: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 6328: (328-342): Assertion violation happens here
-// Warning 2661: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
index 106e60440..6771f6a05 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
@@ -13,5 +13,5 @@ contract C {
 	}
 }
 // ----
+// Warning 4984: (115-120): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 6328: (162-176): Assertion violation happens here
-// Warning 2661: (115-120): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_state_var_init_2.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_state_var_init_2.sol
index 3439ec6d4..ef7cb6647 100644
--- a/test/libsolidity/smtCheckerTests/functions/internal_call_state_var_init_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/internal_call_state_var_init_2.sol
@@ -7,6 +7,3 @@ contract c {
 	bool b = (f() > 0) || (f() > 0);
 }
 // ----
-// Warning 2661: (100-105): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 4144: (100-105): Underflow (resulting value less than 0) happens here
-// Warning 2661: (100-105): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/library_constant.sol b/test/libsolidity/smtCheckerTests/functions/library_constant.sol
index ee521a181..2a72c5216 100644
--- a/test/libsolidity/smtCheckerTests/functions/library_constant.sol
+++ b/test/libsolidity/smtCheckerTests/functions/library_constant.sol
@@ -20,7 +20,6 @@ contract C {
 }
 // ----
 // Warning 6328: (136-155): Assertion violation happens here
-// Warning 2661: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (327-332): Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 8364: (300-302): Assertion checker does not yet implement type type(library l1)
-// Warning 2661: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (327-332): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_mixed_chain_with_params.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_mixed_chain_with_params.sol
index 223703be4..92e53f40c 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_mixed_chain_with_params.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_mixed_chain_with_params.sol
@@ -25,6 +25,5 @@ contract A is B {
 	}
 }
 // ----
+// Warning 4984: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 6328: (328-342): Assertion violation happens here
-// Warning 2661: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (247-252): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol
index a9323fdbc..5538b9ee8 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol
@@ -22,12 +22,10 @@ contract A is B {
 }
 
 // ----
+// Warning 4984: (157-162): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (216-221): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (261-270): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (287-292): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 6328: (275-293): Assertion violation happens here
-// Warning 4144: (157-162): Underflow (resulting value less than 0) happens here
-// Warning 2661: (157-162): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (216-221): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (157-162): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (239-244): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (261-266): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (261-270): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (287-292): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol
index c0ad1b083..f597d60e4 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol
@@ -22,10 +22,9 @@ contract A is B {
 }
 
 // ----
+// Warning 4984: (157-163): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (217-222): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (240-245): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (262-268): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (285-290): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 6328: (273-291): Assertion violation happens here
-// Warning 2661: (157-163): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (217-222): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (157-163): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (240-245): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (262-268): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning 2661: (285-290): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol
index b4d819887..c6cbafaef 100644
--- a/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol
@@ -5,7 +5,6 @@ contract C
 	function f(uint x) public pure {
 		require(x < 100);
 		do {
-			// Overflows due to resetting x.
 			x = x + 1;
 		} while (x < 10);
 		assert(x < 14);
@@ -14,5 +13,4 @@ contract C
 // ====
 // SMTSolvers: z3
 // ----
-// Warning 6328: (179-193): Assertion violation happens here
-// Warning 2661: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 6328: (143-157): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol
index 55f7975f0..2345cc4f3 100644
--- a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol
+++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol
@@ -5,15 +5,10 @@ contract C
 	function f(uint x) public pure {
 		require(x < 100);
 		do {
-			// Overflows due to resetting x.
 			x = x + 1;
 		} while (x < 1000);
-		// The assertion is true but we can't infer so
-		// because x is touched in the loop.
 		assert(x > 0);
 	}
 }
 // ====
 // SMTSolvers: z3
-// ----
-// Warning 2661: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
index de7fdf973..0579325df 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
@@ -14,5 +14,6 @@ contract C
 // ====
 // SMTSolvers: z3
 // ----
+// Warning 1218: (176-181): Error trying to invoke SMT solver.
 // Warning 6328: (189-203): Assertion violation happens here
 // Warning 2661: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
index ba6a6a8d2..d10ba5b42 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
@@ -19,6 +19,7 @@ contract LoopFor2 {
 // ====
 // SMTSolvers: z3
 // ----
+// Warning 1218: (244-249): Error trying to invoke SMT solver.
 // Warning 6328: (281-301): Assertion violation happens here
 // Warning 6328: (305-324): Assertion violation happens here
 // Warning 6328: (328-347): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
index b977ed326..b61baaac9 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
@@ -23,5 +23,6 @@ contract LoopFor2 {
 // ====
 // SMTSolvers: z3
 // ----
+// Warning 1218: (237-242): Error trying to invoke SMT solver.
 // Warning 6328: (362-382): Assertion violation happens here
 // Warning 6328: (409-428): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol
index 5a2dbbcba..f543be8db 100644
--- a/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol
+++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol
@@ -21,5 +21,5 @@ contract C
 	}
 }
 // ----
+// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 6328: (136-149): Assertion violation happens here
-// Warning 2661: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol
index 2b5f131d7..52dd6ee5f 100644
--- a/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol
@@ -15,4 +15,3 @@ contract C
 	}
 }
 // ----
-// Warning 2661: (145-150): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/division_3.sol b/test/libsolidity/smtCheckerTests/operators/division_3.sol
index 03af864ef..dd82c5bb7 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_3.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_3.sol
@@ -6,4 +6,5 @@ contract C {
 	}
 }
 // ----
+// Warning 1218: (127-132): Error trying to invoke SMT solver.
 // Warning 2661: (127-132): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/division_4.sol b/test/libsolidity/smtCheckerTests/operators/division_4.sol
index ce67e3375..52e3db08b 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_4.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_4.sol
@@ -6,3 +6,5 @@ contract C {
 		return x / y;
 	}
 }
+// ----
+// Warning 1218: (147-152): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/division_5.sol b/test/libsolidity/smtCheckerTests/operators/division_5.sol
index ed6966223..6458dd8e3 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_5.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_5.sol
@@ -9,3 +9,5 @@ contract C {
 		return c;
 	}
 }
+// ----
+// Warning 1218: (151-156): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/division_6.sol b/test/libsolidity/smtCheckerTests/operators/division_6.sol
index 24e7a6325..7da33cbaa 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_6.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_6.sol
@@ -11,3 +11,5 @@ contract C {
 		return c;
 	}
 }
+// ----
+// Warning 1218: (265-270): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol
index 6473b98f3..a5a8daf59 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol
@@ -7,4 +7,5 @@ contract C {
 	}
 }
 // ----
+// Warning 1218: (112-117): Error trying to invoke SMT solver.
 // Warning 1218: (105-123): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol
index c9a932a42..8c903a242 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol
@@ -7,4 +7,5 @@ contract C {
 	}
 }
 // ----
+// Warning 1218: (113-118): Error trying to invoke SMT solver.
 // Warning 1218: (106-125): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol
index 95743c934..0514b894f 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol
@@ -7,4 +7,5 @@ contract C {
 	}
 }
 // ----
+// Warning 1218: (113-118): Error trying to invoke SMT solver.
 // Warning 1218: (106-125): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol
index 2570b375f..348ad0dd5 100644
--- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol
+++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol
@@ -7,4 +7,5 @@ contract C {
 	}
 }
 // ----
+// Warning 1218: (114-119): Error trying to invoke SMT solver.
 // Warning 1218: (107-125): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol b/test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol
index c92a1ac5d..e8e388c15 100644
--- a/test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol
+++ b/test/libsolidity/smtCheckerTests/operators/fixed_point_add.sol
@@ -6,7 +6,6 @@ contract test {
 }
 // ----
 // Warning 2072: (80-88): Unused local variable.
+// Warning 4984: (91-112): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 5084: (91-100): Type conversion is not yet fully supported and might yield false positives.
 // Warning 5084: (103-112): Type conversion is not yet fully supported and might yield false positives.
-// Warning 4144: (91-112): Underflow (resulting value less than 0) happens here
-// Warning 2661: (91-112): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/fixed_point_compound_add.sol b/test/libsolidity/smtCheckerTests/operators/fixed_point_compound_add.sol
index b815b0c94..8a8af3a5c 100644
--- a/test/libsolidity/smtCheckerTests/operators/fixed_point_compound_add.sol
+++ b/test/libsolidity/smtCheckerTests/operators/fixed_point_compound_add.sol
@@ -4,5 +4,3 @@ contract C {
   function f() internal { b[0] += 1; }
 }
 // ----
-// Warning 4144: (84-93): Underflow (resulting value less than 0) happens here
-// Warning 2661: (84-93): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/mod_even.sol b/test/libsolidity/smtCheckerTests/operators/mod_even.sol
index ab88a7ede..9e8a9cd96 100644
--- a/test/libsolidity/smtCheckerTests/operators/mod_even.sol
+++ b/test/libsolidity/smtCheckerTests/operators/mod_even.sol
@@ -9,4 +9,5 @@ contract C
 	}
 }
 // ----
+// Warning 1218: (113-118): Error trying to invoke SMT solver.
 // Warning 1218: (122-142): Error trying to invoke SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/special/many.sol b/test/libsolidity/smtCheckerTests/special/many.sol
index 1fbd2f905..2e9b3c79a 100644
--- a/test/libsolidity/smtCheckerTests/special/many.sol
+++ b/test/libsolidity/smtCheckerTests/special/many.sol
@@ -15,6 +15,7 @@ contract C
 	}
 }
 // ----
+// Warning 4984: (311-316): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 6328: (79-115): Assertion violation happens here
 // Warning 6328: (119-161): Assertion violation happens here
 // Warning 6328: (165-204): Assertion violation happens here
@@ -23,4 +24,3 @@ contract C
 // Warning 6328: (304-332): Assertion violation happens here
 // Warning 6328: (336-364): Assertion violation happens here
 // Warning 6328: (368-391): Assertion violation happens here
-// Warning 2661: (311-316): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/types/address_balance.sol b/test/libsolidity/smtCheckerTests/types/address_balance.sol
index 8edae0c8c..c4d10fead 100644
--- a/test/libsolidity/smtCheckerTests/types/address_balance.sol
+++ b/test/libsolidity/smtCheckerTests/types/address_balance.sol
@@ -9,5 +9,5 @@ contract C
 }
 // ----
 // Warning 2072: (96-102): Unused local variable.
+// Warning 4984: (105-127): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning 6328: (131-160): Assertion violation happens here
-// Warning 2661: (105-127): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_2.sol b/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_2.sol
index 0a89c9975..9cea35cbb 100644
--- a/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_2.sol
+++ b/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_2.sol
@@ -15,4 +15,4 @@ contract C
 	}
 }
 // ----
-// Warning 2661: (152-157): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4984: (152-157): Overflow (resulting value larger than 2**256 - 1) happens here