次のコードでは、と宣言されるまで、Z3は1行目のnilを認識しません。これを解決するには？ Z3/SMT-LIB2にimport/includeのような構造がありますか？Z3がタイプなしの挿入文字とNilを認識しない
(assert (= nil nil)) ; (error "line 1 column 12: unknown constant nil")
(declare-const xs (List Int))
(assert (= nil nil)) ; OK after declare-const List Int
z3 -inをファイルからテストすると、エラーが表示されます。
これは残念なことに、SMT-Lib標準の一般的な欠点です。スコープを有効にする唯一の方法は、set-logicの宣言によるものであり、それらの論理のリストは固定されています。個々のソルバ（z3など）が新しい決定手順を実装するとき、シンボルを臨時に持ち込む必要があります。それは、宣言にListがあると、z3はシンボルnilをスコープに持ち込むだけです。エラーが発生しやすいとは言えません。
これは議論の中で何度も出てきました。欲しいものはありません。たとえば、http://www.cs.nyu.edu/pipermail/smt-lib/2015/000862.htmlを参照してください。ここでは、固定ロジック宣言からより多くのimportスタイル指定に移行するよう提案されています。
だから、現状を考えれば、最初はListと思われます。うまくいけば、SMTLibは将来、より柔軟な方法で新機能をサポートする方法に進化します。