Merge

5 files changed, 60 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");

diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
index 6e23c098..77b00b19 100644
--- a/Test/stratifiedinline/Answer
+++ b/Test/stratifiedinline/Answer
@@ -484,3 +484,24 @@ Execution trace:
 

 Boogie program verifier finished with 0 verified, 1 error

 -----

+----- Running regression test bar11.bpl

+bar11.bpl(31,1): Error BP5003: A postcondition might not hold on this return path.

+bar11.bpl(26,1): Related location: This is the postcondition that might not hold.

+Execution trace:

+    bar11.bpl(30,3): anon0

+    Inlined call to procedure foo begins

+        bar11.bpl(15,3): anon0

+        value = 0

+        Inlined call to procedure bar begins

+            bar11.bpl(8,5): anon0

+            value = 1

+        Inlined call to procedure bar ends

+        Inlined call to procedure bar begins

+            bar11.bpl(8,5): anon0

+            value = 2

+        Inlined call to procedure bar ends

+        value = 2

+    Inlined call to procedure foo ends

+

+Boogie program verifier finished with 0 verified, 1 error

+-----

diff --git a/Test/stratifiedinline/bar11.bpl b/Test/stratifiedinline/bar11.bpl
new file mode 100644
index 00000000..baad27a1
--- /dev/null
+++ b/Test/stratifiedinline/bar11.bpl
@@ -0,0 +1,32 @@
+var x: int;

+var y: int;

+procedure boogie_si_record_int(x:int);

+

+procedure {:inline 1} bar()

+modifies y;

+{

+  y := y + 1;

+  call boogie_si_record_int(y);

+}

+

+procedure {:inline 1} foo() 

+modifies x, y;

+{

+  call boogie_si_record_int(x);

+  x := x + 1;

+  call bar();

+  call bar();

+  x := x + 1;

+  call boogie_si_record_int(x);

+}

+

+procedure main()

+requires x == 0;

+requires x == y;

+ensures x != y;

+modifies x, y;

+{

+

+  call foo();

+}

+

diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat
index d731d605..3ba74096 100644
--- a/Test/stratifiedinline/runtest.bat
+++ b/Test/stratifiedinline/runtest.bat
@@ -31,4 +31,7 @@ echo -----
 echo ----- Running regression test bar10.bpl

 %BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar10.bpl

 echo -----

+echo ----- Running regression test bar11.bpl

+%BGEXE% %* /noinfer /stratifiedInline:1 bar11.bpl

+echo -----