summaryrefslogtreecommitdiff
path: root/src/theory/bv/bitblaster.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/bitblaster.cpp')
-rw-r--r--src/theory/bv/bitblaster.cpp4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index a9c6d2676..60a98e6e5 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -173,6 +173,10 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
*
*/
+bool Bitblaster::propagate() {
+ return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
+}
+
bool Bitblaster::assertToSat(TNode lit, bool propagate) {
// strip the not
TNode atom;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback