diff options
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/Translator.cs | 5 |
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);
|