summaryrefslogtreecommitdiff
path: root/src/theory/bv/bv_eager_solver.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/bv_eager_solver.cpp')
-rw-r--r--src/theory/bv/bv_eager_solver.cpp5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 50070b29a..01282880c 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -123,9 +123,10 @@ bool EagerBitblastSolver::hasAssertions(const std::vector<TNode>& formulas) {
return true;
}
-void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
AlwaysAssert(!d_useAig && d_bitblaster);
- d_bitblaster->collectModelInfo(m, fullModel);
+ return d_bitblaster->collectModelInfo(m, fullModel);
}
void EagerBitblastSolver::setProofLog(BitVectorProof* bvp) { d_bvp = bvp; }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback