summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2020-09-14 19:09:03 -0700
committerGitHub <noreply@github.com>2020-09-14 21:09:03 -0500
commit1e1b51f5ad91bac3911a41b2ef5a852f89568aaa (patch)
tree0270661c3f1e566f4c470a26c247a4c6c9335d5c /src
parent51be2e14c632d45e63a40659dea2177133251dfa (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')
-rw-r--r--src/theory/bv/bitblast/aig_bitblaster.cpp5
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback