Z3中神祕的「無法嵌套的數據類型表達式」

Question

我將assert更改爲assert-soft，現在出現「無法嵌套的數據類型表達式」錯誤。這是什麼意思？

Answer 1

這是代碼中的拼寫錯誤。優化模式認爲它可以將數據類型表達式轉換爲枚舉類型，但會遇到它不知道要處理的表達式。該代碼需要被修復以檢查這種情況。 一個小的repro會很有用。我可以修復異常信息中的錯字，但不會解決錯誤。如果您可以在https://github.com/z3prover上提出問題，我們將不勝感激。