fixing bug #26 and #20; full hash-consing of SMT terms used to make refinement literals nominal