summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2017-04-04 11:21:30 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2017-04-04 11:21:30 -0500
commit6c0a62d69368b1af7e9777efcd703da6dc1cda11 (patch)
tree677d518d345a230c35bfbcb016fca199185f131e /src/theory/bv
parent6cb3f49d3933061000fe63d2ee7e004cae06d6ba (diff)
Simplify Theory::collectModelInfo interface to not take deprecated fullModel argument.
Diffstat (limited to 'src/theory/bv')
-rw-r--r--src/theory/bv/theory_bv.cpp6
-rw-r--r--src/theory/bv/theory_bv.h2
2 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 651d44841..9db909c22 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -576,14 +576,14 @@ bool TheoryBV::needsCheckLastEffort() {
return d_needsLastCallCheck;
}
-void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
+void TheoryBV::collectModelInfo( TheoryModel* m ){
Assert(!inConflict());
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- d_eagerSolver->collectModelInfo(m, fullModel);
+ d_eagerSolver->collectModelInfo(m, true);
}
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
if (d_subtheories[i]->isComplete()) {
- d_subtheories[i]->collectModelInfo(m, fullModel);
+ d_subtheories[i]->collectModelInfo(m, true);
return;
}
}
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 9973b0736..62eb6f6b5 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -77,7 +77,7 @@ public:
Node explain(TNode n);
- void collectModelInfo( TheoryModel* m, bool fullModel );
+ void collectModelInfo( TheoryModel* m );
std::string identify() const { return std::string("TheoryBV"); }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback