Add an explicit trigger so that Z3 doesn't choose an overly generous trigger on SeqIndex

1 files changed, 1 insertions, 1 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 45e1fe83..d722b4dd 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -870,7 +870,7 @@ namespace Microsoft.Dafny {
                   FunctionCall(arg.tok, BuiltinFunction.SeqIndex, predef.DatatypeType, args[i], ie)));

               Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

               rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);

-              q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));

+              q = new Bpl.ForallExpr(ctor.tok, bvs, new Trigger(lhs.tok, true, new List<Bpl.Expr> { lhs, rhs }), Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));

               sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q));

               // axiom (forall params, SeqRank(arg) < DtRank(#dt.ctor(params)));

               CreateBoundVariables(ctor.Formals, out bvs, out args);