better (aka sound) types for data projectors; short-circuiting semantics for logical connectives in VC generation; other little bug fixes
adding rbtree to the regression suite