summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv')
-rw-r--r--src/theory/bv/bv_sat.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp
index f580aee44..6f91335ce 100644
--- a/src/theory/bv/bv_sat.cpp
+++ b/src/theory/bv/bv_sat.cpp
@@ -22,6 +22,7 @@
#include "theory/rewriter.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
+#include "prop/sat_solver_factory.h"
using namespace std;
@@ -184,7 +185,7 @@ void Bitblaster::assertToSat(TNode lit) {
bool Bitblaster::solve() {
Trace("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n";
- return SatValTrue == d_satSolver->solve(d_assertedAtoms);
+ return SAT_VALUE_TRUE == d_satSolver->solve(d_assertedAtoms);
}
void Bitblaster::getConflict(std::vector<TNode>& conflict) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback