Чтение модели в строковом языке из SMT-форматов и перекодировка в программу-предикат на Рефале.