Add a sanity check in QuantifiersCollection

1 files changed, 1 insertions, 0 deletions

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 1d5625cd..0ef59bad 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -34,6 +34,7 @@ namespace Microsoft.Dafny.Triggers {
     readonly List<QuantifierWithTriggers> quantifiers;

    

     internal QuantifiersCollection(IEnumerable<QuantifierExpr> quantifiers, ErrorReporter reporter) {

+      Contract.Requires(quantifiers.All(q => q.SplitQuantifier == null));

       this.reporter = reporter;

       this.quantifiers = quantifiers.Select(q => new QuantifierWithTriggers(q)).ToList();

     }