diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and.sol
new file mode 100644
index 000000000..0bf30e46d
--- /dev/null
+++ b/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
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol
new file mode 100644
index 000000000..ee2307521
--- /dev/null
+++ b/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
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol
new file mode 100644
index 000000000..f49a572cf
--- /dev/null
+++ b/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
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both.sol
new file mode 100644
index 000000000..1a4b1edf5
--- /dev/null
+++ b/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
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol
new file mode 100644
index 000000000..c3b6eb8fc
--- /dev/null
+++ b/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
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or.sol
index d20b1c83c..55c218968 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or.sol
+++ b/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
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol
new file mode 100644
index 000000000..31abebec9
--- /dev/null
+++ b/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
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol
new file mode 100644
index 000000000..c699eaac2
--- /dev/null
+++ b/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
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both.sol
new file mode 100644
index 000000000..323ba8f94
--- /dev/null
+++ b/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
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol
new file mode 100644
index 000000000..4169717cf
--- /dev/null
+++ b/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