Add experimental support for optimization (requires Z3 build after changeset 9cba63c31f6f1466dd4ef442bb840d1ab84539c7).

1 files changed, 6 insertions, 0 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index c33f0743..2e33e1dd 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -3218,8 +3218,14 @@ namespace Microsoft.Boogie {
       this.Expr.Emit(stream);
       stream.WriteLine(";");
     }
+    public override void Resolve(ResolutionContext rc) {
+      //Contract.Requires(rc != null);
+      ResolveAttributes(Attributes, rc);
+      base.Resolve(rc);
+    }
     public override void Typecheck(TypecheckingContext tc) {
       //Contract.Requires(tc != null);
+      TypecheckAttributes(Attributes, tc);
       Expr.Typecheck(tc);
       Contract.Assert(Expr.Type != null);  // follows from Expr.Typecheck postcondition
       if (!Expr.Type.Unify(Type.Bool)) {