addressing review comments

libsolidity/formal/BMC.cpp

@@ -354,7 +354,8 @@ bool BMC::visit(TryStatement const& _tryStatement)
 	auto callExpr = expr(*externalCall);
 	if (_tryStatement.successClause()->parameters())
 		tryCatchAssignment(
-			_tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall));
+			_tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall)
+		);
 
 	smtutil::Expression clauseId = m_context.newVariable("clause_choice_" + to_string(m_context.newUniqueId()), smtutil::SortProvider::uintSort);
 	auto const& clauses = _tryStatement.clauses();

libsolidity/formal/CHC.cpp

@@ -548,38 +548,29 @@ bool CHC::visit(TryStatement const& _tryStatement)
 	solAssert(m_currentFunction, "");
 
 	auto tryHeaderBlock = createBlock(&_tryStatement, PredicateType::FunctionBlock, "try_header_");
-	auto tryAfterCallSuccessBlock = createBlock(&_tryStatement, PredicateType::FunctionBlock, "try_after_call_success_");
-	auto tryAfterCallFailBlock = createBlock(&_tryStatement, PredicateType::FunctionBlock, "try_after_call_fail_");
 	auto afterTryBlock = createBlock(&m_currentFunction->body(), PredicateType::FunctionBlock);
 
-	connectBlocks(m_currentBlock, predicate(*tryHeaderBlock));
-	setCurrentBlock(*tryHeaderBlock);
-	// fine-grained control over how the external call is visited
-	// cannot use "_tryStatement.externalCall().accept(*this);" since we need to insert the "connectBlocks"
-	// visit(*externalCall); currently there is nothing to do here, so it's commented out
-	externalCall->expression().accept(*this);
-	ASTNode::listAccept(externalCall->arguments(), *this);
-	connectBlocks(m_currentBlock, predicate(*tryAfterCallFailBlock));
-	endVisit(*externalCall);
-
-	if (_tryStatement.successClause()->parameters())
-		tryCatchAssignment(
-			_tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall));
-
-	connectBlocks(m_currentBlock, predicate(*tryAfterCallSuccessBlock));
-
 	auto const& clauses = _tryStatement.clauses();
 	solAssert(clauses[0].get() == _tryStatement.successClause(), "First clause of TryStatement should be the success clause");
 	auto clauseBlocks = applyMap(clauses, [this](ASTPointer<TryCatchClause> clause) {
 		return createBlock(clause.get(), PredicateType::FunctionBlock, "try_clause_" + std::to_string(clause->id()));
 	});
 
-	setCurrentBlock(*tryAfterCallSuccessBlock);
+	connectBlocks(m_currentBlock, predicate(*tryHeaderBlock));
-	connectBlocks(m_currentBlock, predicate(*clauseBlocks[0]));
+	setCurrentBlock(*tryHeaderBlock);
-
+	// Visit everything, except the actual external call.
-	setCurrentBlock(*tryAfterCallFailBlock);
+	externalCall->expression().accept(*this);
+	ASTNode::listAccept(externalCall->arguments(), *this);
+	// Branch directly to all catch clauses, since in these cases, any effects of the external call are reverted.
 	for (size_t i = 1; i < clauseBlocks.size(); ++i)
 		connectBlocks(m_currentBlock, predicate(*clauseBlocks[i]));
+	// Only now visit the actual call to record its effects and connect to the success clause.
+	endVisit(*externalCall);
+	if (_tryStatement.successClause()->parameters())
+		tryCatchAssignment(
+			_tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall)
+		);
+	connectBlocks(m_currentBlock, predicate(*clauseBlocks[0]));
 
 	for (size_t i = 0; i < clauses.size(); ++i)
 	{

test/libsolidity/smtCheckerTests/try_catch/try_4.sol

@@ -23,6 +23,8 @@ contract C {
 		}
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (211-225): CHC: Assertion violation happens here.\nCounterexample:\nx = (- 1), d = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()
+// Warning 6328: (211-225): CHC: Assertion violation happens here.
-// Warning 6328: (351-365): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()
+// Warning 6328: (351-365): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C {
+
+	function g() public pure returns (bytes memory) {
+		return hex"ffff";
+	}
+
+	function f() public view {
+		try this.g() returns (bytes memory b) {
+			assert(b[0] == bytes1(uint8(255)) && b[1] == bytes1(uint8(255))); // should hold
+			assert(b[0] == bytes1(uint8(0)) || b[1] == bytes1(uint8(0))); // should fail
+		} catch {
+		}
+	}
+}
+// ----
+// Warning 6328: (278-338): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_fixed_bytes.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C {
+
+	function g() public pure returns (bytes2) {
+		return hex"ffff";
+	}
+
+	function f() public view {
+		try this.g() returns (bytes2 b) {
+			assert(uint8(b[0]) == 255 && uint8(b[1]) == 255); // should hold
+			assert(uint8(b[0]) == 0 || uint8(b[1]) == 0); // should fail
+		} catch {
+		}
+	}
+}
+// ----
+// Warning 6328: (250-294): CHC: Assertion violation happens here.