update smtchecker tests with error code

Leo Alt · Leo Alt · commit 830576f1ec1d · 2021-10-13T18:44:44.000+02:00
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol
@@ -10,4 +10,3 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreInv: yes
 // ----
-// 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/blockchain_state/balance_receive_ext_calls.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol
@@ -15,5 +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
+// 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
@@ -12,4 +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
+// 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
@@ -22,4 +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
+// 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/this_does_not_change_external_call.sol b/test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol
@@ -18,4 +18,4 @@ 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
+// 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/external_calls/call_mutex.sol b/test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol
@@ -23,4 +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
+// 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
@@ -15,4 +15,4 @@ contract C {
 // 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
+// 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
@@ -10,4 +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
+// 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
@@ -18,4 +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
+// 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_hash.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash.sol
@@ -28,4 +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
+// 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
@@ -30,4 +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
+// 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
@@ -36,4 +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
+// 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
@@ -41,4 +41,5 @@ contract C {
 // SMTIgnoreInv: yes
 // SMTIgnoreOS: macos
 // ----
-// Info 1180: Reentrancy property(ies) for :C:\n((insidef' || !insidef) && !(<errorCode> >= 3) && (!insidef || ((owner' + ((- 1) * owner)) >= 0)) && (!insidef || ((owner' + ((- 1) * owner)) <= 0)))\n
+// 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
@@ -41,4 +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
+// 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
@@ -31,4 +31,4 @@ contract C is A {
 // SMTIgnoreInv: yes
 // SMTIgnoreOS: macos
 // ----
-// Info 1180: Contract invariant(s) for :C:\n(!(x >= 2) && !(x <= 0))\nContract invariant(s) for :A:\n((x >= 0) && (x <= 0))\nReentrancy property(ies) for :C:\n((!(x' <= 0) || (x <= 0)) && (!(x <= 1) || !(x' >= 2)) && (!(x = 1) || !(<errorCode> >= 7)))\n((!(x' <= 0) || (x <= 0)) && (!(x <= 1) || !(x' >= 2)))\n
+// 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
@@ -28,5 +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
+// 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
@@ -17,4 +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
+// 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
@@ -28,4 +28,3 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreInv: yes
 // ----
-// Info 1180: Reentrancy property(ies) for :C:\n((((x' + ((- 1) * x)) = 0) || !lock) && (<errorCode> <= 0) && (lock' || !lock))\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol
@@ -23,4 +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
+// 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
@@ -24,4 +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
+// 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
@@ -15,4 +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
+// 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
@@ -18,4 +18,4 @@ 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
+// 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
@@ -25,4 +25,4 @@ contract C
 // 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
+// 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
@@ -18,4 +18,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
-// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> >= 2)\n(<errorCode> <= 0)\n
+// 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/operators/conditional_assignment_6.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol
@@ -25,4 +25,4 @@ contract C {
 // 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
+// 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/try_catch/try_4.sol b/test/libsolidity/smtCheckerTests/try_catch/try_4.sol
@@ -28,5 +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
+// 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
@@ -26,4 +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
+// 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
@@ -25,4 +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
+// 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/types/address_call.sol b/test/libsolidity/smtCheckerTests/types/address_call.sol
@@ -22,4 +22,6 @@ contract C
 // SMTIgnoreInv: yes
 // SMTIgnoreOS: macos
 // ----
-// Info 1180: Reentrancy property(ies) for :C:\n(!(<errorCode> >= 2) && (!(x <= 0) || (x' <= 0)))\n
+// Warning 2072: (127-166): Unused local variable.
+// Warning 2072: (191-207): Unused local variable.
+// Warning 6328: (227-242): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol
@@ -20,4 +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
+// 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/tuple_extra_parens_7.sol b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol
@@ -12,4 +12,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> >= 2)\n(<errorCode> <= 0)\n
+// 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
@@ -10,4 +10,4 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreInv: yes
 // ----
-// Info 1180: Contract invariant(s) for :C:\n(true && true)\n
+// Warning 6328: (134-151): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\n\nTransaction trace:\nC.constructor()\nC.f(0)
