diff options
| author |  Unknown <Alex@Mehldau.inf.ethz.ch> | 2014-03-03 13:56:55 +0100 |
|---|---|---|
| committer | Unknown <Alex@Mehldau.inf.ethz.ch> | 2014-03-03 13:56:55 +0100 |
| commit | 2b2d7c7f4ec6226c54ad664ce390fefdaf8fecaf (patch) | |
| tree | 76e38254c3e129022d0454ad0042803b946583ef /Test/test0/Triggers1.bpl | |
| parent | 7a5fa3b224d6cf8015bd9792f7bff5074f82932d (diff) | |
disabled quantifier merging, except when no triggers are provided (as discussed with Rustan)
Diffstat (limited to 'Test/test0/Triggers1.bpl')
| -rw-r--r-- | Test/test0/Triggers1.bpl | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/Test/test0/Triggers1.bpl b/Test/test0/Triggers1.bpl index 02c63406..d079ea03 100644 --- a/Test/test0/Triggers1.bpl +++ b/Test/test0/Triggers1.bpl @@ -99,17 +99,17 @@ axiom (forall x: int, y: int :: {:nopats f(g,g) } // but it is okay not to mention the bound variables (in a pattern exclusion)
x < y);
-// --- merging of nested quantifiers
+// --- merging of nested quantifiers (disabled unless both have no triggers)
-axiom (forall x:int :: (forall y:int :: { f(x,y) } f(x,y) > 0)); // OK
+axiom (forall x:int :: (forall y:int :: { f(x,y) } f(x,y) > 0)); // OK, but no merging - outer quantifier has no trigger
axiom (forall x:int :: (forall y:int :: { f(x,x) } f(x,x) > 0)); // error
-axiom (forall x:int :: (forall y:int :: { f(y,y) } f(y,y) > 0)); // error
+axiom (forall x:int :: (forall y:int :: { f(y,y) } f(y,y) > 0)); // OK - no merging
// three levels
-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y) } f(y,y) > 0))); // error
-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,z) } f(y,y) > 0))); // error
-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(y,z) } f(y,y) > 0))); // error
-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y), f(y,z) } f(y,y) > 0))); // OK
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y) } f(y,y) > 0))); // error - z not mentioned
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,z) } f(y,y) > 0))); // OK - only outer two quantifiers are merged
+//axiom (forall x:int :: (forall y:int :: (forall z:int :: f(y,y) > 0))); // OK - all three are merged
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y), f(y,z) } f(y,y) > 0))); // OK - but not a trigger for outer x,y (which get merged)
// --- no free variables
|