Add/update tests

test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint t;
+	constructor() {
+		t = address(this).balance;
+	}
+	function f(address payable a, uint x) public {
+		require(address(this).balance >= x);
+		a.transfer(x);
+	}
+	function inv() public view {
+		// If only looking at `f`, it looks like this.balance always decreases.
+		// However, the edge case of a contract `selfdestruct` sending its remaining balance
+		// to this contract should make the claim false (since there's no fallback/receive here).
+		assert(address(this).balance == t);
+	}
+}
+// ----
+// Warning 6328: (496-530): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	address t;
+	constructor() {
+		t = address(this);
+	}
+	function inv() public view {
+		assert(address(this) == t);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	address t;
+	constructor() {
+		t = address(this);
+	}
+	function f(D d) public {
+		address a = address(this);
+		d.d();
+		assert(address(this) == t);
+		assert(a == t);
+	}
+}

test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_internal_call.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	address t;
+	constructor() {
+		t = address(this);
+	}
+	function f() public view {
+		g(address(this));
+	}
+	function g(address a) internal view {
+		assert(a == t);
+		assert(a == address(this));
+	}
+}

test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(address payable a) public {
+		require(address(this).balance > 1000);
+		a.transfer(666);
+		assert(address(this).balance > 100);
+		// Fails.
+		assert(address(this).balance > 500);
+	}
+}
+// ----
+// Warning 6328: (199-234): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/functions_external_2.sol

@@ -17,4 +17,3 @@ contract C
 	}
 }
 // ----
-// Warning 4661: (297-321): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol

@@ -15,3 +15,4 @@ contract C
 }
 // ----
 // Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4661: (296-309): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol

@@ -30,4 +30,3 @@ contract C {
 // Warning 6328: (327-354): CHC: Assertion violation happens here.
 // Warning 6328: (376-405): CHC: Assertion violation happens here.
 // Warning 6328: (430-465): CHC: Assertion violation happens here.
-// Warning 6328: (493-534): CHC: Assertion violation happens here.