Simple conditional expression makes verification fail

[tdardinier]

Silicon fails to verify the following Viper program (which is verified successfully by Carbon). However, Silicon succeeds when the if/else statement is uncommented (even though it should have the same behaviour as the conditional expression).

field d: Int
field l: Ref
field r: Ref
 
predicate tree(x: Ref)
{
   x != null ==> acc(x.d) && acc(x.l) && acc(x.r) && tree(x.l) && tree(x.r)
}

method test(x: Ref, key: Int)
   requires x != null
   requires tree(x)
{
   unfold tree(x)
   if (x.l != null && x.r != null)
   {
      var sub: Ref := x.d > key ? x.l : x.r
      /*
      if (x.d > key) {
         sub := x.l
      }
      else {
         sub := x.r
      }
      */
      assert tree(sub)
   }
}

[mschwerhoff]

That's most likely due to disjunctive aliasing, see also #72 and #232. The if statement forces Silicon to branch, thereby resolving the disjunctive aliasing. The problem should also not arise when running Silicon with --moreCompleteExhale, or when enabling QP algorithms for predicate tree (e.g. by ensures forall x: Ref :: false ==> acc(tree(x), none)).

@tdardinier If you agree, please close this issue as a duplicate.