Z3: использование операторов сравнения (<

#c #z3 #comparison-operators Вопрос: Я храню числа как z3::expr и хочу их сравнить. Я попробовал следующее: z3::context c; z3::expr a = c.real_val("0"); z3::expr b = c.real_val("1"); z3::expr comp = (a…