Z3

Z3는 Microsoft Research의 정리 증명기입니다. MIT 라이선스에 따라 사용이 허가됩니다. Windows 바이너리 배포판에는 C++ 런타임 재배포 가능 패키지가 포함되어 있습니다.

Z3에 익숙하지 않다면 여기에서 시작할 수 있습니다.

안정 및 야간 릴리스의 미리 빌드된 바이너리는 여기에서 사용할 수 있습니다.

Z3는 [Visual Studio][1], [Makefile][2], [CMake][3], [vcpkg][4] 또는 [Bazel][5]을 사용하여 빌드할 수 있습니다. [여러 프로그래밍 언어에 대한 바인딩][6]을 제공합니다.

Z3의 다양한 안정 릴리스에 대한 참고 사항은 릴리스 노트를 참조하세요.

빌드 상태

Pull Request 및 Push 워크플로우

WASM 빌드	Windows 빌드	CI	OCaml 바인딩

예약된 워크플로우

오픈 버그	Android 빌드	Pyodide 휠 (PyPI)	야간 빌드	크로스 빌드

MSVC 정적	MSVC Clang-CL	Z3 캐시 빌드	메모리 안전성	PR 준비 표시

수동 및 릴리스 워크플로우

문서	릴리스 빌드	WASM 릴리스	NuGet 빌드

특수 워크플로우

야간 검증	Copilot 설정	Agentics 유지 관리

에이전트 워크플로우

API 일관성	코드 단순화	릴리스 노트	워크플로우 제안	학술 인용

이슈 백로그	메모리 안전성 보고서	QF-S 벤치마크	Specbot 충돌 분석기	SMTLIB 벤치마크 파인더

TPTP 벤치마크