From 70d1a0171840cd62b5c1d89b875ffb50da216793 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan@cs.nyu.edu>
Date: Tue, 26 Mar 2013 16:52:21 -0400
Subject: getModelValue implementation in bitvectors

---
 src/theory/bv/theory_bv.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/theory/bv/theory_bv.cpp')

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;
 
-- 
cgit v1.2.3