Fixing bounded variable addition

By making sure that repeated clauses don't cause any trouble, and fixing
some other issues. It still does not work in library mode