Boolector Python API documentation¶

Interface¶

Python interface

Quickstart¶

First, we create a Boolector instance:
        btor = Boolector()
We can configure this instance via Set_opt(). For example, if we want to enable model generation:
        btor.Set_opt(pyboolector.BTOR_OPT_MODEL_GEN, True)
For a detailed description of all configurable options, see Set_opt().

Next, we can create expressions and assert formulas via Assert().

Note

Boolector’s internal design is motivated by hardware design. Hence we do not distinguish between type Boolean and type bit-vector of length 1.

If incremental usage is enabled, formulas can optionally be assumed via Assume().

Note

Assumptions are invalidated after a call to Sat().

Alternatively, we can parse an input file prior to creating and asserting expressions. For example, to parse an input file example.btor, we can use Parse() (auto detects the input format).
(result, status, error_msg) = btor.Parse("example.btor")
In case the input issues a call to check sat (in case of SMT-LIB v2 or incremental SMT-LIB v1), this function either returns SAT, UNSAT, or UNKNOWN. In any other non-error case it returns UNKNOWN. For a more detailed description of the parsers return values, see Parse().

If the parser encounters an error, it returns PARSE_ERROR() and an explanation of that error is stored in error_msg. If the input file specifies a (known) status of the input formula (either satisfiable or unsatisfiable), that status is stored in status.

As an example for generating and asserting expressions via Assert(), consider the following example:
0 < x <= 100 && 0 < y <= 100 && x * y < 100
Assume that this example is given with x and y as natural numbers. We encode it with bit-vectors of size 8, and to preserve semantics, we have to ensure that the multiplication does not overflow.

We first create a bit-vector sort of size 8.
        bvsort8 = btor.BitVecSort(8)
Then, we create and assert the following expressions:
        x = btor.Var(bvsort8, "x")
        y = btor.Var(bvsort8, "y")
        zero = btor.Const(0, 8)
        hundred = btor.Const(100, 8)
        # 0 < x
        ult_x = btor.Ult(zero, x)
        btor.Assert(ult_x)
        # x <= 100
        ulte_x = btor.Ulte(x, hundred)
        btor.Assert(ulte_x)
        # 0 < y
        ult_y = btor.Ult(zero, y)
        btor.Assert(ult_y)
        # y <= 100
        ulte_y = btor.Ulte(y, hundred)
        btor.Assert(ulte_y)
        # x * y
        mul = btor.Mul(x, y)
        # x * y < 100
        ult = btor.Ult(mul, hundred)
        btor.Assert(ult)
        umulo = btor.Umulo(x, y)
        numulo = btor.Not(umulo)  # prevent overflow
        btor.Assert(numulo)
The satisfiability of the resulting formula can be determined via Sat(),
        res = btor.Sat()
If the resulting formula is satisfiable and model generation has been enabled via Set_opt(), we can either print the resulting model via Print_model(), or query assignments of bit-vector and array variables or uninterpreted functions via assignment().

Note

Querying assignments is not limited to variables. You can query the assignment of any arbitrary expression.

The example above is satisfiable, and we can now either query the assignments of variables x and y or print the resulting model via boolector_print_model().
        # prints "x: 00000100"
        print("assignment of {}: {}".format(x.symbol, x.assignment))
        # prints: "y: 00010101"
        print("assignment of {}: {}".format(y.symbol, y.assignment))
Boolector supports printing models in its own format (“btor”) or in SMT-LIB v2 format (“smt2”). We print the resulting model in BTOR format:
        btor.Print_model("btor")
A possible model is shown below and gives the assignments of bit-vector variables x and y. The first column indicates the id of the input, the second column its assignment, and the third column its name (or symbol) if any.
2 00000001 x
3 01011111 y
In the case that the formula includes arrays as inputs, their values at a certain index are indicated as follows:
4[00] 01 A
Here, array A has id 4 with index and element bit width of 2, and its value at index 0 is 1.

We now print the model of the example above in SMT-LIB v2 format.
        btor.Print_model("smt2")
A possible model is shown below:
(
  (define-fun x () (_ BitVec 8) #b00000001)
  (define-fun y () (_ BitVec 8) #b01011111)
)
Note

Boolector internally represents arrays as uninterpreted functions and prints array models as models for UF.

The source code of the example above can be found at examples/api/python/quickstart.py.

Python Operator Overloading¶

The Boolector Python API provides the following overloaded operators on bit-vectors (BoolectorBVNode).

Arithmetic Operators: + - * / %

x = btor.Var(32)
y = btor.Var(32)

bvadd  = x + y  # btor.Add(x, y)
bvsub  = x - y  # btor.Sub(x, y)
bvmul  = x * y  # btor.Mul(x, y)
bvudiv = x / y  # btor.Udiv(x, y)
bvurem = x % y  # btor.Urem(x, y)
bvneg  = -x     # btor.Neg(x)

Bitwise Operators: ~ & | ^ << >>

z = btor.Var(5)

bvnot = ~x      # btor.Not(x)
bvand = x & y   # btor.And(x, y)
bvor  = x | y   # btor.Or(x, y)
bvxor = x ^ y   # btor.Xor(x, y)
bvshl = x << z  # btor.Sll(x, z)
bvshr = x >> z  # btor.Srl(x, z)

Comparison Operators: < <= == != >= >

lt   = x < y   # btor.Ult(x, y)
lte  = x <= y  # btor.Ulte(x, y)
eq   = x == y  # btor.Eq(x, y)
ne   = x != y  # btor.Ne(x, y)
ugte = x >= y  # btor.Ugte(x, y)
ugt  = x > y   # btor.Ugt(x, y)

Python Slices: It is possible to use Python slices on bit-vectors (see Slice()), e.g.:

slice_5_2  = x[5:2]  # btor.Slice(x, 5, 2)
slice_5_0  = x[5:]   # btor.Slice(x, 5, 0)
slice_31_5 = x[:5]   # btor.Slice(x, x.width - 1, 5)
slice_31_0 = x[:]    # btor.Slice(x, x.width - 1, 0) -- copies variable 'x'

Further, the API also provides convenient ways to create reads (see Read()) on arrays, and function applications (see Apply()).

Reads on Arrays:

a = btor.Array(8, 32)

read = a[x]  # btor.Read(a, x)

Function Applications:

bv8 = btor.BitVecSort(8)
bv32 = btor.BitVecSort(32)
f = btor.UF(btor.FunSort([bv32, bv32], bv8))

app = f(x, y)  # btor.Apply([x, y], f)

Automatic Constant Conversion¶

For almost every method of Boolector that creates nodes, instead of passing arguments of the type BoolectorNode, the Python API allows to pass constants as arguments. The only requirement is that it must be possible to derive the bit width of the constant operands from the remaining operands. For example, for binary operators like Add(), an operandsmay be a constant, and its bit-width will be derived from the other non-constant operand, e.g.:
btor.Add(x, 42)         # btor.Add(x, btor.Const(42, x.width))
btor.And(0x2a, x)       # btor.And(btor.Const(0x2a, x.width), x)
btor.Udiv(0b101010, x)  # btor.Udiv(btor.Const(0b101010, x.width), x)
For all shift operations it is possible to define the shift width as constant, e.g.:
btor.Sll(x, 5)  # btor.Sll(x, btor.Const(5, math.ceil(math.log(x.width, 2))))
btor.Ror(x, 5)  # btor.Ror(x, btor.Const(5, math.ceil(math.log(x.width, 2))))
For operations on arrays all arguments may be constant (except the array itself) since the bit width of the operands can be derived from the array, e.g.:
btor.Read(a, 42)       # btor.Read(a, btor.Const(42, a.index_with))
btor.Write(a, 42, 10)  # btor.Write(a, btor.Const(42, a.index_width), btor.Const(10, a.width))
This also applies to the arguments of function applications, which can be derived from the function’s signature, e.g.:
btor.Apply([42, 10], f)  # btor.Apply([btor.Const(42, ...), btor.Const(10, ...)], f)
Note

Automatic constant conversion is not possible for the following operators: Not(), Neg(), Redor(), Redxor(), Redand(), Slice(), Uext(), Sext(), Inc(), Dec(), and Concat(), as the bit with of the resulting node cannot be determined.

Options¶

Boolector can be configured either via Set_opt(), or via environment variables of the form:
BTOR<capitalized option name without '_'>=<value>
For a list and detailed descriptions of all available options, see Set_opt().

For example, given a Boolector instance btor, model generation is enabled either via
btor.Set_opt(BTOR_OPT_MODEL_GEN, 1)
or via setting the environment variable
BTORMODELGEN=1

API Tracing¶

API tracing allows to record every call to Boolector’s public API. The resulting trace can be replayed and the replayed sequence behaves exactly like the original Boolector run. This is particularly useful for debugging purposes, as it enables replaying erroneous behaviour. API tracing can be enabled via setting the environment variable BTORAPITRACE=<filename>.

For example, given a Boolector instance ‘btor’, API tracing is enabled as follows:
BTORAPITRACE="error.trace"

Internals¶

Boolector internally maintains a directed acyclic graph (DAG) of expressions. By asserting an expression, it will be permanently added to the formula. Assumptions, in contrast, are cleared after a call to Sat(). You can query assumptions that force a formula to be unsatisfiable via Failed().

Operators¶

Boolector internally describes expressions by means of a set of base operators. Boolector’s API, however, provides a richer set of operators for convenience, where non-base operators are internally rewritten to use base operators only. For example, two’s complement (Neg()) is expressed by means of one’s complement.

Note

This behaviour is not influenced by the configured rewrite level.

Rewriting and Preprocessing¶

Boolector simplifies expressions and the expression DAG by means of rewriting. It supports three so-called rewrite levels. Increasing rewrite levels increase the extent of rewriting and preprocessing performed. Rewrite level of 0 is equivalent to disabling rewriting and preprocessing at all.

Note

Rewriting expressions by means of base operators can not be disabled, not even at rewrite level 0.

Boolector not only simplifies expressions during construction of the expression DAG but also performs preprocessing on the DAG. For each call to Sat(), various simplification techniques and preprocessing phases are initiated. You can force Boolector to initiate simplifying the expression DAG via Simplify(). The rewrite level can be configured via Set_opt().

Examples¶

Quickstart Example¶

import os
import pyboolector
from pyboolector import Boolector, BoolectorException

if __name__ == "__main__":
    try:
        # Create Boolector instance
        btor = Boolector()
        # Enable model generation
        btor.Set_opt(pyboolector.BTOR_OPT_MODEL_GEN, True)
        # Create bit-vector sort of size 8
        bvsort8 = btor.BitVecSort(8)
        # Create expressions
        x = btor.Var(bvsort8, "x")
        y = btor.Var(bvsort8, "y")
        zero = btor.Const(0, 8)
        hundred = btor.Const(100, 8)
        # 0 < x
        ult_x = btor.Ult(zero, x)
        btor.Assert(ult_x)
        # x <= 100
        ulte_x = btor.Ulte(x, hundred)
        btor.Assert(ulte_x)
        # 0 < y
        ult_y = btor.Ult(zero, y)
        btor.Assert(ult_y)
        # y <= 100
        ulte_y = btor.Ulte(y, hundred)
        btor.Assert(ulte_y)
        # x * y
        mul = btor.Mul(x, y)
        # x * y < 100
        ult = btor.Ult(mul, hundred)
        btor.Assert(ult)
        umulo = btor.Umulo(x, y)
        numulo = btor.Not(umulo)  # prevent overflow
        btor.Assert(numulo)

        res = btor.Sat()
        print("Expect: sat")
        print("Boolector: ", end='')
        if res == btor.SAT:
            print("sat")
        elif res == btor.UNSAT:
            print("unsat")
        else:
            print("unknown")
        print("")

        # prints "x: 00000100"
        print("assignment of {}: {}".format(x.symbol, x.assignment))
        # prints: "y: 00010101"
        print("assignment of {}: {}".format(y.symbol, y.assignment))
        print("")

        print("Print model in BTOR format:")
        btor.Print_model("btor")
        print("")
        print("Print model in SMT-LIBv2 format:")
        btor.Print_model("smt2")
        print("")
    except BoolectorException as e:
        print("Caught exception: " + str(e))

More Comprehensive API Usage Example¶

import os
import pyboolector
from pyboolector import Boolector, BoolectorException

if __name__ == "__main__":
    b = Boolector()
    print ("Boolector version " + b.Version())
    print ("Boolector id " + b.GitId())
    print ()
    print (b.Copyright())

    # Try pushing a context without enabling incremental usage,
    # raises Exception
    try:
        print("Expect exception to be raised (incremental usage not enabled).")
        b.Push()
    except BoolectorException as e:
        print("Caught exception: " + str(e))

    # Try popping a context without first having pushed a context,
    # raises Exception
    try:
        b.Set_opt(pyboolector.BTOR_OPT_INCREMENTAL, True)
        print("Expect exception to be raised (no context pushed).")
        b.Pop()
    except BoolectorException as e:
        print("Caught exception: " + str(e))

### Creating Boolector nodes

    # Sorts
    _boolsort = b.BoolSort()
    # Try creating a bit-vector sort of size 0,
    # raises Exception
    try:
        print("Expect exception to be raised (bit-vector size of 0).")
        _bvsort = b.BitVecSort(0)
    except BoolectorException as e:
        print("Caught exception: " + str(e))
    _bvsort   = b.BitVecSort(128)
    _arrsort  = b.ArraySort(_bvsort, _bvsort)
    _funsort  = b.FunSort([_boolsort, _boolsort, _bvsort, _bvsort], _boolsort)

    # Constants
    _const = b.Const("10010101")
    _zero  = b.Const(0, 128)
    _ones  = b.Const(-1, 129)
    _true  = b.Const(True)
    _false = b.Const(False)
    _one   = b.Const(1, 128)
    _uint  = b.Const(77, 128)
    _int   = b.Const(-77, 128)

    # Variables
    _var   = b.Var(_bvsort, "var_symbol")
    # Try getting the assignment of _var without a call to Sat(),
    # raises Exception
    try:
        print("Expect exception to be raised (no previous call to Sat()).")
        print("{} {}".format(_var.symbol, _var.assignment))
    except BoolectorException as e:
        print("Caught exception: " + str(e))

    _param = b.Param(_bvsort, "param_symbol")  # used as function parameters
    _array = b.Array(_arrsort, "array_symbol")
    _uf    = b.UF(_funsort)

    # One's complement 
    _not0    = b.Not(_const)
    _not1    = ~_const

    # Two's complement
    _neg0    = b.Neg(_zero)
    _neg1    = -_zero

    # Reduction operations on bit vectors
    _redor   = b.Redor(_ones)
    _redxor  = b.Redxor(_one)
    _redand  = b.Redand(_uint)

    # Slicing of bit vectors
    _slice0  = b.Slice(_param, 8, 0)
    _slice1  = _param[8:0]
    _slice3  = _param[:]   # copy
    _slice2  = _param[8:]  # lower is 0
    _slice4  = _param[:0]  # upper is _param.width - 1
    _slice5  = _param[8]   # extract bit at position 8, equiv. to _param[8:8]
    _slice5  = _param[8:8] # equiv. to _param[8]

    # Unsigned/signed extension
    _uext    = b.Uext(_true, 127)
    _sext    = b.Sext(_false, 127)

    _inc     = b.Inc(_not0)
    _dec     = b.Dec(_not1)
   
    _implies0 = b.Implies(_redor, _redxor)
    _implies1 = b.Implies(False, _redor)
    _implies2 = b.Implies(True, _redxor)

    _iff0     = b.Iff(True, _redxor)
    _iff1     = b.Iff(_redor, _redxor)
    _iff2     = b.Iff(False, _redxor)

    _xor0     = b.Xor(_uext, _sext)
    _xor1     = _uext ^ _sext
    _xor2     = b.Xor(0xff, _sext)
    _xor3     = 0xff ^ _sext

    _and0     = b.And(_inc, _dec)
    _and1     = b.And(128, _dec)
    _and2     = b.And(_dec, 0xaa)
    _and3     = _dec & 0xaa

    _nand0    = b.Nand(_inc, _dec)
    _nand1    = b.Nand(128, _dec)
    _nand2    = b.Nand(_dec, 0xaa)
    _nand3    = ~(_dec & 0xaa)

    _or0      = b.Or(_inc, _dec)
    _or1      = b.Or(128, _dec)
    _or2      = b.Or(_dec, 0xaa)
    _or3      = _dec | 0xaa

    _nor0     = b.Nor(_inc, _dec)
    _nor1     = b.Nor(128, _dec)
    _nor2     = b.Nor(_dec, 0xaa)
    _nor3     = ~(_dec | 0xaa)

    _eq0      = b.Eq(_inc, _dec)
    _eq1      = b.Eq(128, _dec)
    _eq2      = b.Eq(_dec, 0xaa)
    _eq3      = _dec == 0xaa

    _neq0     = b.Ne(_inc, _dec)
    _neq1     = b.Ne(128, _dec)
    _neq2     = b.Ne(_dec, 0xaa)
    _neq3     = _dec != 0xaa

    _add0     = b.Add(_inc, _dec)
    _add1     = b.Add(128, _dec)
    _add2     = b.Add(_dec, 0xaa)
    _add3     = _dec + 0xaa

    _uaddo0   = b.Uaddo(_inc, _dec)
    _uaddo1   = b.Uaddo(128, _dec)
    _uaddo2   = b.Uaddo(_dec, 0xaa)

    _saddo0   = b.Saddo(_inc, _dec)
    _saddo1   = b.Saddo(128, _dec)
    _saddo2   = b.Saddo(_dec, 0xaa)

    _mul0     = b.Mul(_inc, _dec)
    _mul1     = b.Mul(128, _dec)
    _mul2     = b.Mul(_dec, 0xaa)
    _mul3     = _dec * 0xaa

    _umulo0   = b.Umulo(_inc, _dec)
    _umulo1   = b.Umulo(128, _dec)
    _umulo2   = b.Umulo(_dec, 0xaa)

    _smulo0   = b.Smulo(_inc, _dec)
    _smulo1   = b.Smulo(128, _dec)
    _smulo2   = b.Smulo(_dec, 0xaa)

    _ult0     = b.Ult(_inc, _dec)
    _ult1     = b.Ult(128, _dec)
    _ult2     = b.Ult(_dec, 0xaa)
    _ult3     = _dec < 0xaa

    _slt0     = b.Slt(_inc, _dec)
    _slt1     = b.Slt(128, _dec)
    _slt2     = b.Slt(_dec, 0xaa)

    _ulte0    = b.Ulte(_inc, _dec)
    _ulte1    = b.Ulte(128, _dec)
    _ulte2    = b.Ulte(_dec, 0xaa)
    _ulte3    = _dec <= 0xaa

    _slte0    = b.Slte(_inc, _dec)
    _slte1    = b.Slte(128, _dec)
    _slte2    = b.Slte(_dec, 0xaa)

    _ugt0     = b.Ugt(_inc, _dec)
    _ugt1     = b.Ugt(128, _dec)
    _ugt2     = b.Ugt(_dec, 0xaa)
    _ugt3     = _dec > 0xaa

    _sgt0     = b.Sgt(_inc, _dec)
    _sgt1     = b.Sgt(128, _dec)
    _sgt2     = b.Sgt(_dec, 0xaa)

    _ugte0    = b.Ugte(_inc, _dec)
    _ugte1    = b.Ugte(128, _dec)
    _ugte2    = b.Ugte(_dec, 0xaa)
    _ugte3    = _dec >= 0xaa

    _sgte0    = b.Sgte(_inc, _dec)
    _sgte1    = b.Sgte(128, _dec)
    _sgte2    = b.Sgte(_dec, 0xaa)

    _sll0     = b.Sll(_dec, 5)
    _sll1     = b.Sll(_dec, 0b100)
    _sll2     = _dec << 5

    _srl0     = b.Srl(_dec, 5)
    _srl1     = b.Srl(_dec, 0b100)
    _srl2     = _dec >> 5

    _sra0     = b.Sra(_dec, 5)
    _sra1     = b.Sra(_dec, 0b100)

    _rol0     = b.Rol(_dec, 5)
    _rol1     = b.Rol(_dec, 0b100)

    _ror0     = b.Ror(_dec, 5)
    _ror1     = b.Ror(_dec, 0b100)

    _sub0     = b.Sub(_inc, _dec)
    _sub1     = b.Sub(128, _dec)
    _sub2     = b.Sub(_dec, 0xaa)
    _sub3     = _dec - 0xaa

    _ssubo0   = b.Ssubo(_inc, _dec)
    _ssubo1   = b.Ssubo(128, _dec)
    _ssubo2   = b.Ssubo(_dec, 0xaa)

    _udiv0    = b.Udiv(_inc, _dec)
    _udiv1    = b.Udiv(128, _dec)
    _udiv2    = b.Udiv(_dec, 0xaa)
    _udiv3    = _dec / 0xaa

    _urem0    = b.Urem(_inc, _dec)
    _urem1    = b.Urem(128, _dec)
    _urem2    = b.Urem(_dec, 0xaa)
    _urem3    = _dec % 0xaa

    _sdiv0    = b.Sdiv(-_inc, _dec)
    _sdiv1    = b.Sdiv(128, -_dec)
    _sdiv2    = b.Sdiv(_dec, -0xaa)

    _srem0    = b.Srem(-_inc, _dec)
    _srem1    = b.Srem(128, -_dec)
    _srem2    = b.Srem(_dec, -0xaa)

    _sdivo0   = b.Sdivo(-_inc, _dec)
    _sdivo1   = b.Sdivo(128, -_dec)
    _sdivo2   = b.Sdivo(_dec, -0xaa)

    _smod0    = b.Smod(-_inc, _dec)
    _smod1    = b.Smod(128, -_dec)
    _smod2    = b.Smod(_dec, -0xaa)

    # Concatenation of bit vectors
    _concat   = b.Concat(_dec, _inc)
    _repeat   = b.Repeat(_concat, 1)
    _repeat   = b.Repeat(_repeat, 5)


    # Reads on arrays
    _read0    = b.Read(_array, _var)
    _read1    = b.Read(_array, 12)
    _read2    = _array[_var]
    _read3    = _array[0x1a]

    # Writes on arrays
    _write0   = b.Write(_array, _var, _var)
    _write1   = b.Write(_array, 10, 0b00001)

    # If-Then-Else on bit vectors
    _cond0    = b.Cond(_read0[0], _read0, _read1)
    _cond1    = b.Cond(False, _read0, _read1)
    _cond2    = b.Cond(True, 1, _read1)

    # If-Then-Else on arrays
    _cond3    = b.Cond(0, _write0, _write1)

    # Function
    p0        = b.Param(_bvsort)
    p1        = b.Param(_bvsort)
    _fun      = b.Fun([p0, p1], b.Cond(p0 < p1, p0, p1))

    # Function applications
    _apply0   = b.Apply([_var, _var], _fun)
    _apply1   = b.Apply([1, 2], _fun)
    _apply2   = _fun(1, 2)
    _apply3   = b.Apply([_true, _false, _var, _var], _uf)
    _apply4   = b.Apply([1, True, 3, 42], _uf)
    _apply5   = b.Apply([1, False, 3, 42], _uf)
    _apply6   = _uf(1, False, 3, 42)

### Node attributes and methods

    # Get symbol
    s = _var.symbol
    s = _apply4.symbol

    # Set symbol
    _var.symbol = "new_symbol"

    # Get bit width
    w = _apply4.width
    w = _fun.width

    # Get bit width of array index
    w = _array.index_width

    # Get arity of functions
    a = _fun.arity
    a = _uf.arity

    # Get bit vector representation of constants as string
    bits = _const.bits

    # Dump nodes to stdout or files (default format is BTOR)
    _apply4.Dump()
    # Dump to file 'dump.btor'
    _apply4.Dump(outfile="dump.btor")
    _apply4.Dump("smt2")
    # Dump to file 'dump.smt2'
#    _apply4.Dump("smt2", "dump.smt2")

### Boolector methods

    # Available options
    b.Options()
    # Print available options
    print("Available Boolector options:")
    print("\n".join(["  " + str(o) for o in b.Options()]))

    # Set options
    b.Set_opt(pyboolector.BTOR_OPT_INCREMENTAL, 1)
    b.Set_opt(pyboolector.BTOR_OPT_MODEL_GEN, 1)

    # Get options
    o = b.Get_opt(pyboolector.BTOR_OPT_MODEL_GEN)
#    print(o.lng)  # long option name
#    print(o.shrt) # short option name
#    print(o.desc) # description
#    print(o.min)  # min value
#    print(o.max)  # max value
#    print(o.dflt) # default value
#    print(o.val)  # current value

    # Set SAT solver (can only be done before the first Sat() call)
    # Lingeling is the default SAT solver
    #b.Set_sat_solver("MiniSAT")

    # Assert formulas
    b.Assert(_cond0[1])
    b.Assert(_apply5 != _apply3)

    # Assume formulas
    b.Assume(_cond1[1])

    # Run simplification separately
    res = b.Simplify()

    # Clone boolector instance 'b'
    bb = b.Clone()

    # Check sat
    res = b.Sat()
    # Check sat with limits
#    res = b.Sat(100, 10000)
#    res = b.Sat(lod_limit=100, sat_limit=10000)
    if res == b.SAT: print("result: SAT")
    else           : print("result: UNSAT")

    # Get model or query assignments for nodes
    if res == b.SAT:
        print("Model:")
        # Get model and print to stdout
        b.Print_model()
        # Get model and print to file 'model.out'
#        b.Print_model("model.out")

         # Query assignments
#        print("Query assignments:")
#        print("{} {}".format(_var.symbol, _var.assignment))
#        print("{} {}".format(_array.symbol, _array.assignment))
#        print("{} {}".format(_uf.symbol, _uf.assignment))

    # Get matching node of _cond0 in clone 'bb'
    _cond0_matched = bb.Match(_cond0)
    # Assume
    bb.Assume(~_cond0_matched[1])
    bb.Assume(_cond0_matched[2])
    # Check sat
    res = bb.Sat()
    if res == bb.SAT: print("result: SAT")
    else            : print("result: UNSAT")

    if res == b.UNSAT:
        # Check if assumptions are failed
        bb.Failed(~_cond0_matched[1])
        bb.Failed(_cond0_matched[2])

    os.remove("dump.btor")

### Quantifiers
    bbb = Boolector()
    bbb.Set_opt(pyboolector.BTOR_OPT_MODEL_GEN, 1)
    _bvsort   = bbb.BitVecSort(128)
    x        = bbb.Param(_bvsort)
    y        = bbb.Param(_bvsort)
    z        = bbb.Param(_bvsort)
    _exists   = bbb.Exists([x], x > z)
    _forall   = bbb.Forall([y, z], _exists)
    bbb.Assert(_forall)
    res       = bbb.Sat()
    if res == bbb.SAT: print("result: SAT")
    else             : print("result: UNSAT")

### Option interaction
    bbbb = Boolector()
    desired_output_format = pyboolector.BTOR_OUTPUT_FORMAT_AIGER_ASCII
    bbbb.Set_opt(
        pyboolector.BTOR_OPT_OUTPUT_FORMAT, desired_output_format
    )
    assert (
        bbbb.Get_opt(pyboolector.BTOR_OPT_OUTPUT_FORMAT).val
        == desired_output_format
    )
    assert (
        bbbb.Get_opt(pyboolector.BTOR_OPT_OUTPUT_FORMAT).val
        != pyboolector.BTOR_OUTPUT_FORMAT_SMT2
    )