Removed the set cardinality/subset axiom (with no trigger, it caused …

…test suite to fail; even with a restrictive trigger, it added a few minutes to the test suite)
dafny-lang · Apr 2, 2013 · 10f618e · 10f618e
1 parent 572da62
commit 10f618e
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
@@ -84,8 +84,9 @@ axiom (forall<T> a, b: Set T, y: T :: { Set#Difference(a, b), b[y] }
 function Set#Subset<T>(Set T, Set T): bool;
 axiom(forall<T> a: Set T, b: Set T :: { Set#Subset(a,b) }
   Set#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o]));
-axiom(forall<T> a: Set T, b: Set T :: { Set#Subset(a,b) }
-  Set#Subset(a,b) ==> Set#Card(a) <= Set#Card(b));
+//axiom(forall<T> a: Set T, b: Set T ::
+// { Set#Subset(a,b), Set#Card(a), Set#Card(b) }  // very restrictive trigger
+//  Set#Subset(a,b) ==> Set#Card(a) <= Set#Card(b));
 
 
 function Set#Equal<T>(Set T, Set T): bool;