[SMTChecker] Fix ICE in branch-inline function call-modify local variable

test/libsolidity/smtCheckerTests/complex/slither/external_function.sol

@@ -0,0 +1,96 @@
+pragma experimental SMTChecker;
+
+contract ContractWithFunctionCalled {
+    function funcCalled() external  {
+        uint256 i = 0;
+    }
+}
+
+contract ContractWithFunctionCalledSuper is ContractWithFunctionCalled {
+    function callWithSuper() public {
+        uint256 i = 0;
+    }
+}
+
+contract ContractWithFunctionNotCalled {
+
+    function funcNotCalled3() public {
+
+    }
+
+    function funcNotCalled2() public {
+
+    }
+
+    function funcNotCalled() public {
+
+    }
+
+    function my_func() internal returns(bool){
+        return true;
+    }
+
+}
+
+contract ContractWithFunctionNotCalled2 is ContractWithFunctionCalledSuper {
+    function funcNotCalled() public {
+        uint256 i = 0;
+        address three = address(new ContractWithFunctionNotCalled());
+        three.call(abi.encode(bytes4(keccak256("helloTwo()"))));
+        super.callWithSuper();
+        ContractWithFunctionCalled c = new ContractWithFunctionCalled();
+        c.funcCalled();
+    }
+}
+
+contract InternalCall {
+
+    function() returns(uint) ptr;
+
+    function set_test1() external{
+        ptr = test1;
+    }
+
+    function set_test2() external{
+        ptr = test2;
+    }
+
+    function test1() public returns(uint){
+        return 1;
+    }
+
+    function test2() public returns(uint){
+        return 2;
+    }
+
+    function test3() public returns(uint){
+        return 3;
+    }
+
+    function exec() external returns(uint){
+        return ptr();
+    }
+
+}
+// ----
+// Warning: (760-815): Return value of low-level calls not used.
+// Warning: (117-126): Unused local variable.
+// Warning: (260-269): Unused local variable.
+// Warning: (667-676): Unused local variable.
+// Warning: (75-137): Function state mutability can be restricted to pure
+// Warning: (218-280): Function state mutability can be restricted to pure
+// Warning: (470-539): Function state mutability can be restricted to pure
+// Warning: (1144-1206): Function state mutability can be restricted to pure
+// Warning: (1212-1274): Function state mutability can be restricted to pure
+// Warning: (1280-1342): Function state mutability can be restricted to pure
+// Warning: (714-749): Internal error: Expression undefined for SMT solver.
+// Warning: (799-811): Assertion checker does not yet support the type of this literal (literal_string "helloTwo()").
+// Warning: (782-813): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (771-814): Assertion checker does not yet implement this type of function call.
+// Warning: (825-830): Assertion checker does not yet support the type of this variable.
+// Warning: (887-919): Internal error: Expression undefined for SMT solver.
+// Warning: (690-750): Underflow (resulting value less than 0) happens here
+// Warning: (690-750): Overflow (resulting value larger than 2**160 - 1) happens here
+// Warning: (1057-1068): Assertion checker does not yet implement type function () returns (uint256)
+// Warning: (1120-1131): Assertion checker does not yet implement type function () returns (uint256)
+// Warning: (1403-1408): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		if (true) {
+			address a = g();
+			assert(a == address(0));
+		}
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+}
+// ----
+// Warning: (208-218): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (208-218): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_2.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		if (true) {
+			address a = g();
+			assert(a == address(0));
+		}
+		else
+		{
+			address b = g();
+			assert(b == address(0));
+		}
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+}
+// ----
+// Warning: (271-281): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (271-281): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (186-196): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (271-281): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_3.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		if (true) {
+			address a = g();
+			assert(a == address(0));
+		}
+		if (true) {
+			address a = g();
+			assert(a == address(0));
+		}
+
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+}
+// ----
+// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (189-199): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_branch_4.sol

@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		if (true) {
+			address a = g();
+			assert(a == address(0));
+		}
+		if (true) {
+			address a = h();
+			assert(a == address(0));
+		}
+
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+	function h() public pure returns (address) {
+		address a;
+		return a;
+	}
+
+}
+// ----
+// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (123-133): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (189-199): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (275-285): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_else_branch.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		if (true) {
+		} else {
+			address a = g();
+			assert(a == address(0));
+		}
+	}
+	function g() public pure returns (address) {
+		address x;
+		x = address(0);
+		return x;
+	}
+}
+// ----
+// Warning: (219-229): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (134-144): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (219-229): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_modifier_branch.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	modifier m(address a) {
+		if (true) {
+			a = g();
+			_;
+			assert(a == address(0));
+		}
+	}
+
+	function f(address a) m(a) public pure {
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+}
+// ----
+// Warning: (249-259): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (118-128): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (249-259): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/control_flow/function_call_inside_placeholder_inside_modifier_branch.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	modifier m {
+		if (true)
+			_;
+	}
+
+	function f(address a) m public pure {
+		if (true) {
+			a = g();
+			assert(a == address(0));
+		}
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+}
+// ----
+// Warning: (247-257): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (162-172): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (247-257): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/functions/functions_external_4.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint _x) public pure returns (uint) {
+		return _x;
+	}
+}
+
+contract D
+{
+	C c;
+	function g(uint _y) public view {
+		uint z = c.f(_y);
+		assert(z == _y);
+	}
+}
+// ----
+// Warning: (180-187): Internal error: Expression undefined for SMT solver.
+// Warning: (191-206): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_inline_function_inside_branch.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	address owner;
+	modifier m {
+		if (true)
+			owner = g();
+		_;
+	}
+	function f() m public {
+	}
+	function g() public pure returns (address) {
+		address a;
+		a = address(0);
+		return a;
+	}
+}
+// ----
+// Warning: (205-215): Type conversion is not yet fully supported and might yield false positives.
+// Warning: (205-215): Type conversion is not yet fully supported and might yield false positives.

test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol

@@ -22,5 +22,4 @@ contract C
 	}
 }
 // ----
-// Warning: (86-93): Condition is always true.
 // Warning: (311-324): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_parameters.sol

@@ -15,4 +15,3 @@ contract C
 	}
 }
 // ----
-// Warning: (127-132): Condition is always true.

test/libsolidity/smtCheckerTests/modifiers/modifier_return.sol

@@ -18,4 +18,3 @@ contract C
 	}
 }
 // ----
-// Warning: (138-144): Condition is always false.

test/libsolidity/smtCheckerTests/modifiers/modifier_two_invocations.sol

@@ -17,5 +17,3 @@ contract C
 	}
 }
 // ----
-// Warning: (137-142): Condition is always true.
-// Warning: (155-164): Condition is always true.