summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-12-08 10:14:31 -0600
committerGitHub <noreply@github.com>2017-12-08 10:14:31 -0600
commit564234963dd7e76c8d9b88ef941a6683694e5b53 (patch)
tree313e46520c07d1536fffbad4b7080937cfc09aae /src/theory/bv/theory_bv.cpp
parent805d4b7483e51a9b4d24058d493f85700a87f099 (diff)
Make collect model info return a Bool (#1421)
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r--src/theory/bv/theory_bv.cpp13
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index e03cecdd9..cb214217c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -576,18 +576,21 @@ bool TheoryBV::doExtfReductions( std::vector< Node >& terms ) {
bool TheoryBV::needsCheckLastEffort() {
return d_needsLastCallCheck;
}
-
-void TheoryBV::collectModelInfo( TheoryModel* m ){
+bool TheoryBV::collectModelInfo(TheoryModel* m)
+{
Assert(!inConflict());
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- d_eagerSolver->collectModelInfo(m, true);
+ if (!d_eagerSolver->collectModelInfo(m, true))
+ {
+ return false;
+ }
}
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
if (d_subtheories[i]->isComplete()) {
- d_subtheories[i]->collectModelInfo(m, true);
- return;
+ return d_subtheories[i]->collectModelInfo(m, true);
}
}
+ return true;
}
Node TheoryBV::getModelValue(TNode var) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback