cbmc_solvers.cpp File Reference

Solvers for VCs Generated by Symbolic Execution of ANSI-C. More...

#include "cbmc_solvers.h"
#include <memory>
#include <iostream>
#include <fstream>
#include <util/unicode.h>
#include <solvers/sat/satcheck.h>
#include <solvers/refinement/bv_refinement.h>
#include <solvers/smt1/smt1_dec.h>
#include <solvers/smt2/smt2_dec.h>
#include <solvers/cvc/cvc_dec.h>
#include <solvers/prop/aig_prop.h>
#include <solvers/sat/dimacs_cnf.h>
#include "bv_cbmc.h"
#include "cbmc_dimacs.h"
#include "counterexample_beautification.h"
#include "version.h"

Include dependency graph for cbmc_solvers.cpp:

Go to the source code of this file.

Detailed Description

Solvers for VCs Generated by Symbolic Execution of ANSI-C.

Definition in file cbmc_solvers.cpp.