copilot-theorem-4.0: k-induction for Copilot.
Safe HaskellTrustworthy
LanguageHaskell2010

Copilot.Theorem.Kind2.Prover

Description

A prover backend based on Kind2.

Synopsis

Documentation

module Data.Default

data Options Source #

Options for Kind2

Constructors

Options 

Fields

  • bmcMax :: Int

    Upper bound on the number of unrolling that base and step will perform. A value of 0 means unlimited.

Instances

Instances details
Default Options Source #

Default options with unlimited unrolling for base and step.

Instance details

Defined in Copilot.Theorem.Kind2.Prover

Methods

def :: Options #

kind2Prover :: Options -> Prover Source #

A prover backend based on Kind2.

The executable kind2 must exist and its location be in the PATH.