3 files changed, 0 insertions, 27 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 53e8e86a..5530f8a7 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -610,18 +610,3 @@ type TickType;
 var $Tick: TickType;
 
 // ---------------------------------------------------------------
-// -- Arithmetic -------------------------------------------------
-// ---------------------------------------------------------------
-
-// the connection between mod and div
-axiom (forall x:int, y:int :: {x mod y} {x div y}  x mod y == x - x div y * y);
-
-// remainder is always Euclidean Modulus.
-axiom (forall x:int, y:int :: {x mod y}  0 < y  ==>  0 <= x mod y  &&  x mod y < y);
-axiom (forall x:int, y:int :: {x mod y}  y < 0  ==>  0 <= x mod y  &&  x mod y < -y);
-
-// the following axiom has some unfortunate matching, but it does state a property about mod that
-// is sometimes useful
-axiom (forall a: int, b: int, d: int :: { a mod d, b mod d } 2 <= d && a mod d == b mod d && a < b  ==>  a + d <= b);
-
-// ---------------------------------------------------------------
diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
index 3f68ee5d..774008b8 100644
--- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
@@ -205,7 +205,6 @@ class Node {
       invariant forall k,l :: 0 <= k < l < steps ==> Nexxxt(k, S) != Nexxxt(l, S);
       decreases S - Visited;
     {
-assume 2<2;  // TEMPORARY HACK
       p, steps, Visited := p.next, steps + 1, Visited + {p};
     }
     if (p == null) {
@@ -219,7 +218,6 @@ assume 2<2;  // TEMPORARY HACK
         invariant forall k :: 0 <= k < A ==> Nexxxt(k, S) != p;
         decreases steps - A;
       {
-assume 2<2;  // TEMPORARY HACK
         A := A + 1;
       }
       B := steps - A;
@@ -228,13 +226,6 @@ assume 2<2;  // TEMPORARY HACK
     }
   }
 
-/**  TEMPORARY
-  ghost method AnalyzeList_Aux(S: set<Node>, steps: int, p: Node) returns (A: int)
-    ensures 0 <= A < steps;
-    ensures forall k :: 0 <= k < A ==> Nexxxt(k, S) != p;
-    ensures Nexxxt(A, S) == p;
-**/
-
   ghost method CrucialLemma(a: int, b: int, S: set<Node>)
     requires IsClosed(S);
     requires 0 <= a && 1 <= b;
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index 9f22b887..c691d9da 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -231,9 +231,6 @@ namespace DafnyLanguage
       if (Bpl.CommandLineOptions.Clo.UseAbstractInterpretation) {
         if (Bpl.CommandLineOptions.Clo.Ai.J_Intervals || Bpl.CommandLineOptions.Clo.Ai.J_Trivial) {
           Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
-        } else if (Bpl.CommandLineOptions.Clo.Ai.AnySet) {
-          // run one of the old domains
-          Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);
         } else {
           // use /infer:j as the default
           Bpl.CommandLineOptions.Clo.Ai.J_Intervals = true;