fixed bug related to conditionally pure arguments being passed to functions; you can now write f (g x) and it should work instead of sometimes needing to write let y = g x in f y; but, in some cases, the former style produces VCs that Z3 chokes on, e.g, rbtree takes MUCH longer when a couple of the applications are written that way