diff --git a/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol b/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol
index 55b2160c4..5ed512278 100644
--- a/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol
@@ -13,6 +13,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
-// Warning 6328: (139-161): CHC: Assertion violation happens here.
+// Warning 6328: (139-161): CHC: Assertion violation happens here.\nCounterexample:\ndata = [0x62]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()
 // Warning 6328: (263-290): CHC: Assertion violation happens here.\nCounterexample:\ndata = [0x01]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()
diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol
index 4796e3a81..294038399 100644
--- a/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol
@@ -16,4 +16,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
+// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 0)\n!(arr2.length <= 0)\n(((arr.length + ((- 1) * arr2.length)) <= 0) && ((arr2.length + ((- 1) * arr.length)) <= 0))\n(((arr2[0].length + ((- 1) * arr[0].length)) >= 0) && ((arr2[0].length + ((- 1) * arr[0].length)) <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol
index 5ad65991a..468f34257 100644
--- a/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol
@@ -17,3 +17,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 1)\n
diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol
index c6e695f24..48e0f73bf 100644
--- a/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol
@@ -7,3 +7,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(true && (map[1].length <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol
index 3ab218741..833caa24f 100644
--- a/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol
@@ -11,3 +11,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(((s1.arr.length + ((- 1) * s2.arr.length)) >= 0) && ((s1.arr.length + ((- 1) * s2.arr.length)) <= 0))\n
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 cd9b6690d..71571d944 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
@@ -21,3 +21,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// 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/length_function_call.sol b/test/libsolidity/smtCheckerTests/array_members/length_function_call.sol
index a51c7aa7d..c96d53047 100644
--- a/test/libsolidity/smtCheckerTests/array_members/length_function_call.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/length_function_call.sol
@@ -9,3 +9,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(arr.length <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol
index 5756c7aff..4f1cf701b 100644
--- a/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol
@@ -15,3 +15,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 2)\n
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
index 525c704e1..66dad8412 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) 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
index 086224a11..0023906fe 100644
--- 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.
+// Info 1180: Contract invariant(s) 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
index 78a020e05..caafcbd39 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) 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
index f4d5c889c..062b668c3 100644
--- 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
@@ -25,8 +25,10 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (319-345): 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: (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()
+// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 3)\n!(arr.length <= 5)\n!(arr.length <= 7)\n!(arr.length <= 8)\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..30f194eb7 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
@@ -18,4 +18,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()
+// Warning 6328: (199-229): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol
index 6b23ac1d4..ad3ba7823 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol
@@ -12,5 +12,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
-// Warning 6328: (204-230): CHC: Assertion violation happens here.
+// Warning 6328: (204-230): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol
index 0a440e7a4..930736ce8 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol
@@ -8,4 +8,5 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreInv: yes
 // ----
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
index 6992ca1e4..9cc3f2e37 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(!((x[x.length] := 23)[0] >= 43) && !((x[x.length] := 23)[0] <= 41))\n
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol
index 1b241745a..60b11c91a 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol
@@ -11,4 +11,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(x.length >= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol
index c29c34f62..dcda253ce 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol
@@ -10,6 +10,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (90-116): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
 // Warning 6328: (170-186): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
index 43eebddcf..87b9d92bf 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
@@ -12,6 +12,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6368: (188-192): CHC: Out of bounds access happens here.\nCounterexample:\na = []\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
 // Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol
index 100f11066..f88eab0bf 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol
@@ -11,3 +11,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (153-188): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ msg.value: 101 }\nC.f()
+// Info 1180: Contract invariant(s) for :C:\n!((:var 0).balances[address(this)] <= 100)\n
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol
index ea5947d01..fc4719cef 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol
@@ -16,3 +16,4 @@ contract C {
 // ----
 // Warning 6328: (132-188): CHC: Assertion violation happens here.
 // Warning 6328: (269-324): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n((prevBalance + ((- 1) * (:var 1).balances[address(this)])) <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol
index c561179ec..c4714e2e3 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol
@@ -17,3 +17,4 @@ contract C {
 // ----
 // Warning 4984: (266-272): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = true\n\nTransaction trace:\nC.constructor(){ msg.value: 28100 }\nState: x = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = false\nC.f(){ msg.value: 8 }
 // Warning 6328: (235-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, once = true\n\nTransaction trace:\nC.constructor(){ msg.value: 0 }\nState: x = 0, once = false\nC.f(){ msg.value: 8 }
+// Info 1180: Contract invariant(s) for :C:\nonce\n
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
index 183e60d95..e8f750d07 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
@@ -15,7 +15,8 @@ contract C {
 // 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.
 // Warning 4984: (212-218): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 6328: (180-219): CHC: Assertion violation happens here.\nCounterexample:\nc = 1\n\nTransaction trace:\nC.constructor()\nState: c = 0\nC.f(){ msg.value: 11 }\nState: c = 1\nC.inv()
+// Warning 6328: (180-219): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n(((11 * c) + ((- 1) * (:var 1).balances[address(this)])) <= 0)\n
 // Warning 2661: (82-85): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (154-160): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (212-218): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol
index e703c65c3..1885a60c8 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol
@@ -12,3 +12,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (122-158): CHC: Assertion violation happens here.\nCounterexample:\nsum = 0\n\nTransaction trace:\nC.constructor()\nState: sum = 0\nC.inv()
+// Info 1180: Contract invariant(s) for :C:\n((sum + ((- 1) * (:var 1).balances[address(this)])) <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol
index 3bc569997..263a90b08 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol
@@ -20,7 +20,9 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (173-208): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ msg.value: 10 }
 // Warning 6328: (321-356): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ msg.value: 10 }\n    C.g() -- internal call
 // Warning 6328: (469-504): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ msg.value: 10 }\n    C.g() -- internal call\n        C.h() -- internal call
+// Info 1180: Contract invariant(s) for :C:\n((:var 1).balances[address(this)] >= 0)\nonce\n
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 6144056a8..e46dfda34 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol
@@ -15,4 +15,5 @@ contract C {
 // ----
 // Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (131-165): CHC: Assertion violation might happen here.
+// Info 1180: Reentrancy property(ies) for :C:\n(!(<errorCode> >= 2) && (((:var 0).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) >= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance >= x)\n
 // Warning 4661: (131-165): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol
index e0da57fb2..28c4734bd 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol
@@ -12,3 +12,4 @@ contract C {
 // ----
 // Warning 9302: (82-93): Return value of low-level calls not used.
 // Warning 6328: (97-131): CHC: Assertion violation happens here.
+// Info 1180: Reentrancy property(ies) for :C:\n((((:var 1).balances[address(this)] + ((- 1) * (:var 0).balances[address(this)])) <= 0) && !(<errorCode> >= 2))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance >= x)\n
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol
index 59c123429..559f67e19 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol
@@ -22,3 +22,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (277-310): CHC: Assertion violation happens here.
+// Info 1180: Reentrancy property(ies) for :C:\n((!lock || (((:var 3).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) <= 0)) && !(<errorCode> = 1) && (lock' || !lock) && (!lock || (((:var 3).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) >= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance < x)\n
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol
index 72755cc35..1e4ec7a32 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol
@@ -19,4 +19,5 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (280-314): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n((!(c <= 1) || !((:var 1).balances[address(this)] <= 91)) && !((:var 1).balances[address(this)] <= 82) && (!(c <= 0) || !((:var 1).balances[address(this)] <= 100)))\n
 // Warning 1236: (175-190): BMC: Insufficient funds happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol
index 9b40afa2e..260d3c942 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol
@@ -13,3 +13,5 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// ----
+// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol
index 6c3d12026..50081bc5a 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol
@@ -20,4 +20,5 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (258-274): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n
 // Warning 1236: (33-46): BMC: Insufficient funds happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol
index 4f7497625..9df3aa27a 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol
@@ -16,3 +16,5 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// ----
+// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol
index 8fca1916f..f32652da9 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol
@@ -23,4 +23,5 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (315-331): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n
 // Warning 1236: (87-100): BMC: Insufficient funds happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol
index 7e233950c..0b66b2791 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol
@@ -9,4 +9,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(((address(this) + ((- 1) * t)) <= 0) && ((address(this) + ((- 1) * t)) >= 0))\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
index f3abd33c9..0b5136dca 100644
--- 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
@@ -16,4 +16,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(((address(this) + ((- 1) * t)) <= 0) && ((address(this) + ((- 1) * t)) >= 0))\nReentrancy property(ies) for :C:\n((!(<errorCode> >= 2) || !((t + ((- 1) * address(this))) = 0)) && (!((t + ((- 1) * address(this))) <= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((t + ((- 1) * address(this))) >= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n(((<errorCode> <= 0) || !((t + ((- 1) * address(this))) = 0)) && (!((t + ((- 1) * address(this))) <= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((t + ((- 1) * address(this))) >= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this) == t)\n<errorCode> = 2 -> Assertion failed at assert(a == t)\n
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol
index 3c7b1214e..0ffe43469 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol
@@ -14,3 +14,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\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
index 097637168..21f1f5c7f 100644
--- 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
+// Info 1180: Contract invariant(s) 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
index 458c78081..bf1da4275 100644
--- 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
+// Info 1180: Contract invariant(s) 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
index b8323501c..ace158bb9 100644
--- 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
+// Info 1180: Contract invariant(s) 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
index 81f8b3d7c..44910fa62 100644
--- 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.
+// Info 1180: Contract invariant(s) 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
index aa8199cd0..32d647762 100644
--- 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()
+// Info 1180: Contract invariant(s) for :C:\n(x = 0)\n
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..9765fc1f9 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
@@ -44,5 +44,5 @@ contract C {
 // SMTEngine: all
 // ----
 // 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
+// Warning 6328: (502-519): CHC: Assertion violation happens here.
 // Warning 6328: (615-629): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(10)\nState: x = 10\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 9ca87a4b0..09ee2b2b2 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
@@ -18,3 +18,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n((c <= 0) && (a <= 0) && (b <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output.sol
index aae296695..228f9d580 100644
--- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output.sol
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output.sol
@@ -37,3 +37,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(((erc + ((- 1) * ecrecover(tuple_constructor(h, v, r, s)))) <= 0) && ((erc + ((- 1) * ecrecover(tuple_constructor(h, v, r, s)))) >= 0))\n(((kec + ((- 1) * keccak256(data))) >= 0) && ((kec + ((- 1) * keccak256(data))) <= 0))\n(((rip + ((- 1) * ripemd160(data))) <= 0) && ((rip + ((- 1) * ripemd160(data))) >= 0))\n(((sha + ((- 1) * sha256(data))) <= 0) && ((sha + ((- 1) * sha256(data))) >= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol b/test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol
index 4352a7e95..a31093924 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol
@@ -23,3 +23,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 9302: (218-234): Return value of low-level calls not used.
+// Info 1180: Reentrancy property(ies) for :C:\n((!lock || ((x' + ((- 1) * x)) = 0)) && (<errorCode> <= 0) && (lock' || !lock))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(y == x)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol b/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol
index 69c2e2953..f0f844fff 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol
@@ -10,7 +10,9 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 2519: (106-112): This declaration shadows an existing declaration.
 // Warning 2072: (106-112): Unused local variable.
 // Warning 2072: (114-131): Unused local variable.
+// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && ((<errorCode> <= 0) || !(x <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_safe.sol b/test/libsolidity/smtCheckerTests/external_calls/call_safe.sol
index 33791dd0d..09d3a2592 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/call_safe.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/call_safe.sol
@@ -10,3 +10,4 @@ contract C {
 // ----
 // Warning 2072: (57-63): Unused local variable.
 // Warning 2072: (65-82): Unused local variable.
+// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && ((<errorCode> <= 0) || !(x <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external.sol b/test/libsolidity/smtCheckerTests/external_calls/external.sol
index 8dd0f404a..659329e0b 100644
--- 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.
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Overflow at ++x\n<errorCode> = 3 -> Assertion failed at assert(x < 10)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol
index cfd56271b..3fbdd8511 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol
@@ -14,3 +14,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nz = 2\n_x = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: z = 2\nC.g(0)
+// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash.sol
index 3464874c8..8f5b162a0 100644
--- 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.
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(prevOwner == owner)\n<errorCode> = 3 -> Assertion failed at assert(sig_1 == sig_2)\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
index e1273a299..2e837478d 100644
--- 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.
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(prevOwner == owner)\n<errorCode> = 3 -> Assertion failed at assert(sig_1 == sig_2)\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
index ecf7ff5ad..317400e1d 100644
--- 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.
+// Info 1180: Reentrancy property(ies) for :C:\n(((owner + ((- 1) * owner')) >= 0) && !(<errorCode> = 1) && ((owner + ((- 1) * owner')) <= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(prevOwner == owner)\n<errorCode> = 3 -> Assertion failed at assert(owner == address(0) || y != z)\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
index a90e87cb3..be9f698e1 100644
--- 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
@@ -38,6 +38,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreInv: yes
+// SMTIgnoreOS: macos
 // ----
 // Warning 2018: (33-88): Function state mutability can be restricted to view
 // Warning 6328: (367-381): CHC: Assertion violation happens here.
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
index 83ab8873b..e5259c6c4 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) for :C:\n((insidef || (z <= 0)) && (y <= 0))\nReentrancy property(ies) for :C:\n((!insidef || !(<errorCode> >= 2)) && (!(y <= 0) || (y' <= 0)) && (insidef' || !insidef))\n((!insidef || !(<errorCode> >= 3)) && (insidef' || !insidef))\n<errorCode> = 0 -> no errors\n<errorCode> = 2 -> Assertion failed at assert(z == y)\n<errorCode> = 3 -> Assertion failed at assert(prevOwner == owner)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol
index ff2cd7c85..590133a78 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol
@@ -28,5 +28,7 @@ contract C is A {
 // ====
 // SMTEngine: all
 // SMTIgnoreCex: yes
+// SMTIgnoreInv: yes
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (154-168): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
index 98f6d80be..627f79763 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
@@ -28,4 +28,5 @@ contract C {
 // ----
 // Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (302-333): CHC: Assertion violation might happen here.
+// Info 1180: Contract invariant(s) for :C:\n(((kec + ((- 1) * keccak256(data))) >= 0) && ((kec + ((- 1) * keccak256(data))) <= 0))\nReentrancy property(ies) 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<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(_kec == kec)\n<errorCode> = 2 -> Assertion failed at assert(kec == keccak256(_data))\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
index a2b0f1363..5921189b7 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) for :C:\n!(x >= 11)\nReentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!(x <= 10) || !(<errorCode> >= 3)) && (!(x <= 10) || !(x' >= 11)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Overflow at ++x\n<errorCode> = 3 -> Assertion failed at assert(x < 11)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/mutex.sol b/test/libsolidity/smtCheckerTests/external_calls/mutex.sol
index 977115ec0..79b5ac153 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/mutex.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/mutex.sol
@@ -26,4 +26,5 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreInv: yes
 // ----
diff --git a/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol
index 30f4392c5..b7fa57197 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol
@@ -23,3 +23,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 9302: (218-240): Return value of low-level calls not used.
+// Info 1180: Reentrancy property(ies) for :C:\n((!lock || (<errorCode> <= 0)) && (lock' || !lock))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(y == x)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex_2.sol b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex_2.sol
index bccf18caf..f87cf5f74 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex_2.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex_2.sol
@@ -24,3 +24,4 @@ contract C {
 // ----
 // Warning 9302: (212-234): Return value of low-level calls not used.
 // Warning 2018: (164-271): Function state mutability can be restricted to view
+// Info 1180: Reentrancy property(ies) for :C:\n(<errorCode> <= 0)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(y == x)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/staticcall_reentrancy_view.sol b/test/libsolidity/smtCheckerTests/external_calls/staticcall_reentrancy_view.sol
index 96a73cb5d..ee9e57189 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/staticcall_reentrancy_view.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/staticcall_reentrancy_view.sol
@@ -15,3 +15,4 @@ contract C {
 // Warning 2072: (106-112): Unused local variable.
 // Warning 2072: (114-131): Unused local variable.
 // Warning 2018: (72-188): Function state mutability can be restricted to view
+// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol
index 6887c00db..ace2d56f2 100644
--- a/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol
+++ b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol
@@ -16,4 +16,6 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!(x <= 0) || !(<errorCode> >= 2)) && (!(x <= 0) || (x' <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == y)\n<errorCode> = 2 -> Assertion failed at assert(x == y)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
index bc2fa2dc3..5efcb2da1 100644
--- a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
@@ -22,5 +22,7 @@ contract C
 // ====
 // SMTEngine: all
 // SMTIgnoreCex: yes
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (234-253): CHC: Assertion violation happens here.
+// Info 1180: Reentrancy property(ies) 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<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 2 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol
index 93273800e..d83970977 100644
--- 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
 // ----
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> >= 2)\n(<errorCode> <= 0)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 2 -> Assertion failed at assert(map[0] == map[1])\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
index 2afe4b1ff..fb3228aca 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) 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
index 8b4218b45..530b46900 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(a <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol
index b3f6cad02..421c4fd4f 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol
@@ -16,3 +16,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0, 0, 0]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0, 0, 0]\nC.f()
+// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 2)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
index d4e1dc147..ebc7877f0 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
@@ -20,3 +20,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (242-256): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 2)\n!(a[2].length <= 3)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol
index 5a9b13aff..5038294ed 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol
@@ -15,3 +15,4 @@ contract D {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :D:\n(items[1][2][3].y <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol
index b90bc412a..30907bd67 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol
@@ -17,3 +17,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (210-224): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 42\n\nTransaction trace:\nC.constructor()\nC.f()
+// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol
index 7fa0381b6..56032d9d5 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol
@@ -20,3 +20,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (256-270): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n!(m.length <= 0)\n!(m[0][1].length <= 2)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol
index f1afc6e80..c3a3d660d 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol
@@ -21,3 +21,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (274-288): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n!(m[0][1].length <= 2)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol
index 97cc03919..0083f92d8 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol
@@ -24,3 +24,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n!(m[0][1].length <= 2)\n!(m[0][1][2].length <= 3)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol
index 4aca89ef7..43047758e 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol
@@ -19,3 +19,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (260-274): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n!(m[0][1].length <= 2)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol
index ce22da600..2e8abe5dc 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol
@@ -23,3 +23,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (354-368): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n!(m[0][1].length <= 2)\n!(m[0][1][2].length <= 3)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol
index 3ad4d94ae..d7964552d 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol
@@ -19,3 +19,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n!(m[0][1][2].length <= 3)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol
index 5c5af070e..fc4c9efcf 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol
@@ -16,3 +16,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (192-206): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 42\n\nTransaction trace:\nC.constructor()\nC.f()
+// Info 1180: Contract invariant(s) for :C:\n!(m.length <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol
index 1a0f9a799..0b2b6fadf 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol
@@ -18,3 +18,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 42\n\nTransaction trace:\nC.constructor()\nC.f()
+// Info 1180: Contract invariant(s) for :C:\n!(m.length <= 0)\n!(m[0].length <= 1)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol
index 8df8edad4..be6bc2383 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol
@@ -16,3 +16,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (218-232): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 42\n\nTransaction trace:\nC.constructor()\nC.f()
+// Info 1180: Contract invariant(s) for :C:\n!(m.length <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol b/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol
index d77ab04e3..d66545e43 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol
@@ -13,3 +13,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (162-184): CHC: Assertion violation happens here.\nCounterexample:\nx = [42, 1]\n\nTransaction trace:\nC.constructor()\nState: x = [42, 1]\nC.f()
+// Info 1180: Contract invariant(s) for :C:\n!(x.length <= 1)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol
index ddeaa655b..ea433b786 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol
@@ -22,3 +22,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (307-326): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n!(m.b.length <= 2)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol
index 308332700..c3c231ede 100644
--- a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol
+++ b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol
@@ -19,5 +19,7 @@ contract C{
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 5667: (37-43): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Info 1180: Contract invariant(s) for :C:\n!(x >= 2)\n(!(x <= 0) && !(x >= 2))\n(!(x >= 2) && !(x <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol
index 1fe537aad..d067795ac 100644
--- a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol
@@ -26,3 +26,4 @@ contract C{
 // Warning 6328: (137-151): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n    C.g() -- internal call
 // Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n    C.g() -- internal call
 // Warning 6328: (212-226): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n    C.g() -- internal call
+// Info 1180: Contract invariant(s) for :C:\n!(x >= 2)\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
index 3f17744fb..4bca2544e 100644
--- 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.
+// Info 1180: Contract invariant(s) 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
index f03e1b4eb..c0f524e10 100644
--- 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: (49-63): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0)
 // 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
+// Info 1180: Contract invariant(s) 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
index 58d541a8a..85e97661c 100644
--- a/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol
+++ b/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol
@@ -31,3 +31,4 @@ 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
+// Info 1180: Contract invariant(s) for :A:\n((x = 0) || (x = 2))\nContract invariant(s) 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
index 4d69e4815..126add640 100644
--- a/test/libsolidity/smtCheckerTests/functions/this_state.sol
+++ b/test/libsolidity/smtCheckerTests/functions/this_state.sol
@@ -13,3 +13,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 2))\n
diff --git a/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol b/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol
index 4c4a8b246..4c5e38131 100644
--- a/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol
+++ b/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol
@@ -20,3 +20,4 @@ contract C is A {
 // SMTEngine: all
 // ----
 // Warning 6328: (227-241): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.proxy()\n    C.f() -- internal call
+// Info 1180: Contract invariant(s) for :A:\n((x >= 0) && (x <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol b/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol
index 17f3daa79..0117f9b49 100644
--- a/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol
+++ b/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol
@@ -23,6 +23,8 @@ contract C is A {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (199-214): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nA.constructor()\nState: x = 2\nA.i()
 // Warning 6328: (387-401): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.i()
+// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x >= 11) && !(x <= 9))\n
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol
index c86ea3e59..1f05d1176 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol
@@ -16,3 +16,4 @@ contract C is B {
 // SMTEngine: all
 // ----
 // Warning 6328: (52-66): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n    B.f() -- internal call\nState: y = 0, x = 1\nB.f()
+// Info 1180: Contract invariant(s) for :B:\n(x <= 0)\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
index f97bae5cd..a87a8eeb6 100644
--- 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: (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 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
+// Info 1180: Contract invariant(s) for :A:\n(x = 0)\n
diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol
index e70d37230..0a4599a3d 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_uses_function_base.sol
@@ -18,3 +18,4 @@ contract C is B {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(!(y <= 41) && !(y >= 43))\n
diff --git a/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol b/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol
index 959e53d45..b8487e321 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol
@@ -33,3 +33,4 @@ 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
+// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 111))\nContract invariant(s) for :D:\n((x = 0) || (x = 101))\nContract invariant(s) for :E:\n((x = 0) || (x = 111))\nContract invariant(s) for :B:\n((x = 0) || (x = 101))\n
diff --git a/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol b/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol
index 149027691..59d042302 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol
@@ -16,3 +16,4 @@ contract C is B {
 // SMTEngine: all
 // SMTSolvers: z3
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(!(x <= 1) && !(x >= 3))\n
diff --git a/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol b/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol
index 2b1de17cb..653bb23b7 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol
@@ -20,3 +20,4 @@ contract C is B {
 // SMTEngine: all
 // SMTSolvers: z3
 // ----
+// Info 1180: Contract invariant(s) for :A:\n(x <= 0)\nContract invariant(s) for :C:\n(x <= 0)\nContract invariant(s) for :B:\n(x <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol b/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol
index beafa4af0..91b96f78c 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) for :C:\n!(x >= 7)\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
index 9a578cf89..d3467d0b8 100644
--- 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 = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, owner = 0x0\nC.g(1){ msg.sender: 0x0 }
+// Info 1180: Contract invariant(s) for :C:\n(owner <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol
index 13a83ee55..25141b8bf 100644
--- a/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overflow.sol
@@ -15,3 +15,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) 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
index 7da8d0f6a..39be35cb6 100644
--- a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol
+++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol
@@ -39,3 +39,4 @@ 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()
+// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 2))\nContract invariant(s) for :D:\n((x = 0) || (x = 3))\nContract invariant(s) for :B:\n((x = 0) || (x = 1))\n
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations_2.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations_2.sol
index 0a63ed321..5641e2812 100644
--- 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()
+// Info 1180: Contract invariant(s) for :C:\n(x = 3)\n
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol
index 4bd8f328f..43d41f755 100644
--- a/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol
+++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol
@@ -21,3 +21,4 @@ contract C is A {
 // SMTEngine: all
 // ----
 // Warning 6328: (83-98): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()
+// Info 1180: Contract invariant(s) for :C:\n((x >= 0) && (x <= 0))\n
diff --git a/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol b/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol
index 11fcbf6f6..ed160d95c 100644
--- a/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol
+++ b/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol
@@ -28,3 +28,4 @@ contract C {
 // Warning 2018: (33-335): Function state mutability can be restricted to view
 // Warning 2018: (457-524): Function state mutability can be restricted to pure
 // Warning 6328: (135-150): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n(y <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol
index 3331b57de..284f9bcbd 100644
--- 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.
+// Info 1180: Contract invariant(s) for :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/assignment_contract_member_variable_array.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array.sol
index 3df77d2fb..292eab85d 100644
--- 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()
+// Info 1180: Contract invariant(s) 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
index fac19a6ff..7a925d134 100644
--- 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()
+// Info 1180: Contract invariant(s) 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
index d1387ee8e..e4b764686 100644
--- 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()
+// Info 1180: Contract invariant(s) 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
index 17c812aec..9b27a277b 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) 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
index 58afa2413..e37d3f84c 100644
--- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol
@@ -22,5 +22,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 2072: (255-261): Unused local variable.
+// Info 1180: Reentrancy property(ies) for :C:\n((!(x <= 2) || !(x' >= 3)) && (<errorCode> <= 0) && (!(x' <= 0) || !(x >= 2)))\n((!(x' <= 0) || ((x' + ((- 1) * x)) = 0)) && (<errorCode> <= 0) && (!(x' >= 3) || ((x' + ((- 1) * x)) = 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n
diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol
index bda1c07f2..32f2526cc 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) 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
index ea9c4f55a..4f9001115 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) 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
index b0ec97d98..80a692429 100644
--- 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.
+// Info 1180: Contract invariant(s) 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
index f40a02c93..63dad1ab0 100644
--- a/test/libsolidity/smtCheckerTests/operators/delete_function.sol
+++ b/test/libsolidity/smtCheckerTests/operators/delete_function.sol
@@ -28,4 +28,5 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 2)\n
 // Warning 6838: (262-263): BMC: Condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol
index 6de2c9c61..ae526775f 100644
--- a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol
+++ b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol
@@ -23,4 +23,5 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (335-354): CHC: Assertion violation might happen here.
+// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 2)\n!(a.length <= 3)\n
 // Warning 4661: (335-354): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_array_push_2.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_array_push_2.sol
index 0c2fdba6f..b1cef5e40 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) for :C:\n!(data.length <= 1)\n!(data[1].d.length <= 3)\n
diff --git a/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol b/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol
index 8997abbe6..ee57f069d 100644
--- a/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol
+++ b/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol
@@ -18,7 +18,10 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 3944: (181-184): CHC: Underflow (resulting value less than 0) might happen here.
 // Warning 6368: (259-263): CHC: Out of bounds access happens here.\nCounterexample:\na = [0], l = 1\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = [], l = 0\nC.p()\nState: a = [0], l = 1\nC.r()
 // Warning 2661: (112-115): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4144: (181-184): BMC: Underflow (resulting value less than 0) happens here.
diff --git a/test/libsolidity/smtCheckerTests/out_of_bounds/array_2.sol b/test/libsolidity/smtCheckerTests/out_of_bounds/array_2.sol
index 6adc6273c..d331abef7 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) for :C:\n((l + ((- 1) * a.length)) <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol
index afaeb5448..b28b6598c 100644
--- a/test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol
@@ -6,5 +6,6 @@ contract C  {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 0\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, (- 57896044618658097711785492504343953926634992332820282019728792003956564819968))
diff --git a/test/libsolidity/smtCheckerTests/special/msg_value_3.sol b/test/libsolidity/smtCheckerTests/special/msg_value_3.sol
index 8d35e1754..79302b142 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) for :C:\nlock\n
diff --git a/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol
index b7984d21e..475cc2291 100644
--- a/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol
+++ b/test/libsolidity/smtCheckerTests/special/msg_vars_chc_internal.sol
@@ -8,6 +8,7 @@ contract C {
 		sender = msg.sender;
 		sig = msg.sig;
 		value = msg.value;
+		require(value == 42);
 
 		g();
 	}
@@ -28,4 +29,4 @@ contract C {
 // ====
 // SMTEngine: chc
 // ----
-// Warning 6328: (621-644): CHC: Assertion violation happens here.\nCounterexample:\ndata = [0x26, 0x12, 0x1f, 0xf0], sender = 0x0, sig = 0x26121ff0, value = 0\n\nTransaction trace:\nC.constructor()\nState: data = [], sender = 0x0, sig = 0x0, value = 0\nC.f(){ msg.data: [0x26, 0x12, 0x1f, 0xf0], msg.sender: 0x0, msg.sig: 0x26121ff0, msg.value: 0 }\n    C.g() -- internal call
+// Warning 6328: (645-668): CHC: Assertion violation happens here.\nCounterexample:\ndata = [0x26, 0x12, 0x1f, 0xf0], sender = 0x0, sig = 0x26121ff0, value = 42\n\nTransaction trace:\nC.constructor()\nState: data = [], sender = 0x0, sig = 0x0, value = 0\nC.f(){ msg.data: [0x26, 0x12, 0x1f, 0xf0], msg.sender: 0x0, msg.sig: 0x26121ff0, msg.value: 42 }\n    C.g() -- internal call
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_4.sol b/test/libsolidity/smtCheckerTests/try_catch/try_4.sol
index 6988906a2..0abf62df8 100644
--- a/test/libsolidity/smtCheckerTests/try_catch/try_4.sol
+++ b/test/libsolidity/smtCheckerTests/try_catch/try_4.sol
@@ -28,4 +28,5 @@ contract C {
 // Warning 1218: (178-192): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (178-192): CHC: Assertion violation might happen here.
 // Warning 6328: (318-332): CHC: Assertion violation happens here.
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 2)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n<errorCode> = 2 -> Assertion failed at assert(x == 0)\n<errorCode> = 3 -> Assertion failed at assert(x == 1)\n
 // Warning 4661: (178-192): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_5.sol b/test/libsolidity/smtCheckerTests/try_catch/try_5.sol
index 6c9b776c4..236a26f1b 100644
--- 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()
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 2)\n((!(x' >= 100) || ((x' + ((- 1) * x)) = 0)) && !(<errorCode> = 1))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x < 100)\n<errorCode> = 2 -> Assertion failed at assert(x == 0)\n<errorCode> = 3 -> Assertion failed at assert(x == 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
index 80ebe0d93..abef4c76a 100644
--- 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()
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 3)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n<errorCode> = 2 -> Assertion failed at assert(!c)\n<errorCode> = 3 -> Assertion failed at assert(x == 0)\n<errorCode> = 4 -> Assertion failed at assert(x == 1)\n
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol b/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol
index 3048558e7..0854dedd1 100644
--- a/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol
+++ b/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol
@@ -19,5 +19,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (280-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
+// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n(!(m[0][1] >= 43) && !(m[0][1] <= 41))\n
diff --git a/test/libsolidity/smtCheckerTests/typecast/address_literal.sol b/test/libsolidity/smtCheckerTests/typecast/address_literal.sol
index d56275fed..40540bb51 100644
--- a/test/libsolidity/smtCheckerTests/typecast/address_literal.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/address_literal.sol
@@ -23,3 +23,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (454-468): CHC: Assertion violation happens here.\nCounterexample:\nx = 0x0\na = 0x0\nb = 0x01\nc = 0x0\nd = 0x0\ne = 0x12345678\n\nTransaction trace:\nC.constructor()\nState: x = 0x0\nC.g()
+// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/types/address_call.sol b/test/libsolidity/smtCheckerTests/types/address_call.sol
index 568ab91e1..8ea389482 100644
--- a/test/libsolidity/smtCheckerTests/types/address_call.sol
+++ b/test/libsolidity/smtCheckerTests/types/address_call.sol
@@ -19,6 +19,8 @@ contract C
 // EVMVersion: >spuriousDragon
 // SMTEngine: all
 // SMTIgnoreCex: yes
+// SMTIgnoreInv: yes
+// SMTIgnoreOS: macos
 // ----
 // Warning 2072: (127-166): Unused local variable.
 // Warning 2072: (191-207): Unused local variable.
diff --git a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol
index 40d867fa0..11b862a10 100644
--- 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.
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> >= 2)\n!(<errorCode> >= 3)\n!(<errorCode> >= 4)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(success)\n<errorCode> = 2 -> Assertion failed at assert(x == 0)\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n<errorCode> = 4 -> Assertion failed at assert(localMap[0] == 0)\n
diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol
index 36b851ff3..7e89f1c9d 100644
--- 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
 // ----
+// Info 1180: Contract invariant(s) 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
index c13842daa..fad9d2bba 100644
--- 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)
+// Info 1180: Contract invariant(s) 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
index ebd28101d..b2fd91327 100644
--- 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.
+// Info 1180: Contract invariant(s) for :C:\n!(c.length <= 0)\n
diff --git a/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol b/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol
index 6ec629c9f..689fc045d 100644
--- a/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol
+++ b/test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol
@@ -23,3 +23,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.
+// Info 1180: Contract invariant(s) 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
index 07e09a9e8..dd0d8e004 100644
--- 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.
+// Info 1180: Contract invariant(s) 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
index cde229e4f..f415cfd95 100644
--- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol
+++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol
@@ -28,3 +28,4 @@ contract C
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (456-487): CHC: Assertion violation happens here.
+// Info 1180: Contract invariant(s) for :C:\n!(severalMaps3d.length <= 1)\n!(severalMaps8.length <= 1)\n
diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
index 8ebd7025d..f9aa3a650 100644
--- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
+++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
@@ -33,3 +33,4 @@ contract C
 // Warning 6328: (860-880): CHC: Assertion violation happens here.
 // Warning 6368: (936-952): CHC: Out of bounds access might happen here.
 // Warning 6368: (936-955): CHC: Out of bounds access might happen here.
+// Info 1180: Contract invariant(s) for :C:\n!(severalMaps8.length <= 1)\n
diff --git a/test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol b/test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol
index fda74030e..edc35f802 100644
--- a/test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol
+++ b/test/libsolidity/smtCheckerTests/types/enum_explicit_values.sol
@@ -11,3 +11,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n((d = 0) || (d = 1))\n
diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol
index 2aee19042..6a24c1e9c 100644
--- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol
+++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol
@@ -7,3 +7,4 @@ contract c {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :c:\n!(data2.length <= 5)\n
diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol
index 941cfd237..b55293231 100644
--- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol
+++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol
@@ -30,5 +30,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
+// Warning 6368: (374-381): CHC: Out of bounds access might happen here.
 // Warning 6368: (456-462): CHC: Out of bounds access happens here.
+// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 4)\n
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_4.sol b/test/libsolidity/smtCheckerTests/types/mapping_4.sol
index c5b035740..ba6688cd5 100644
--- a/test/libsolidity/smtCheckerTests/types/mapping_4.sol
+++ b/test/libsolidity/smtCheckerTests/types/mapping_4.sol
@@ -10,3 +10,4 @@ contract C
 // SMTEngine: all
 // SMTSolvers: z3
 // ----
+// Info 1180: Contract invariant(s) for :C:\n!map[true]\n
diff --git a/test/libsolidity/smtCheckerTests/types/static_array_length_5.sol b/test/libsolidity/smtCheckerTests/types/static_array_length_5.sol
index f632f3bc8..e3ab2189c 100644
--- a/test/libsolidity/smtCheckerTests/types/static_array_length_5.sol
+++ b/test/libsolidity/smtCheckerTests/types/static_array_length_5.sol
@@ -11,3 +11,4 @@ contract C {
 // ----
 // Warning 6328: (95-115): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0]\nC.f()
 // Warning 6328: (134-154): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0]\nC.f()
+// Info 1180: Contract invariant(s) for :C:\n(!(a.length <= 1) && !(a.length >= 3))\n
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_state_constructor.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_state_constructor.sol
index 7c31c616c..986781b77 100644
--- a/test/libsolidity/smtCheckerTests/types/struct/struct_state_constructor.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_state_constructor.sol
@@ -13,3 +13,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Contract invariant(s) for :C:\n(!(s.x <= 41) && !(s.x >= 43))\n
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol
index f1b128162..60b305402 100644
--- a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol
+++ b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol
@@ -12,3 +12,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> >= 2)\n(<errorCode> <= 0)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2)\n<errorCode> = 2 -> Assertion failed at assert(y == 3)\n
diff --git a/test/libsolidity/smtCheckerTests/userTypes/mapping_1.sol b/test/libsolidity/smtCheckerTests/userTypes/mapping_1.sol
index 52ea82800..120348a04 100644
--- a/test/libsolidity/smtCheckerTests/userTypes/mapping_1.sol
+++ b/test/libsolidity/smtCheckerTests/userTypes/mapping_1.sol
@@ -6,5 +6,8 @@ contract C {
 		assert(m[a] != 0); // should fail
 	}
 }
+// ====
+// SMTEngine: all
+// SMTIgnoreInv: yes
 // ----
 // Warning 6328: (134-151): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\n\nTransaction trace:\nC.constructor()\nC.f(0)