Z3

Z3 は、Microsoft Research の定理証明器です。 MIT ライセンスの下で提供されています。Windows バイナリ配布には C++ ランタイム再頒布可能パッケージが含まれています。

Z3 に詳しくない場合は、こちらから始めることができます。

安定版およびナイトリーリリースのプリビルドバイナリはこちらから入手できます。

Z3 は、[Visual Studio][1]、[Makefile][2]、[CMake][3]、[vcpkg][4]、または [Bazel][5] を使用してビルドできます。 また、[いくつかのプログラミング言語向けのバインディング][6]を提供しています。

各種安定版リリースに関する注意事項については、リリースノートを参照してください。

ビルドステータス

プルリクエスト & プッシュワークフロー

WASM ビルド	Windows ビルド	CI	OCaml バインディング

定期実行ワークフロー

Open Bugs	Android ビルド	Pyodide Wheel (PyPI)	ナイトリービルド	クロスビルド

MSVC スタティック	MSVC Clang-CL	Z3 キャッシュのビルド	メモリ安全性	PR のレビュー準備完了

手動 & リリースワークフロー

ドキュメント	リリースビルド	WASM リリース	NuGet ビルド

特化ワークフロー

ナイトリー検証	Copilot セットアップ	Agentics メンテナンス

エージェンティックワークフロー

API 一貫性	コード簡略化	リリースノート	ワークフロー提案	学術引用

課題バックログ	メモリ安全性レポート	QF-S ベンチマーク	Specbot クラッシュアナライザ	SMTLIB ベンチマークファインダー

TPTP ベンチマーク