Merge

1 files changed, 3 insertions, 2 deletions

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 19272ef4..54a51d11 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3067,7 +3067,8 @@ namespace Microsoft.Dafny {
           Bpl.Expr Si = FunctionCall(stmt.Tok, BuiltinFunction.SeqIndex, predef.BoxType, S, i);

           Bpl.Trigger tr = new Bpl.Trigger(stmt.Tok, true, new Bpl.ExprSeq(Si));

           // TODO: in the next line, the == should be replaced by something that understands extensionality, for sets and sequences

-          oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, o)));

+          var boxO = etran.BoxIfNecessary(stmt.Tok, o, ((SeqType)s.Collection.Type).Arg);

+          oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, boxO)));

         }

         oInS = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), oInS);

         

@@ -5533,7 +5534,7 @@ namespace Microsoft.Dafny {
       // consider automatically applying induction

       var inductionVariables = new List<BoundVar>();

       foreach (var n in e.BoundVars) {

-        if (VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {

+        if (!n.Type.IsTypeParameter && VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {

           if (CommandLineOptions.Clo.Trace) {

             Console.Write("Applying automatic induction on variable '{0}' of: ", n.Name);

             new Printer(Console.Out).PrintExpression(e);