diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-09-14 19:09:03 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-14 21:09:03 -0500 |
commit | 1e1b51f5ad91bac3911a41b2ef5a852f89568aaa (patch) | |
tree | 0270661c3f1e566f4c470a26c247a4c6c9335d5c /src/theory/bv/bitblast | |
parent | 51be2e14c632d45e63a40659dea2177133251dfa (diff) |
Fix ABC build (#5061)
For some reason, our ABC build was including cnf_stream.h in an
extern "C" block instead of outside of it, which made the build fail
because the header indirectly includes cdqueue.h, which uses
templates. This change is older
(e9bfbb2)
but only started causing problems with our nightly builds recently.
Diffstat (limited to 'src/theory/bv/bitblast')
-rw-r--r-- | src/theory/bv/bitblast/aig_bitblaster.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index 331db9378..8f3c5d05a 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -14,12 +14,12 @@ ** AIG bitblaster. **/ -#include "cvc4_private.h" - #include "theory/bv/bitblast/aig_bitblaster.h" #include "base/check.h" +#include "cvc4_private.h" #include "options/bv_options.h" +#include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" @@ -28,7 +28,6 @@ extern "C" { #include "base/abc/abc.h" #include "base/main/main.h" -#include "prop/cnf_stream.h" #include "sat/cnf/cnf.h" extern Aig_Man_t* Abc_NtkToDar(Abc_Ntk_t* pNtk, int fExors, int fRegisters); |