update to the tests

test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_catch_clauses_2.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+contract C {
+
+	function g() public pure {}
+
+	function f() public view {
+		uint x = 0;
+		bool success = false;
+		try this.g() {
+			success = true;
+			x = 1;
+		} catch Error (string memory /*reason*/) {
+			x = 2;
+		} catch (bytes memory /*reason*/) {
+			x = 3;
+		}
+		assert(x > 0 && x < 4); // should hold
+		assert(x == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (338-352): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_returned_values_with_tuple.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+contract C {
+
+	struct S {
+		uint x;
+		int y;
+	}
+
+	function g() public pure returns (bool b, S memory s) {
+		b = true;
+		s.x = 42;
+		s.y = -1;
+	}
+
+	function f() public view {
+		bool success = false;
+		try this.g() returns (bool b, S memory s) {
+			success = true;
+			assert(b && s.x == 42 && s.y == -1); // should hold
+		} catch {
+		}
+		assert(success); // fails, not guaranteed that there will be no error
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (368-383): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() public returns (uint) {
+		while(1==1)
+			try this.f() returns (uint b) {
+				b = 2;
+			} catch {
+			}
+	}
+}
+// ----
+// Warning 6321: (75-79): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
+// Warning 6838: (91-95): BMC: Condition is always true.

test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+contract C {
+
+	function g() public pure {}
+
+	function f() public view {
+		uint x = 0;
+		bool success = false;
+		try this.g() {
+			success = true;
+			x = 1;
+		} catch Error (string memory /*reason*/) {
+			x = 2;
+		} catch (bytes memory /*reason*/) {
+			x = 3;
+		}
+		assert(x > 0 && x < 4); // should hold
+		assert(x == 0); // should fail
+	}
+}
+// ----
+// Warning 6328: (338-352): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+contract C {
+
+	struct S {
+		uint x;
+		int y;
+	}
+
+	function g() public pure returns (bool b, S memory s) {
+		b = true;
+		s.x = 42;
+		s.y = -1;
+	}
+
+	function f() public view {
+		bool success = false;
+		try this.g() returns (bool b, S memory s) {
+			success = true;
+			assert(b && s.x == 42 && s.y == -1);
+		} catch {
+		}
+		assert(success); // fails, not guaranteed that there will be no error
+	}
+}
+// ----
+// Warning 6328: (353-368): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nC.constructor()\nC.f()