disabled quantifier merging, except when no triggers are provided (as discussed with Rustan)

1 files changed, 1 insertions, 4 deletions

diff --git a/Test/test0/Answer b/Test/test0/Answer
index f92dd1dc..f4e2b981 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -21,13 +21,10 @@ Triggers1.bpl(82,7): Error: trigger must mention all quantified variables, but d
 Triggers1.bpl(94,16): Error: a matching pattern must be more than just a variable by itself: x

 Triggers1.bpl(95,16): Error: a matching pattern must be more than just a variable by itself: g

 Triggers1.bpl(105,40): Error: trigger must mention all quantified variables, but does not mention: y

-Triggers1.bpl(106,40): Error: trigger must mention all quantified variables, but does not mention: x

 Triggers1.bpl(109,57): Error: trigger must mention all quantified variables, but does not mention: z

-Triggers1.bpl(110,57): Error: trigger must mention all quantified variables, but does not mention: y

-Triggers1.bpl(111,57): Error: trigger must mention all quantified variables, but does not mention: x

 Triggers1.bpl(119,33): Error: cannot refer to a global variable in this context: h1

 Triggers1.bpl(120,33): Error: cannot refer to a global variable in this context: h0

-23 name resolution errors detected in Triggers1.bpl

+20 name resolution errors detected in Triggers1.bpl

 const x: int;

 

 const y: int;