diff options
| author |  stefanheule <unknown> | 2012-02-25 03:23:24 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:23:24 -0800 |
| commit | 7715d16742a3ec7b8467587d668514a11d4272b6 (patch) | |
| tree | 44d484e766c211ae675803bdb50b05c3d799e19d | |
| parent | 8e2a3b7af5d7781a055b35f52e4decc0fe940e1e (diff) | |
Chalice: Fix trigger problem (wrongly used limited function as trigger, instead of normal function).
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index add4fafb..2a37af41 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -260,7 +260,7 @@ class Translator { Axiom(new Boogie.Forall(Nil, formalsOnlyReceiver,
triggers,
new Boogie.Forall(formalsWithoutReceiver,
- new Trigger(List(limitedApplyF,wellformed)),
+ new Trigger(List(applyF,wellformed)),
(applyF ==@ limitedApplyF)))) ::
Nil
else
|