diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Translator.cs | 5 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 3 |
2 files changed, 4 insertions, 4 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 29632ea4..c21ce5d3 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -7045,13 +7045,14 @@ namespace Microsoft.Dafny { List<Bpl.Expr> args;
CreateBoundVariables(ctor.Formals, out bvs, out args);
Bpl.Expr ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
- // (exists args :: args-have-the-expected-types ==> ct(args) == expr)
+ // (exists args :: args-have-the-expected-types && ct(args) == expr)
Bpl.Expr q = Bpl.Expr.Binary(ctor.tok, BinaryOperator.Opcode.Eq, ct, expr);
if (bvs.Length != 0) {
int i = 0;
Bpl.Expr typeAntecedent = Bpl.Expr.True;
foreach (Formal arg in ctor.Formals) {
- Bpl.Expr wh = GetWhereClause(arg.tok, args[i], Resolver.SubstType(arg.Type, subst), etran);
+ var instantiatedArgType = Resolver.SubstType(arg.Type, subst);
+ Bpl.Expr wh = GetWhereClause(arg.tok, etran.CondApplyUnbox(arg.tok, args[i], arg.Type, instantiatedArgType), instantiatedArgType, etran);
if (wh != null) {
typeAntecedent = BplAnd(typeAntecedent, wh);
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index ea17983f..420c24ab 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1371,7 +1371,6 @@ namespace VC private bool refinementLoopCheckPath(ApiChecker apiChecker, HashSet<VCExprVar> varsToSet, HashSet<VCExprVar> allVars)
{
var assumptions = new List<VCExpr>();
- List<int> temp = null;
var query = new HashSet<string>();
varsToSet.Iter(v => query.Add(v.Name));
@@ -1405,7 +1404,7 @@ namespace VC }
//Console.WriteLine();
- var o = apiChecker.CheckAssumptions(assumptions, out temp);
+ var o = apiChecker.CheckAssumptions(assumptions);
Debug.Assert(o == Outcome.Correct || o == Outcome.Errors);
//Console.WriteLine("Result = " + o.ToString());
apiChecker.LogComment("FindLeast: Query End");
|