New tests

test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero.sol

@@ -0,0 +1,11 @@
+contract C {
+	constructor() payable {
+		assert(address(this).balance == 0); // should fail
+		assert(address(this).balance > 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (40-74): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (93-126): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()

test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol

@@ -0,0 +1,13 @@
+contract C {
+	constructor() payable {
+		require(msg.value > 100);
+	}
+	function f() public view {
+		assert(address(this).balance > 100); // should hold
+		assert(address(this).balance > 200); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (153-188): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ value: 101 }\nC.f()

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol

@@ -0,0 +1,17 @@
+contract C {
+	uint prevBalance;
+	constructor() payable {
+		prevBalance = address(this).balance;
+	}
+	function f() public payable {
+		assert(address(this).balance == prevBalance + msg.value); // should fail because there might be funds from selfdestruct/block.coinbase
+		assert(address(this).balance < prevBalance + msg.value); // should fail
+		assert(address(this).balance >= prevBalance + msg.value); // should hold
+		prevBalance = address(this).balance;
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (132-188): CHC: Assertion violation happens here.\nCounterexample:\nprevBalance = 0\n\nTransaction trace:\nC.constructor()\nState: prevBalance = 0\nC.f(){ value: 168 }
+// Warning 6328: (269-324): CHC: Assertion violation happens here.\nCounterexample:\nprevBalance = 0\n\nTransaction trace:\nC.constructor()\nState: prevBalance = 0\nC.f(){ value: 1201 }

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol

@@ -0,0 +1,19 @@
+contract C {
+	uint x;
+	bool once;
+	constructor() payable {
+		x = address(this).balance;
+	}
+	function f() public payable {
+		require(!once);
+		once = true;
+		require(msg.value > 0);
+		assert(address(this).balance > x); // should hold
+		assert(address(this).balance > x + 10); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// 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(){ value: 28100 }\nState: x = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = false\nC.f(){ value: 8 }
+// Warning 6328: (235-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, once = true\n\nTransaction trace:\nC.constructor()\nState: x = 0, once = false\nC.f(){ value: 8 }

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_3.sol

@@ -0,0 +1,9 @@
+contract C {
+	constructor() payable {
+		assert(address(this).balance == msg.value); // should fail because there might be funds from before deployment
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (40-82): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol

@@ -0,0 +1,21 @@
+contract C {
+	uint c;
+	function f() public payable {
+		require(msg.value > 10);
+		++c;
+	}
+	function inv() public view {
+		assert(address(this).balance >= c * 10); // should hold
+		assert(address(this).balance >= c * 12); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// 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(){ value: 11 }\nState: c = 1\nC.inv()
+// 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.

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol

@@ -0,0 +1,14 @@
+contract C {
+	uint sum = msg.value;
+	function f() public payable {
+		sum += msg.value;
+	}
+	function inv() public view {
+		assert(address(this).balance == sum); // should fail
+		assert(address(this).balance >= sum); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (122-158): CHC: Assertion violation happens here.\nCounterexample:\nsum = 0\n\nTransaction trace:\nC.constructor()\nState: sum = 0\nC.inv()

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol

@@ -0,0 +1,26 @@
+contract C {
+	bool once;
+	function f() public payable {
+		require(!once);
+		once = true;
+		require(msg.value == 10);
+		assert(address(this).balance >= 10); // should hold
+		assert(address(this).balance >= 20); // should fail
+		g();
+	}
+	function g() internal view {
+		assert(address(this).balance >= 10); // should hold
+		assert(address(this).balance >= 20); // should fail
+		h();
+	}
+	function h() internal view {
+		assert(address(this).balance >= 10); // should hold
+		assert(address(this).balance >= 20); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (173-208): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ value: 10 }
+// Warning 6328: (321-356): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ value: 10 }\n    C.g(){ value: 10 } -- internal call
+// Warning 6328: (469-504): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ value: 10 }\n    C.g(){ value: 10 } -- internal call\n        C.h(){ value: 10 } -- internal call

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol

@@ -0,0 +1,17 @@
+interface I {
+	function ext() external;
+}
+
+contract C {
+	function f(I _i) public {
+		uint x = address(this).balance;
+		_i.ext();
+		assert(address(this).balance == x); // should fail
+		assert(address(this).balance >= x); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (131-165): CHC: Assertion violation might happen here.

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol

@@ -0,0 +1,13 @@
+contract C {
+	function f(address _a) public {
+		uint x = address(this).balance;
+		_a.call("");
+		assert(address(this).balance == x); // should fail
+		assert(address(this).balance >= x); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (82-93): Return value of low-level calls not used.
+// Warning 6328: (97-131): CHC: Assertion violation happens here.\nCounterexample:\n\n_a = 0\nx = 5921\n\nTransaction trace:\nC.constructor()\nC.f(0)\n    _a.call("") -- untrusted external call, synthesized as:\n        C.f(0) -- reentrant call\n            _a.call("") -- untrusted external call

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol

@@ -0,0 +1,23 @@
+interface I {
+	function ext() external;
+}
+
+contract C {
+	bool lock;
+	modifier mutex {
+		require(!lock);
+		lock = true;
+		_;
+		lock = false;
+	}
+	function f(I _i) public mutex {
+		uint x = address(this).balance;
+		_i.ext();
+		assert(address(this).balance == x); // should hold
+		assert(address(this).balance < x); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (277-310): CHC: Assertion violation happens here.\nCounterexample:\nlock = true\n_i = 0\nx = 730\n\nTransaction trace:\nC.constructor()\nState: lock = false\nC.f(0)\n    _i.ext() -- untrusted external call

test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol

@@ -0,0 +1,21 @@
+contract C {
+	constructor() payable {
+		require(msg.value > 100);
+	}
+	uint c;
+	function f(address payable _a, uint _v) public {
+		require(_v < 10);
+		require(c < 2);
+		++c;
+		_a.transfer(_v);
+	}
+	function inv() public view {
+		assert(address(this).balance > 80); // should hold
+		assert(address(this).balance > 90); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (280-314): CHC: Assertion violation happens here.\nCounterexample:\nc = 2\n\nTransaction trace:\nC.constructor(){ value: 101 }\nState: c = 0\nC.f(15, 6)\nState: c = 1\nC.f(5599, 8)\nState: c = 2\nC.inv()
+// Warning 1236: (175-190): BMC: Insufficient funds happens here.

test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol

@@ -0,0 +1,23 @@
+contract C {
+	constructor() payable {
+		require(msg.value > 100);
+	}
+	function f(address payable _a, uint _v) public {
+		require(_v < 10);
+		_a.transfer(_v);
+	}
+	function inv() public view {
+		assert(address(this).balance > 0); // should fail
+		assert(address(this).balance > 80); // should fail
+		assert(address(this).balance > 90); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 1218: (193-226): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (193-226): CHC: Assertion violation might happen here.
+// Warning 6328: (245-279): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ value: 101 }\nC.f(0, 7)\nC.f(4, 9)\nC.f(0, 9)\nC.inv()
+// Warning 6328: (298-332): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ value: 101 }\nC.f(4645, 7)\nC.f(4644, 9)\nC.inv()
+// Warning 1236: (141-156): BMC: Insufficient funds happens here.
+// Warning 4661: (193-226): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/blockchain_state/balance_zero.sol

@@ -0,0 +1,11 @@
+contract C {
+	constructor() {
+		assert(address(this).balance == 0); // should fail because there might be funds from before deployment
+		assert(address(this).balance > 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (32-66): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (137-170): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()

test/libsolidity/smtCheckerTests/blockchain_state/balance_zero_2.sol

@@ -0,0 +1,11 @@
+contract C {
+	function f() public view {
+		assert(address(this).balance == 0); // should fail because there might be funds from before deployment
+		assert(address(this).balance > 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (43-77): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (148-181): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/blockchain_state/balance_zero_3.sol

@@ -0,0 +1,18 @@
+contract C {
+	uint x = address(this).balance;
+	constructor() {
+		assert(x == 0); // should fail because there might be funds from before deployment
+		assert(x > 0); // should fail
+	}
+	function f() public view {
+		assert(x == 0); // should fail because there might be funds from before deployment
+		assert(x > 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (65-79): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (150-163): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (213-227): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.f()
+// Warning 6328: (298-311): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

test/libsolidity/smtCheckerTests/blockchain_state/balance_zero_4.sol

@@ -0,0 +1,21 @@
+contract C {
+	uint x = g();
+	function g() internal view returns (uint) {
+		return address(this).balance;
+	}
+	constructor() {
+		assert(x == 0); // should fail because there might be funds from before deployment
+		assert(x > 0); // should fail
+	}
+	function f() public view {
+		assert(x == 0); // should fail because there might be funds from before deployment
+		assert(x > 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (127-141): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (212-225): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (275-289): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.f()
+// Warning 6328: (360-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

test/libsolidity/smtCheckerTests/types/address_transfer_3.sol

@@ -0,0 +1,15 @@
+contract C
+{
+	function f(address payable a) public {
+		require(1000 == address(this).balance);
+		require(100 == a.balance);
+		a.transfer(600);
+		// a == this is not possible because address(this).balance == 1000
+		// and a.balance == 100,
+		// so this should hold in CHC, ignoring the transfer revert.
+		assert(a.balance == 700);
+	}
+}
+// ====
+// SMTEngine: all
+// ----