Short circuit tests

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() == 0) && (f() == 0);
+		assert(x == 1);
+		assert(!b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() == 0) && (f() == 0);
+		assert(x == 1);
+		assert(b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (227-236): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g(bool a) public returns (bool) {
+		bool b;
+		if (a) {
+			x = 0;
+			b = (f() == 0) && (f() == 0);
+			assert(x == 1);
+			assert(!b);
+		} else {
+			x = 100;
+			b = (f() > 0) && (f() > 0);
+			assert(x == 102);
+			// Should fail.
+			assert(!b);
+		}
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (362-372): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() > 0) && (f() > 0);
+		assert(x == 2);
+		assert(b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() > 0) && (f() > 0);
+		assert(x == 2);
+		assert(!b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (225-235): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or.sol

@@ -6,15 +6,13 @@ contract c {
 		x = x + 1;
 		return x;
 	}
-	function g() public {
+	function g() public returns (bool) {
 		x = 0;
 		bool b = (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);
+		assert(b);
+		return b;
 	}
 }
 // ----
 // Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (344-358): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() > 0) || (f() > 0);
+		assert(x == 1);
+		assert(!b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (225-235): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g(bool a) public returns (bool) {
+		bool b;
+		if (a) {
+			x = 0;
+			b = (f() > 0) || (f() > 0);
+			assert(x == 1);
+			assert(b);
+		} else {
+			x = 100;
+			b = (f() == 0) || (f() > 0);
+			assert(x == 102);
+			// Should fail.
+			assert(!b);
+		}
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (360-370): Assertion violation happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() > 1) || (f() > 1);
+		assert(x == 2);
+		assert(b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+		return x;
+	}
+	function g() public returns (bool) {
+		x = 0;
+		bool b = (f() > 1) || (f() > 1);
+		assert(x == 2);
+		assert(!b);
+		return b;
+	}
+}
+// ----
+// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (225-235): Assertion violation happens here