Does JSC originate with JSCheck?
A: Yes
smap requires an inverse function, which isn't always practical. Is this complexity related to shrinking?
A: Yes. We don't want to give an easy-to-use interface which forgets shrinking altogether. Note, that right inverse is enough, which is most likely easy to write, even complete inverse doesn't exist.