Hi Roberto, > I suspect barcelogic does depends on this restrictio. Am I wrong? I don't know which tools depend on this restriction, but I don't see a problem with them since the SMT-LIB specifies this restriction. Leonardo