diff options
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index eca9f12ab..3f076bd4c 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -187,7 +187,8 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { TNodeSet::iterator it = d_variables.begin(); for (; it!= d_variables.end(); ++it) { TNode var = *it; - if (d_bv->isLeaf(var) || isSharedTerm(var)) { + if (d_bv->isLeaf(var) || isSharedTerm(var) || + (var.isVar() && var.getType().isBoolean())) { // only shared terms could not have been bit-blasted Assert (hasBBTerm(var) || isSharedTerm(var)); |