"Invariant unproven" when using method that creates a specific new object in its return statement

The following simple code will yield an "invariant unproven" warning by the static checker of Code Contracts, although there is no way `_foo` can be `null`. The warning is for the `return` statement inside `UncalledMethod`. ``` public class Node { public Node(string s1, string s2, string s3, string s4, object o, string s5) { } } public class Bar { private readonly string _foo; public Bar() { _foo = "foo"; } private object UncalledMethod() { return new Node(string.Empty, string.Empty, string.Empty, string.Empty, GetNode(), string.Empty); } private Node GetNode() { return null; } public string Foo { get { Contract.Ensures(Contract.Result<string>() != null); return _foo; } } [ContractInvariantMethod] private void Invariants() { Contract.Invariant(_foo != null); } } ``` Apart from the fact, that the warning is simply invalid, it only occures in certain specific circumstances. Changing any of the following will make the warning go away: Inline `GetNode` so the return statement looks like this: ``` return new Node(string.Empty, string.Empty, string.Empty, string.Empty, null, string.Empty); ``` - Remove any of the parameters s1 to s5 from the constructor of `Node`. - Change the type of any of the parameters s1 to s5 from the constructor of `Node` to `object`. Use a temporary variable for the result of `GetNode`: ``` var node = GetNode(); return new Node(string.Empty, string.Empty, string.Empty, string.Empty, node, string.Empty); ``` - Changing the order of the parameters of the constructor of `Node`. - Checking the option "Show assumptions" in the code contracts settings pane in the project settings. Am I missing something obvious here or is this simply a bug in the static checker? My settings: My output: ``` C:\{path}\Program.cs(20,9): message : CodeContracts: Suggested ensures: Contract.Ensures(this._foo != null); C:\{path}\Program.cs(41,17): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<System.String>() == this._foo); C:\{path}\Program.cs(33,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<ConsoleApplication3.Program+Node>() == null); C:\{path}\Program.cs(27,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<System.Object>() != null); C:\{path}\Program.cs(55,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.ForAll(0, args.Length, __k__ => args[__k__] != 0)); CodeContracts: ConsoleApplication3: Validated: 92,3% CodeContracts: ConsoleApplication3: Contract density: 1,81 CodeContracts: ConsoleApplication3: Total methods analyzed 8 CodeContracts: ConsoleApplication3: Methods with 0 warnings 7 CodeContracts: ConsoleApplication3: Total method analysis read from the cache 8 CodeContracts: ConsoleApplication3: Total time 2,522sec. 315ms/method CodeContracts: ConsoleApplication3: Retained 0 preconditions after filtering CodeContracts: ConsoleApplication3: Inferred 0 object invariants CodeContracts: ConsoleApplication3: Retained 0 object invariants after filtering CodeContracts: ConsoleApplication3: Detected 0 code fixes CodeContracts: ConsoleApplication3: Proof obligations with a code fix: 0 C:\{path}\Program.cs(27,13): warning : CodeContracts: invariant unproven: _foo != null C:\{path}\Program.cs(49,13): warning : + location related to previous warning C:\windows\system32\ConsoleApplication3.exe(1,1): message : CodeContracts: Checked 13 assertions: 12 correct 1 unknown CodeContracts: ConsoleApplication3: CodeContracts: ConsoleApplication3: Background contract analysis done. ```