Modules

This module exposes options which can be set on a Btor instance.

Structs

An Array in Boolector is really just a map from BVs to BVs.

A bitvector object: that is, a single symbolic value, consisting of some number of symbolic bits.

A BVSolution represents a possible solution for one BV in a given model.

A Btor represents an instance of the Boolector solver. Each BV and Array is created in a particular Btor instance.

Enums