//@Description Implement a TreeSet from a HashSet specification.

#include "TreeSet.skh"
#include "HashSetComplete.skh"

pragma options "--bnd-unroll-amnt 5 --bnd-inbits 3";


int T = 4;

harness void main(int[T] vals, int tval){ /* automatically rewritten */
	
	HashTable ht = newHashTable();
	Tree t = newTree();
	for(int i=0; i<T; ++i){
		bit t1;
		t1 =  addh(ht, vals[i]);
		bit t2;
		t2 = addt(t, vals[i]);		
		assert t1 == t2;				
	}
	
	
	for(int i=0; i<T; ++i){
		bit t1 =  containsh(ht, vals[i]);
		bit t2 = containst(t, vals[i]);		
		assert t1 && t2;				
	}
	
	assert containsh(ht, tval) == containst(t, tval);

	
}