SMTChecker tests

2023-10-03 13:03:40 +00:00 · 2021-10-06 11:53:03 +02:00 · 2021-10-06 11:53:03 +02:00 · 38b0cf7f9c
commit 38b0cf7f9c
parent 2cbd496576
141 changed files with 169 additions and 6 deletions
--- 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()
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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.
--- 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()
--- 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
 // ----
--- 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
--- 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
--- 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.
--- 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()
--- 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
--- 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
--- 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
--- 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.
--- 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
--- 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
--- 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.
--- 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
--- 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
--- 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.
--- 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
--- 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.
--- 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
--- 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.
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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.
--- 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
--- 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.
--- 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.
--- 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
--- 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
 // ----
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- a/Show More
+++ b/Show More