# Caissa

[2006-10-16]

Coypright © 2006 Saarland Univerisity

## Introduction

Caissa implements the eager approach to decision procedures for the quantifier-free theories of equality with uninterpreted symbols, integer linear arithmetic, fixed-size bit-vectors, arrays, sets, multisets, and lists with a length function.

Caissa translates an input quantifier-free formula *F* into an output CNF propositional formula *G* such that *F* is satisfiable modulo the combination of the supported theories if and only if *G* is propositionally satisfiable.

## Usage

caissa in [out]Caissa reads the input formula from the file

## Download

You can download and use CAISSA under the terms of the following LICENSE.

## Contact

Questions and bug reports can be emailed to zarba at cs dot uni-sb dot de.