Fix: substitution of binding guards does not crash if splits present

Source/DafnyCore/Triggers/QuantifierSplitter.cs

@@ -108,6 +108,10 @@ protected override void VisitOneExpr(Expression expr) {
           splits[quantifier] = SplitQuantifier(quantifier).ToList();
         }
       }
+
+      if (expr is ITEExpr iteExpr && iteExpr.IsBindingGuard) {
+        splits.Remove((ExistsExpr)iteExpr.Test);
+      }
     }
 
     protected override void VisitOneStmt(Statement stmt) {
@@ -119,6 +123,10 @@ protected override void VisitOneStmt(Statement stmt) {
           }
         }
       }
+
+      if (stmt is IfStmt ifStatement && ifStatement.IsBindingGuard) {
+        splits.Remove((ExistsExpr)ifStatement.Guard);
+      }
     }
 
     /// <summary>

Test/git-issues/git-issue-2748.dfy

@@ -0,0 +1,21 @@
+// RUN: %dafny_0 /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function method f(x: int): int { 10 - x * x }
+
+function method BindingGuardTestStmt(): int {
+  var x: nat := 1;
+  assert true by {
+    if i :| 0 <= i < 10 && (f(i) == f(i+1) || f(i) == f(i+2)) {
+    }
+  }
+  2
+}
+
+function method BindingGuardTestExpr(): int {
+  var x: nat := 1;
+  assert true by {
+    var x := if i :| 0 <= i < 10 && (f(i) == f(i+1) || f(i) == f(i+2)) then 1 else 0;
+  }
+  2
+}

Test/git-issues/git-issue-2748.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors

docs/dev/news/2748.fix

@@ -0,0 +1 @@
+substitution of binding guards does not crash if splits present