2 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 501aafb29..f48a03975 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -127,3 +127,7 @@ EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
 void BitblastSolver::collectModelInfo(TheoryModel* m) {
   return d_bitblaster->collectModelInfo(m); 
 }
+
+Node BitblastSolver::getModelValue(TNode node) {
+  return d_bitblaster->getVarValue(node);
+}
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 3396d813b..510006710 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -45,7 +45,8 @@ public:
   bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
-  void collectModelInfo(TheoryModel* m); 
+  void collectModelInfo(TheoryModel* m);
+  Node getModelValue(TNode node);
 };
 
 }