---
name: "formulacheck"
section: "1"
platform: "linux"
package: "mcrl2"
version: "201202.0-2+b1"
release: "Debian 7 (Wheezy)"
platforms: ["linux"]
url: "https://new.carta.tech/formulacheck"
---

# formulacheck(1)

check a boolean formula

## NAME

formulacheck - check a boolean formula

## SYNOPSIS

**formulacheck** \[*OPTION*\]... \[*INFILE*\]

## DESCRIPTION

Checks whether the boolean formula (an mCRL2 data expression of sort Bool) in  INFILE holds. If INFILE is not present, stdin is used.

## OPTIONS

- *OPTION* can be any of the following:

  - **-c**, **--counter-example**

  display a valuation for which the formula does not hold, in case it is neither  a contradiction nor a tautology

- **-o**, **--induction**

  apply induction on lists

- **-p***PREFIX*, **--print-dot**=*PREFIX*

  save a .dot file of the resulting BDD if it is impossible to determine whether  the formula is a contradiction or a tautology; PREFIX will be used as prefix of  the output files

- **-r***NAME*, **--rewriter**=*NAME*

  use rewrite strategy NAME:\
     'jitty' for jitty rewriting (default),\
     'jittyc' for compiled jitty rewriting,\
     'jittyp' for jitty rewriting with prover

- **-z***SOLVER*, **--smt-solver**=*SOLVER*

  use SOLVER to remove inconsistent paths from the internally used BDDs (by  default, no path elimination is applied):\
     'cvc' for the SMT solver CVC3

- **-s***SPECFILE*, **--spec**=*SPECFILE*

  check the formula against the data types from the LPS or PBES in SPECFILE

- **-t***LIMIT*, **--time-limit**=*LIMIT*

  spend at most LIMIT seconds on proving a single formula

- **--timings**\[=*FILE*\]

  append timing measurements to FILE. Measurements are written to standard error  if no FILE is provided

- **-w**, **--witness**

  display a valuation for which the formula holds, in case it is neither a  contradiction nor a tautology

- Standard options:

  - **-q**, **--quiet**

  do not display warning messages

- **-v**, **--verbose**

  display short intermediate messages

- **-d**, **--debug**

  display detailed intermediate messages

- **--log-level**=*LEVEL*

  display intermediate messages up to and including level

- **-h**, **--help**

  display help information

- **--version**

  display version information

## AUTHOR

Written by Luc Engelen.

## REPORTING BUGS

Report bugs at \<http://www.mcrl2.org/issuetracker\>.

## COPYRIGHT

Copyright © 2012 Technische Universiteit Eindhoven.\
 This is free software.  You may redistribute copies of it under the terms of the Boost Software License \<http://www.boost.org/LICENSE\_1\_0.txt\>. There is NO WARRANTY, to the extent permitted by law.

## SEE ALSO

See also the manual at \<http://www.mcrl2.org/mcrl2/wiki/index.php/User\_manual/formulacheck\>.