Merge pull request #10801 from blishko/issue-10793

[SMTChecker] Gather local variables also from nested try/catch clauses

libsolidity/formal/SMTEncoder.cpp

@@ -2705,7 +2705,7 @@ vector<VariableDeclaration const*> SMTEncoder::tryCatchVariables(FunctionDefinit
 					vars.push_back(param.get());
 			}
 
-			return false;
+			return true;
 		}
 
 		vector<VariableDeclaration const*> vars;

test/libsolidity/smtCheckerTests/try_catch/try_nested_1.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+contract C {
+	int public x;
+
+	function f() public view {
+		int y = 42;
+		bool success = false;
+		try this.x() returns (int v) {
+			y = v;
+			try this.x() returns (int w) {
+				success = true;
+				y = w;
+			}
+			catch {}
+		} catch {}
+		assert(!success || y == x); // should hold
+		assert(y == 42); // should fail
+	}
+}
+// ----
+// Warning 6328: (312-327): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+contract C {
+	function g() public pure returns (uint, uint) {
+	}
+	function f() public view {
+		uint choice = 42;
+		try this.g() returns (uint, uint) {
+			choice = 10;
+			try this.g() returns (uint, uint) {
+				choice = 1;
+			} catch {
+				choice = 2;
+			}
+		} catch {
+			choice = 3;
+		}
+		assert(choice >= 1 && choice <= 3); // should hold
+		assert(choice == 42); // should fail
+	}
+}
+// ----
+// Warning 6328: (374-394): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_nested_3.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+contract C {
+	function g() public pure returns (uint) {
+	}
+	function f() public view {
+		uint choice = 42;
+		try this.g() returns (uint) {
+			choice = 1;
+		} catch{
+			choice = 10;
+			try this.g() returns (uint) {
+				choice = 2;
+			} catch {
+				choice = 3;
+			}
+		}
+		assert(choice >= 1 && choice <= 3); // should hold
+		assert(choice == 42); // should fail
+	}
+}
+// ----
+// Warning 6328: (355-375): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()