summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Binaries/DafnyPrelude.bpl15
-rw-r--r--Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy9
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs3
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;