私はZ3 Pythonインターフェイスを使用して実験用の式を作成しています。私はその数式をZ3ソルバに送ります。私が正しいとすれば、Z3はそれ自身のソルバーを使います！Z3で異なるバックエンドソルバを使用する
Z3pyで別のSAT/SMTソルバーを使用するにはどうすればよいですか？
CBMC（C限定モデルチェッカー）で行う方法：プログラムを実行し、中間のDIMAC表現をファイルに吐出し、そのファイルを他のSATソルバーへの入力として使用します。 Z3で同様のことをすることはできますか？ありがとうございました。
すべてのSMTソルバはSMT2入力形式をサポートしているので、Z3や他のSMTソルバでも同じことができます。 Z3pyは、SolverオブジェクトとGoalオブジェクトをSMT2準拠の文字列に変換することができます（いくつかの複雑な変数宣言、たとえば、いくつかのデータ型が欠落している可能性があります）。
Z3pyは、Z3固有のAPI（名前が示すとおり）で、他のSMTソルバーを使用する方法を提供しません。
実際にZ3pyの代わりにソルバーにとらわれないSMTインターフェイスを使用する必要があります。複数のソルバのサポートの様々な程度で、そのようなインターフェイスを作成するためにいくつかの試みがなされてきた：
https://github.com/pysmt/pysmtは、SMTソルバのソルバ依存しないPythonのAPIです。私は自分で使ったことはありませんが、特にPythonをトップレベルのAPIとして使用したい場合は、有望です。
https://github.com/sosy-lab/java-smtは、Javaをホスト言語として使用する同様のプロジェクトです。
は、SMTソルバー（これはHaskellで書かれています）を使用するためのソルバー・アグノスティックAPIを提供する私自身の試みです。
決してこれは網羅的なリストではありません。さまざまなホスト言語で、成熟度の異なる他のものもあると確信しています。あなたが実際に選ぶべきものは、あなたのホスト言語の好みと、各システムによって提供される機能に依存します。それは広く変化し得る。