update tests round1

Leo Alt · Leo Alt · commit a0c8df3d1bed · 2021-05-31T20:09:21.000+02:00
diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol
@@ -23,3 +23,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-380): Contract invariants for :C:\n!(arr.length <= 2)\n!(arr.length <= 3)\n!(arr[2].length <= 3)\n
diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol
@@ -27,3 +27,4 @@ contract C {
 // Warning 6328: (291-317): CHC: Assertion violation happens here.
 // Warning 6328: (321-347): CHC: Assertion violation happens here.
 // Warning 6328: (351-374): CHC: Assertion violation happens here.
+// Warning 0: (0-380): Contract invariants for :C:\n!(arr.length <= 2)\n!(arr.length <= 3)\n!(arr[2].length <= 3)\n
diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol
@@ -28,3 +28,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-440): Contract invariants for :C:\n!(arr.length <= 7)\n!(arr.length <= 8)\n((arr[5].length <= 0) && (arr[8].length <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol
@@ -30,3 +30,4 @@ contract C {
 // Warning 6328: (349-375): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
 // Warning 6328: (379-402): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
 // Warning 6328: (406-432): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
+// Warning 0: (0-438): Contract invariants for :C:\n!(arr.length <= 7)\n!(arr.length <= 8)\n
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol
@@ -9,3 +9,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-135): Contract invariants for :C:\n(!((x[x.length] := 23)[0] <= 41) && !((x[x.length] := 23)[0] >= 43))\n
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol
@@ -9,3 +9,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-121): Contract invariants for :C:\n(!((x[x.length] := 23)[0] >= 43) && !((x[x.length] := 23)[0] <= 41))\n
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol
@@ -17,3 +17,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (57-239): Contract invariants for :C:\n((!((address(this) + ((- 1) * t)) = 0) || (<errorCode> <= 0)) && (!((address(this) + ((- 1) * t)) >= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((address(this) + ((- 1) * t)) <= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n((!(<errorCode> >= 2) || !((address(this) + ((- 1) * t)) = 0)) && (!((address(this) + ((- 1) * t)) >= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (((address(this) + ((- 1) * t')) <= 0) || !((address(this) + ((- 1) * t)) <= 0)))\n(((t + ((- 1) * address(this))) >= 0) && ((t + ((- 1) * address(this))) <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol
@@ -23,3 +23,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (327-341): CHC: Assertion violation happens here.\nCounterexample:\nx = 7\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n    C.f() -- internal call
+// Warning 0: (0-350): Contract invariants for :C:\n((x = 0) || (x = 7))\n
diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol
@@ -23,3 +23,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (333-347): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n    C.f() -- internal call
+// Warning 0: (0-356): Contract invariants for :C:\n((x = 0) || (x = 3))\n
diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol
@@ -23,3 +23,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (326-340): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n    C.f() -- internal call
+// Warning 0: (0-349): Contract invariants for :C:\n((x = 0) || (x = 3))\n
diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol
@@ -24,3 +24,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (333-347): CHC: Assertion violation happens here.
+// Warning 0: (0-356): Contract invariants for :C:\n((x = 0) || (x = 7))\n
diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers.sol
@@ -24,3 +24,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (70-84): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()
+// Warning 0: (0-251): Contract invariants for :C:\n(x = 0)\n
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
@@ -18,3 +18,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-203): Contract invariants for :C:\n((a <= 0) && (b <= 0) && (c <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external.sol b/test/libsolidity/smtCheckerTests/external_calls/external.sol
@@ -18,3 +18,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (167-181): CHC: Assertion violation happens here.
+// Warning 0: (57-187): Contract invariants for :C:\n!(<errorCode> = 1)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash.sol
@@ -28,3 +28,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (390-412): CHC: Assertion violation happens here.
+// Warning 0: (95-418): Contract invariants for :C:\n!(<errorCode> = 1)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol
@@ -30,3 +30,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (398-420): CHC: Assertion violation happens here.
+// Warning 0: (103-426): Contract invariants for :C:\n!(<errorCode> = 1)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol
@@ -36,3 +36,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (495-532): CHC: Assertion violation happens here.
+// Warning 0: (155-538): Contract invariants for :C:\n(((owner + ((- 1) * owner')) >= 0) && !(<errorCode> = 1) && ((owner + ((- 1) * owner')) <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol
@@ -31,3 +31,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (266-280): CHC: Assertion violation happens here.
+// Warning 0: (97-375): Contract invariants for :C:\n!(<errorCode> >= 2)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol
@@ -41,3 +41,4 @@ contract C {
 // ----
 // Warning 2018: (33-88): Function state mutability can be restricted to view
 // Warning 6328: (367-381): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, z = 3, s = 0, insidef = true\nprevOwner = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, z = 0, s = 0, insidef = false\nC.f()\n    s.f() -- untrusted external call, synthesized as:\n        C.zz() -- reentrant call
+// Warning 0: (92-495): Contract invariants for :C:\n(((owner' + ((- 1) * owner)) >= 0) && ((owner' + ((- 1) * owner)) <= 0) && !(<errorCode> >= 2))\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol
@@ -41,3 +41,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (97-581): Contract invariants for :C:\n!(<errorCode> >= 2)\n(!(z' <= 0) || (<errorCode> <= 0))\n((z <= 0) && !insidef && (y <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol
@@ -29,3 +29,4 @@ contract C is A {
 // ----
 // Warning 6328: (154-168): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()
 // Warning 6328: (352-366): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nd = 0\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.call(0)\n    d.d() -- untrusted external call, synthesized as:\n        C.f() -- reentrant call
+// Warning 0: (190-387): Contract invariants for :C:\n(!(x <= 0) && !(x >= 2))\n(!(x >= 2) && !(x <= 0))\n((!(x <= 1) || !(x' >= 2)) && (!(x' <= 0) || (x <= 0)))\n((!(x' <= 0) || (x <= 0)) && (!(<errorCode> = 5) || !(x = 1)) && (!(x <= 1) || !(x' >= 2)))\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
@@ -30,4 +30,5 @@ contract C {
 // Warning 6328: (302-333): CHC: Assertion violation might happen here.
 // Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (302-333): CHC: Assertion violation might happen here.
+// Warning 0: (55-395): Contract invariants for :C:\n((!((kec + ((- 1) * keccak256(data))) >= 0) || ((kec' + ((- 1) * keccak256(data'))) >= 0)) && (!((kec + ((- 1) * keccak256(data))) <= 0) || ((kec' + ((- 1) * keccak256(data'))) <= 0)))\n((!(<errorCode> = 1) || !((kec + ((- 1) * keccak256(data))) = 0)) && (!((kec + ((- 1) * keccak256(data))) <= 0) || ((kec' + ((- 1) * keccak256(data'))) <= 0)) && (!((kec + ((- 1) * keccak256(data))) >= 0) || ((kec' + ((- 1) * keccak256(data'))) >= 0)))\n(((kec + ((- 1) * keccak256(data))) >= 0) && ((kec + ((- 1) * keccak256(data))) <= 0))\n
 // Warning 4661: (302-333): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol
@@ -17,3 +17,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (57-187): Contract invariants for :C:\n!(<errorCode> = 1)\n!(x >= 11)\n((!(x <= 10) || !(<errorCode> >= 2)) && (!(x <= 10) || !(x' >= 11)))\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/mutex.sol b/test/libsolidity/smtCheckerTests/external_calls/mutex.sol
@@ -27,3 +27,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (57-300): Contract invariants for :C:\n((!lock || ((x' + ((- 1) * x)) = 0)) && (<errorCode> <= 0) && (lock' || !lock))\n
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol
@@ -17,3 +17,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (61-244): Contract invariants for :C:\n!(<errorCode> = 1)\n((!(x <= 0) || !(<errorCode> >= 2)) && (!(x <= 0) || (x' <= 0)))\n(x <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
@@ -24,3 +24,4 @@ contract C
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (234-253): CHC: Assertion violation happens here.
+// Warning 0: (61-337): Contract invariants for :C:\n!(<errorCode> = 1)\n((!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)) && !(<errorCode> = 2) && (!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)))\n
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol
@@ -18,3 +18,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (61-352): Contract invariants for :C:\n!(<errorCode> >= 2)\n(<errorCode> <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_identifier_nested_tuple_1.sol
@@ -14,3 +14,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-184): Contract invariants for :C:\n((x = 0) || (x = 1))\n
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol
@@ -23,3 +23,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-213): Contract invariants for :C:\n(a <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1.sol b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1.sol
@@ -21,3 +21,4 @@ contract C{
 // SMTEngine: all
 // ----
 // Warning 5667: (37-43): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning 0: (0-210): Contract invariants for :C:\n!(x <= 0)\n!(x >= 2)\n(!(x <= 0) && !(x >= 2))\n
diff --git a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol
@@ -24,3 +24,4 @@ contract C{
 // Warning 6328: (105-119): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()
 // Warning 6328: (151-165): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n    C.g() -- internal call\n    C.g() -- internal call
 // Warning 6328: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)
+// Warning 0: (0-210): Contract invariants for :C:\n!(x <= 0)\n!(x >= 2)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol b/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol
@@ -31,3 +31,5 @@ contract D is C {
 // ----
 // Warning 6328: (205-219): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.proxy()\n    C.f() -- internal call\n        A.f() -- internal call
 // Warning 6328: (328-342): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.proxy()\n    D.f() -- internal call\n        C.f() -- internal call\n            A.f() -- internal call
+// Warning 0: (0-110): Contract invariants for :A:\n((x = 0) || (x = 2))\n
+// Warning 0: (242-363): Contract invariants for :D:\n((x = 0) || (x = 2))\n
diff --git a/test/libsolidity/smtCheckerTests/functions/this_state.sol b/test/libsolidity/smtCheckerTests/functions/this_state.sol
@@ -13,3 +13,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-157): Contract invariants for :C:\n((x = 0) || (x = 2))\n
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol
@@ -30,3 +30,4 @@ contract C is B {
 // ----
 // Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()\n    A.v() -- internal call
 // Warning 6328: (62-76): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nB.f()\n    A.f() -- internal call\n        C.v() -- internal call
+// Warning 0: (0-247): Contract invariants for :A:\n(x = 0)\n
diff --git a/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol b/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol
@@ -33,3 +33,7 @@ contract E is C,D {
 // SMTEngine: all
 // ----
 // Warning 6328: (379-394): CHC: Assertion violation happens here.\nCounterexample:\nx = 111\n\nTransaction trace:\nE.constructor()\nState: x = 0\nE.f()\n    C.f() -- internal call\n        B.f() -- internal call\n            A.f() -- internal call
+// Warning 0: (74-161): Contract invariants for :B:\n((x = 0) || (x = 101))\n
+// Warning 0: (163-249): Contract invariants for :C:\n((x = 0) || (x = 111))\n
+// Warning 0: (251-270): Contract invariants for :D:\n((x = 0) || (x = 101))\n
+// Warning 0: (272-415): Contract invariants for :E:\n((x = 0) || (x = 111))\n
diff --git a/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol b/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol
@@ -32,3 +32,4 @@ contract C {
 // SMTEngine: all
 // SMTSolvers: z3
 // ----
+// Warning 0: (0-425): Contract invariants for :C:\n!(x >= 3)\n
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol
@@ -35,3 +35,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (540-554): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, owner = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, owner = 0\nC.g(1)
+// Warning 0: (0-560): Contract invariants for :C:\n(owner <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol
@@ -15,3 +15,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-123): Contract invariants for :C:\n(x <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol
@@ -39,3 +39,6 @@ contract D is B,C {
 // Warning 6328: (160-174): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nB.constructor()\nState: x = 0\nA.f()
 // Warning 6328: (193-207): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.f()
 // Warning 6328: (226-240): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.f()
+// Warning 0: (298-369): Contract invariants for :B:\n((x = 0) || (x = 1))\n
+// Warning 0: (371-442): Contract invariants for :C:\n((x = 0) || (x = 2))\n
+// Warning 0: (444-522): Contract invariants for :D:\n((x = 0) || (x = 3))\n
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations_2.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations_2.sol
@@ -17,3 +17,4 @@ contract C
 // SMTEngine: all
 // ----
 // Warning 6328: (76-90): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()
+// Warning 0: (0-140): Contract invariants for :C:\n(x = 3)\n
diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol
@@ -29,3 +29,4 @@ contract A {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (392-408): CHC: Assertion violation happens here.
+// Warning 0: (0-476): Contract invariants for :A:\n(((x = 0) && (y = 0)) || ((x = (- 2)) && (y = (- 2))))\n
diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol
@@ -13,3 +13,4 @@ contract A {
 // SMTEngine: all
 // ----
 // Warning 6328: (124-146): CHC: Assertion violation happens here.\nCounterexample:\na = []\n\nTransaction trace:\nA.constructor()\nState: a = []\nA.f()
+// Warning 0: (0-179): Contract invariants for :A:\n(a.length <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol
@@ -30,3 +30,4 @@ contract A {
 // Warning 6328: (311-328): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\nb = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f()
 // Warning 6368: (422-426): CHC: Out of bounds access happens here.\nCounterexample:\na = [0, 0]\nu = []\nb = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f()
 // Warning 6328: (415-432): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\nb = [0, 0]\n\nTransaction trace:\nA.constructor()\nState: a = [1]\nA.f()
+// Warning 0: (0-503): Contract invariants for :A:\n!(a.length <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol
@@ -30,3 +30,4 @@ contract A {
 // ----
 // 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()
+// Warning 0: (AASource:25-457): Contract invariants for AASource:A:\n(((x = (- 2)) && (y = (- 2))) || ((x = 0) && (y = 0)))\n(((x = 0) && (y = 0)) || ((x = (- 2)) && (y = (- 2))))\n
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
@@ -19,3 +19,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-294): Contract invariants for :C:\n!(s.x.length <= 2)\n
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol
@@ -24,3 +24,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 2072: (255-261): Unused local variable.
+// Warning 0: (59-367): Contract invariants for :C:\n((!(x' <= 0) || !(x >= 2)) && (<errorCode> <= 0) && (!(x <= 2) || !(x' >= 3)))\n((!(x' <= 0) || ((x' + ((- 1) * x)) = 0)) && (<errorCode> <= 0) && (!(x <= 2) || !(x' >= 3)))\n
diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol
@@ -17,3 +17,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-226): Contract invariants for :C:\n(true && !(a.length <= 2))\n(true && !(a[2].length <= 3))\n
diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_index.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_index.sol
@@ -20,4 +20,5 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-218): Contract invariants for :C:\n!(a.length <= 2)\n
 // Warning 6838: (154-155): BMC: Condition is always false.
diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol
@@ -27,4 +27,5 @@ contract C
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (315-335): CHC: Assertion violation might happen here.
+// Warning 0: (0-341): Contract invariants for :C:\n!(a.length <= 1)\n
 // Warning 4661: (315-335): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/delete_function.sol b/test/libsolidity/smtCheckerTests/operators/delete_function.sol
@@ -28,4 +28,5 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-344): Contract invariants for :C:\n!(a.length <= 2)\n
 // Warning 6838: (262-263): BMC: Condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_array_push_2.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_array_push_2.sol
@@ -18,3 +18,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-234): Contract invariants for :C:\n!(data.length <= 1)\n!(data[1].d.length <= 3)\n
diff --git a/test/libsolidity/smtCheckerTests/out_of_bounds/array_2.sol b/test/libsolidity/smtCheckerTests/out_of_bounds/array_2.sol
@@ -21,3 +21,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-341): Contract invariants for :C:\n((l + ((- 1) * a.length)) <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_constant_bound.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_constant_bound.sol
@@ -13,5 +13,6 @@ contract DepositContract {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (256-277): CHC: Error trying to invoke SMT solver.
 // Warning 4984: (256-277): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 2661: (256-277): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/special/msg_value_3.sol b/test/libsolidity/smtCheckerTests/special/msg_value_3.sol
@@ -13,3 +13,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (0-183): Contract invariants for :C:\nlock\n
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_4.sol b/test/libsolidity/smtCheckerTests/try_catch/try_4.sol
@@ -27,3 +27,4 @@ contract C {
 // ----
 // Warning 6328: (178-192): CHC: Assertion violation happens here.
 // Warning 6328: (318-332): CHC: Assertion violation happens here.
+// Warning 0: (57-357): Contract invariants for :C:\n!(<errorCode> = 2)\n
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_5.sol b/test/libsolidity/smtCheckerTests/try_catch/try_5.sol
@@ -26,3 +26,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (315-329): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()
+// Warning 0: (57-354): Contract invariants for :C:\n!(<errorCode> = 2)\n((!(x <= 0) || !(x' >= 100)) && !(<errorCode> = 1))\n
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol
@@ -25,3 +25,4 @@ contract C {
 // Warning 6328: (185-199): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\nx = 1\nc = false\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()\n    d.d() -- untrusted external call
 // Warning 6328: (273-283): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\nx = 1\nc = true\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()\n    d.d() -- untrusted external call
 // Warning 6328: (393-407): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()
+// Warning 0: (82-432): Contract invariants for :C:\n!(<errorCode> = 3)\n
diff --git a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol
@@ -20,3 +20,4 @@ contract C
 // ----
 // Warning 2072: (191-207): Unused local variable.
 // Warning 6328: (233-248): CHC: Assertion violation happens here.
+// Warning 0: (0-323): Contract invariants for :C:\n(x = 0)\n
diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol
@@ -28,3 +28,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 0: (35-710): Contract invariants for :C:\n!(array.length <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/types/array_branch_3d.sol b/test/libsolidity/smtCheckerTests/types/array_branch_3d.sol
@@ -23,3 +23,4 @@ contract C
 // Warning 6368: (177-184): CHC: Out of bounds access might happen here.
 // Warning 6368: (177-187): CHC: Out of bounds access might happen here.
 // Warning 6328: (170-192): CHC: Assertion violation happens here.\nCounterexample:\nc = [[[0]]]\nb = false\n\nTransaction trace:\nC.constructor()\nState: c = [[[0]]]\nC.f(false)
+// Warning 0: (0-198): Contract invariants for :C:\n!(c.length <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/types/array_branches_3d.sol b/test/libsolidity/smtCheckerTests/types/array_branches_3d.sol
@@ -22,3 +22,4 @@ contract C
 // Warning 6368: (152-162): CHC: Out of bounds access might happen here.
 // Warning 6368: (177-184): CHC: Out of bounds access might happen here.
 // Warning 6368: (177-187): CHC: Out of bounds access might happen here.
+// Warning 0: (0-198): Contract invariants for :C:\n!(c.length <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol
@@ -43,3 +43,4 @@ contract C
 // Warning 6368: (850-869): CHC: Out of bounds access happens here.
 // Warning 6328: (936-956): CHC: Assertion violation happens here.
 // Warning 6368: (1029-1043): CHC: Out of bounds access might happen here.
+// Warning 0: (0-1050): Contract invariants for :C:\n!(severalMaps8.length <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol
diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
diff --git a/test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol b/test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol
