Z3の不思議な「未使用のネストされたデータ型式」

Question

assertをassert-softに変更しましたが、「使用できないネストされたデータ型式」というエラーが発生しました。これは何を意味するのでしょうか？

Answer 1

これはコードの入力ミスです。最適化モードでは、データ型式を列挙型に変換できますが、処理することがわからない式があります。この状態をチェックするには、コードを修正する必要があります。 小規模の再編集が便利です。私は例外メッセージの誤字を修正することができますが、バグに対処しません。もしあなたがhttps://github.com/z3proverに問題を提出することができれば、それは評価されるでしょう。