eager bit-blasting gives models for boolean variables too (fixes bug618)

diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index eca9f12ab34183d0eed2c5f133d65df84f9b007a..3f076bd4c9fb646fb65d84e82f067520758a50de 100644 (file)
--- 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));