added model generation for bv subtheories and bv-inequality solver option

1 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f7f689850..b89ca8fa4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1129,6 +1129,11 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
 }
 
+Node TheoryEngine::getModelValue(TNode var) {
+  Assert(d_sharedTerms.isShared(var));
+  return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
+}
+
 static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
 
   std::set<TNode> all;