From: Liana Hadarean <lianahady@gmail.com>
Date: Mon, 24 Aug 2015 09:40:18 +0000 (+0100)
Subject: eager bit-blasting gives models for boolean variables too (fixes bug618)
X-Git-Tag: cvc5-1.0.0~6252^2~9
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d455be07def0b09c3eadbe4e602950fddd4aec1c;p=cvc5.git

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 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));