Removed AIFramework from Boogie -- use native trivial or native interval-based abstract interpretation instead.

Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie.
Command-line option '/logInfer' has been dropped.

1 files changed, 0 insertions, 5 deletions

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 9bbeada1..66eee658 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -63,11 +63,6 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Absy>() != null);

       return node.StdDispatch(this);

     }

-    public virtual AIVariableExpr VisitAIVariableExpr(AIVariableExpr node) {

-      Contract.Requires(node != null);

-      Contract.Ensures(Contract.Result<AIVariableExpr>() != null);

-      return node;

-    }

     public virtual Cmd VisitAssertCmd(AssertCmd node) {

       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<Cmd>() != null);