fixing markings of internal nodes in equality engine
Add the ability to "mute" commands, needed for SMT-LIB compliance.
Better error in case of nonlinear assertions while in linear logic