From d455be07def0b09c3eadbe4e602950fddd4aec1c Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Mon, 24 Aug 2015 10:40:18 +0100 Subject: [PATCH] eager bit-blasting gives models for boolean variables too (fixes bug618) --- src/theory/bv/eager_bitblaster.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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)); -- 2.30.2