Merge pull request #10623 from ethereum/smt_const_expr

[SMTChecker] Apply const eval to arithmetic binary expressions

test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol

@@ -50,7 +50,9 @@ contract MyConc{
     }
 
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 2519: (773-792): This declaration shadows an existing declaration.
 // Warning 2018: (1009-1086): Function state mutability can be restricted to view
-// Warning 4984: (985-1002): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nA = 1, should_be_constant = 0, should_be_constant_2 = 2, not_constant = 0, not_constant_2 = 115792089237316195423570985008687907853269984665640564039457584007913129639926, not_constant_3 = 0\n\nTransaction trace:\nconstructor()
+// Warning 4984: (985-1002): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/operators/const_exp_1.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint constant x = 2;
+	uint constant y = x ** 10;
+
+	function f() public view {
+		assert(y == 2 ** 10);
+		assert(y == 1024);
+		assert(y == 14); // should fail
+	}
+}
+// ----
+// Warning 2018: (98-206): Function state mutability can be restricted to pure
+// Warning 6328: (172-187): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, y = 1024\n\n\n\nTransaction trace:\nconstructor()\nState: x = 2, y = 1024\nf()

test/libsolidity/smtCheckerTests/operators/constant_propagation_1.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint constant DEPOSIT_CONTRACT_TREE_DEPTH = 32;
+	uint constant MAX_DEPOSIT_COUNT = 2**DEPOSIT_CONTRACT_TREE_DEPTH - 1;
+	function f() public pure {
+		assert(DEPOSIT_CONTRACT_TREE_DEPTH == 32);
+		assert(MAX_DEPOSIT_COUNT == 4294967295);
+		assert(MAX_DEPOSIT_COUNT == 2); // should fail
+	}
+}
+// ----
+// Warning 6328: (284-314): CHC: Assertion violation happens here.\nCounterexample:\nDEPOSIT_CONTRACT_TREE_DEPTH = 32, MAX_DEPOSIT_COUNT = 4294967295\n\n\n\nTransaction trace:\nconstructor()\nState: DEPOSIT_CONTRACT_TREE_DEPTH = 32, MAX_DEPOSIT_COUNT = 4294967295\nf()