summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r--src/theory/bv/theory_bv.cpp6
1 files changed, 6 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback