package alt-ergo-lib

  1. Overview
  2. Docs
The Alt-Ergo SMT prover library

Install 

dune-project
 Dependency

alt-ergo.ocamlpro.com Readme Changelog LicenseRef-OCamlpro-Non-Commercial; Apache-2.0 License Edit opam file Versions (17)

Authors

  1. A
    Alt-Ergo developers <alt-ergo@ocamlpro.com>

Maintainers

  1. A
    Alt-Ergo developers <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.6.4.tbz
sha256=c35b5b49ec2816a24c9325b083eefe237839ebaceb83331aeef041bed720b137
sha512=ed1486c0a86eb4cc66fc7b77f0d25f64949d7d134a456a78f6cdd19aa455b0808ba430cb6621fa89e89e09f5b48b1ad07fe4d5e29d0088d7804e09b4a2f712ac

doc/LICENSE.html

These software are distributed in the hope that they will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

Please, do not use enclosed software until you have read and accepted the terms of the licensing below. The use of these software implies that you automatically agree with our terms and conditions. In case of doubt, please contact us to clarify licensing.

The resources are licensed as follows:

OCaml source files and Alt-Ergo preludes

All the files of this project, with the exception of the preludes and plugins, are distributed under the terms of OCamlPro-Non-Commercial-License.

As an exception, Alt-Ergo Club members at the Gold level can use these same files under the terms of Apache Software License version 2.0.

Note that plugins or preludes may have different licenses. Please referer to their directory.

In case of doubt, please refer to the header of each file to know under which license it is distributed.

Releases

We publish our releases on GitHub and opam repository under the license OCamlPro-Non-Commercial-License. The same exceptions as above apply to the plugins and preludes.

We also publish a free release of Alt-Ergo under the terms of CeCILL-C License v1. The packages of the free releases are suffixed with -free on the opam repository.

Plugins

Please refer to the LICENSE.md of each plugins:

  • AB-Why3: src/plugins/AB-Why3/LICENSE.md
  • fm-simplex: src/plugins/fm-simplex/LICENSE.md