add daikon results.
Add invariant annotations and exepcted results