Incorrect handling of split quantifier expressions in substitution of binding guards

[jtristan]

Reproduction:

function method f(x: int): int { 10 - x * x }

function method BindingGuardTest(): int {
  var x: nat := 1;
  assert true by {
    if i :| 0 <= i < 10 && (f(i) == f(i+1) || f(i) == f(i+2)) {
    }
  }
  2
}

Error:
Unhandled exception. System.AggregateException: One or more errors occurred. (Unable to cast object of type 'Microsoft.Dafny.BinaryExpr' to type 'Microsoft.Dafny.ComprehensionExpr'.) ---> System.InvalidCastException: Unable to cast object of type 'Microsoft.Dafny.BinaryExpr' to type 'Microsoft.Dafny.ComprehensionExpr'. at Microsoft.Dafny.Substituter.SubstituteComprehensionExpr(ComprehensionExpr expr, Boolean forceSubstituteOfBoundVars) in /Users/trjohnb/Code/dafny/Source/Dafny/Substituter.cs:line 920 at Microsoft.Dafny.Substituter.SubstStmt(Statement stmt) in /Users/trjohnb/Code/dafny/Source/Dafny/Substituter.cs:line 683

[cpitclaudel]

Adding a copy of the comment I wrote accompanying the report of this issue in #2745 in relation to the implementation of Substitute:

Substitute(q.SplitQuantifierExpression); was always wrong: it takes a quantifier and returns a conjunction or disjunction of quantifiers, so when applied to the BindingGuard of an If it replaces an ExistsExpr with a BinaryExpr, which confuses later parts of the code.