Skip to content

Latest commit

 

History

History
19 lines (14 loc) · 360 Bytes

why3.md

File metadata and controls

19 lines (14 loc) · 360 Bytes

The Why3 backend (experimental)

# Install dependencies, which includes the Why3 IDE
opam install . --deps-only

# Install some provers (optional)
which z3 # already installed
opam install alt-ergo
brew install cvc4

# Configure why3
why3 config detect

# Run examples and tests
PROVER=WHY3 dune exec parsing/hip.exe $EXAMPLE
PROVER=WHY3 dune test