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)

1 files changed, 3 insertions, 2 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 2f8fb5f7..a89ded50 100644
--- 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;