Merge pull request #6351 from ethereum/smt_shortcircuit_test

[SMTChecker] Add buggy short circuit test

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public {
+		x = 0;
+		assert((f() > 0) || (f() > 0));
+		// This assertion should NOT fail.
+		// It currently does because the SMTChecker does not
+		// handle short-circuiting properly and inlines f() twice.
+		assert(x == 1);
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (344-358): Assertion violation happens here