The z3 package

[ Tags: bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers ] [ Propose Tags ]

Bindings for the Z3 Theorem Prover.

This package is still a work in progress. Low and medium-level bindings to the Z3 API are provided (Z3.Base.C and Z3.Base) in the spirit of yices-painless. These APIs are still incomplete but usable. The high-level API (Z3.Lang) is still very experimental and likely to change.

Installation (Unix-like): Just be sure to use the standard locations for dynamic libraries (/usr/lib) and header files (/usr/include), or else use the appropriate Cabal flags.

Haddock documentation:

More information about Z3:


Versions 0.1.1, 0.2.0, 0.3.0, 0.3.1, 0.3.2, 4.0.0, 4.1.0, 4.1.1, 4.1.2, 4.2.0
Dependencies base (>3 && <5), containers, mtl [details]
License BSD3
Copyright 2012, Iago Abal, David Castro
Author Iago Abal <>, David Castro <>
Maintainer Iago Abal <>, David Castro <>
Category Math, Theorem Provers, Formal Methods
Home page
Source repo head: hg clone
Uploaded Tue Dec 18 11:14:48 UTC 2012 by IagoAbal
Distributions NixOS:4.1.2
Downloads 3110 total (99 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-23 [all 8 reports]
Hackage Matrix CI


  • Z3
    • Z3.Base
      • Z3.Base.C
    • Z3.Lang
      • Z3.Lang.Lg2
      • Z3.Lang.Nat
      • Z3.Lang.Pow2
      • Z3.Lang.Prelude


Maintainer's Corner

For package maintainers and hackage trustees