summaryrefslogtreecommitdiff
path: root/src/theory/bv/bv_subtheory.h
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/bv_subtheory.h
parent805d4b7483e51a9b4d24058d493f85700a87f099 (diff)
Make collect model info return a Bool (#1421)
Diffstat (limited to 'src/theory/bv/bv_subtheory.h')
-rw-r--r--src/theory/bv/bv_subtheory.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 454f89b6c..63dd53407 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -75,7 +75,7 @@ class SubtheorySolver {
virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
virtual void preRegister(TNode node) {}
virtual void propagate(Theory::Effort e) {}
- virtual void collectModelInfo(TheoryModel* m, bool fullModel) = 0;
+ virtual bool collectModelInfo(TheoryModel* m, bool fullModel) = 0;
virtual Node getModelValue(TNode var) = 0;
virtual bool isComplete() = 0;
virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback