сделать режим рабочий, в котором выводится только один (основной) ответ, для теста скорости. Основным пока оставить тестовый, с логами и тремя вариантами (пока работаем с БЗ, он идеален для этой цели). Посмотреть по таймаутам, и если модель в среднем в рабочем режиме думает больше, чем 30 секунд, добавлять пояснение, что ответ готовится.
аналогично с formalize - неплохо бы предупреждать пользователя о том, что происходит (формализация, передача в интерпретатор, проверка модели в smt-решателе).
Originally posted by @TonitaN in #73