z3rs
====
z3rs is a pure-Rust, zero-external-dependency port of the Z3 theorem prover.
It is a derivative work of Z3:
Z3
Copyright (c) Microsoft Corporation
Licensed under the MIT License.
Source: https://github.com/Z3Prover/z3
Ported from Z3 version 4.17.0.
Substantial portions of z3rs are translations of Z3's C++ source into Rust.
Algorithms, data-structure designs, module layout, heuristics, and comments
derive directly from the upstream Z3 project and remain under the MIT License
(see LICENSE).
The Rust translation, adaptations, and any new code are provided under the
same MIT License.
This project is not affiliated with or endorsed by Microsoft Corporation.
"Z3" is a project of Microsoft Research; this port merely tracks its behaviour.
Upstream attribution convention
-------------------------------
Every ported Rust module carries a header comment pointing at the specific
upstream file(s) it derives from, e.g.:
//! Ported from `z3/src/util/mpz.{h,cpp}` (Z3 4.17.0, MIT).