diff options
author | Liana Hadarean <lianahady@gmail.com> | 2015-08-24 10:40:18 +0100 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2015-08-24 17:50:49 +0100 |
commit | d455be07def0b09c3eadbe4e602950fddd4aec1c (patch) | |
tree | 8bd2290f37a939e49a4958140c020622b517d3f0 /src/theory/bv/eager_bitblaster.cpp | |
parent | d7dc7c2b3038b862af5ea55e7cf6b1fc4e1fe684 (diff) |
eager bit-blasting gives models for boolean variables too (fixes bug618)
Diffstat (limited to 'src/theory/bv/eager_bitblaster.cpp')
-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)); |