diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-04-04 09:34:14 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-04-04 09:34:14 -0700 |
| commit | 3ff2e42970584ad66f8b8e353ddce86dbea92baf (patch) | |
| tree | b506751550be2b708766fc0eca39edddf6ddb8ef | |
| parent | f9d9312fa9c8e649355183e0c46e95ea6ba6e36c (diff) | |
small fix
added regressions
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 31 | ||||
| -rw-r--r-- | Test/stratifiedinline/Answer | 422 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar10.bpl | 41 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar7.bpl | 2 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar8.bpl | 2 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar9.bpl | 45 | ||||
| -rw-r--r-- | Test/stratifiedinline/runtest.bat | 12 |
7 files changed, 540 insertions, 15 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 5667429a..08322ebb 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -838,9 +838,20 @@ namespace Microsoft.Boogie.SMTLib public override Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions, out List<int> unsatisfiedSoftAssumptions, ErrorHandler handler) {
unsatisfiedSoftAssumptions = new List<int>();
- Push();
+ // First, convert both hard and soft assumptions to SMTLIB strings
+ List<string> hardAssumptionStrings = new List<string>();
foreach (var a in hardAssumptions) {
- SendThisVC("(assert " + VCExpr2String(a, 1) + ")");
+ hardAssumptionStrings.Add(VCExpr2String(a, 1));
+ }
+ List<string> currAssumptionStrings = new List<string>();
+ foreach (var a in softAssumptions) {
+ currAssumptionStrings.Add(VCExpr2String(a, 1));
+ }
+
+ Push();
+ AssertAxioms();
+ foreach (var a in hardAssumptionStrings) {
+ SendThisVC("(assert " + a + ")");
}
Check();
Outcome outcome = GetResponse();
@@ -849,17 +860,11 @@ namespace Microsoft.Boogie.SMTLib return outcome;
}
- List<string> currAssumptions = new List<string>();
- foreach (var a in softAssumptions) {
- currAssumptions.Add(VCExpr2String(a, 1));
- }
-
int k = 0;
List<string> relaxVars = new List<string>();
while (true) {
Push();
- AssertAxioms();
- foreach (var a in currAssumptions) {
+ foreach (var a in currAssumptionStrings) {
SendThisVC("(assert " + a + ")");
}
Check();
@@ -870,12 +875,12 @@ namespace Microsoft.Boogie.SMTLib string relaxVar = "relax_" + k;
relaxVars.Add(relaxVar);
SendThisVC("(declare-fun " + relaxVar + " () Int)");
- List<string> nextAssumptions = new List<string>();
- for (int i = 0; i < currAssumptions.Count; i++) {
+ List<string> nextAssumptionStrings = new List<string>();
+ for (int i = 0; i < currAssumptionStrings.Count; i++) {
string constraint = "(= " + relaxVar + " " + i + ")";
- nextAssumptions.Add("(or " + currAssumptions[i] + " " + constraint + ")");
+ nextAssumptionStrings.Add("(or " + currAssumptionStrings[i] + " " + constraint + ")");
}
- currAssumptions = nextAssumptions;
+ currAssumptionStrings = nextAssumptionStrings;
k++;
}
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index aee2722e..6e23c098 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -62,3 +62,425 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
-----
+----- Running regression test bar7.bpl
+bar7.bpl(42,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar7.bpl(35,5): anon0
+ bar7.bpl(37,5): anon4_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar7.bpl(7,3): anon0
+ bar7.bpl(7,3): anon2_Else
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ bar7.bpl(42,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar8.bpl
+bar8.bpl(41,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar8.bpl(34,5): anon0
+ bar8.bpl(36,5): anon4_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar8.bpl(7,3): anon0
+ bar8.bpl(7,3): anon2_Else
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ bar8.bpl(41,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar9.bpl
+bar9.bpl(44,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar9.bpl(35,5): anon0
+ bar9.bpl(41,5): anon4_Else
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(18,7): anon2_Then
+ Inlined call to procedure bar1 begins
+ bar9.bpl(16,3): anon0
+ bar9.bpl(16,3): anon2_Else
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(27,7): anon2_Then
+ Inlined call to procedure bar2 begins
+ bar9.bpl(26,3): anon0
+ bar9.bpl(26,3): anon2_Else
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure bar2 ends
+ bar9.bpl(44,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar10.bpl
+bar10.bpl(40,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar10.bpl(35,5): anon0
+ Inlined call to procedure bar1 begins
+ bar10.bpl(16,3): anon0
+ bar10.bpl(16,3): anon2_Else
+ Inlined call to procedure bar1 ends
+ Inlined call to procedure bar2 begins
+ bar10.bpl(26,3): anon0
+ bar10.bpl(26,3): anon2_Else
+ Inlined call to procedure bar2 ends
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(8,9): anon2_Then
+ Inlined call to procedure foo begins
+ bar10.bpl(7,3): anon0
+ bar10.bpl(7,3): anon2_Else
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
diff --git a/Test/stratifiedinline/bar10.bpl b/Test/stratifiedinline/bar10.bpl new file mode 100644 index 00000000..8cfcfc13 --- /dev/null +++ b/Test/stratifiedinline/bar10.bpl @@ -0,0 +1,41 @@ +var i: int;
+var m: int;
+
+procedure {:inline 1} foo()
+modifies i;
+{
+ if (i < 20) {
+ i := i + 1;
+ call foo();
+ }
+}
+
+procedure {:inline 1} bar1(j: int)
+modifies i;
+{
+ if (j < 2*m)
+ {
+ i := i + 1;
+ call bar1(j+1);
+ }
+}
+
+procedure {:inline 1} bar2(j: int)
+modifies i;
+{
+ if (j < m) {
+ i := i - 1;
+ call bar2(j+1);
+ }
+}
+
+procedure main()
+modifies i;
+{
+ i := 0;
+ call bar1(0);
+ call bar2(0);
+ i := 0;
+ call foo();
+ assert i < 10;
+}
\ No newline at end of file diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl index 747510de..b28777bd 100644 --- a/Test/stratifiedinline/bar7.bpl +++ b/Test/stratifiedinline/bar7.bpl @@ -4,7 +4,7 @@ var m: int; procedure {:inline 1} foo()
modifies i;
{
- if (i < 80) {
+ if (i < 20) {
i := i + 1;
call foo();
}
diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl index d447e3a7..e96655f3 100644 --- a/Test/stratifiedinline/bar8.bpl +++ b/Test/stratifiedinline/bar8.bpl @@ -4,7 +4,7 @@ var m: int; procedure {:inline 1} foo()
modifies i;
{
- if (i < 80) {
+ if (i < 20) {
i := i + 1;
call foo();
}
diff --git a/Test/stratifiedinline/bar9.bpl b/Test/stratifiedinline/bar9.bpl new file mode 100644 index 00000000..12de78ad --- /dev/null +++ b/Test/stratifiedinline/bar9.bpl @@ -0,0 +1,45 @@ +var i: int;
+var m: int;
+
+procedure {:inline 1} foo(x: int)
+modifies i;
+{
+ if (i < x) {
+ i := i + 1;
+ call foo(x);
+ }
+}
+
+procedure {:inline 1} bar1(j: int)
+modifies i;
+{
+ if (j < 2*m)
+ {
+ i := i + 1;
+ call bar1(j+1);
+ }
+}
+
+procedure {:inline 1} bar2(j: int)
+modifies i;
+{
+ if (j < m) {
+ i := i - 1;
+ call bar2(j+1);
+ }
+}
+
+procedure main()
+modifies i;
+{
+ i := 0;
+ if (*) {
+ call foo(20);
+ i := 0;
+ call foo(4);
+ } else {
+ call bar1(0);
+ call bar2(0);
+ }
+ assert i < 10;
+}
\ No newline at end of file diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat index 194570d0..d731d605 100644 --- a/Test/stratifiedinline/runtest.bat +++ b/Test/stratifiedinline/runtest.bat @@ -19,4 +19,16 @@ echo ----- echo ----- Running regression test bar6.bpl
%BGEXE% %* /noinfer /stratifiedInline:1 bar6.bpl
echo -----
+echo ----- Running regression test bar7.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar7.bpl
+echo -----
+echo ----- Running regression test bar8.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar8.bpl
+echo -----
+echo ----- Running regression test bar9.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar9.bpl
+echo -----
+echo ----- Running regression test bar10.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar10.bpl
+echo -----
|