12#ifndef CPROVER_SOLVERS_FLATTENING_BV_DIMACS_H
13#define CPROVER_SOLVERS_FLATTENING_BV_DIMACS_H
message_handlert & message_handler
bv_dimacst(const namespacet &_ns, dimacs_cnft &_prop, message_handlert &message_handler, std::ostream &_out)
const dimacs_cnft & dimacs_cnf_prop
bv_pointerst(const namespacet &, propt &, message_handlert &, bool get_array_constraints=false)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...