getModelValue implementation in bitvectors

2 files changed, 8 insertions, 0 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 57a77c0d2..e28ef3ddf 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -137,6 +137,12 @@ void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
   
 }
 
+Node TheoryBV::getModelValue(TNode var) {
+  Assert(!inConflict());
+  return d_bitblastSolver.getModelValue(var);
+}
+
+
 void TheoryBV::propagate(Effort e) {
   Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index e38f3568c..ffb043bb6 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -117,6 +117,8 @@ private:
 
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
+  Node getModelValue(TNode var);
+
   inline std::string indent()
   {
     std::string indentStr(getSatContext()->getLevel(), ' ');