Previously, models were retrieved using get-model, which could cause issues when minimizing invariants for Lustre models with arrays encoded as values of an uninterpreted sort, FArray, with arity 2. If the Lustre model includes arrays for two different element types (e.g., FArray Int Bool and FArray Int Int), Z3 returns models where the universes for FArray Int Bool and FArray Int Int may contain constants with the same name (e.g. FArray!val!3).
Previously, models were retrieved using get-model, which could cause issues when minimizing invariants for Lustre models with arrays encoded as values of an uninterpreted sort, FArray, with arity 2. If the Lustre model includes arrays for two different element types (e.g., FArray Int Bool and FArray Int Int), Z3 returns models where the universes for FArray Int Bool and FArray Int Int may contain constants with the same name (e.g. FArray!val!3).