Interactive mode support for multiline input
Better error in case of nonlinear assertions while in linear logic
Fix to bug 497: make justification heuristic's ITE cache context-dependent.