diff options
| -rw-r--r-- | src/smt/model_blocker.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp index 39fa7a4f8..33831b918 100644 --- a/src/smt/model_blocker.cpp +++ b/src/smt/model_blocker.cpp @@ -239,7 +239,13 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions, blockers.push_back(a); } } - blocker = nm->mkNode(OR, blockers); + if (blockers.size() == 0) { + blocker = nm->mkConst<bool>(true); + } else if (blockers.size() == 1) { + blocker = blockers[0]; + } else { + blocker = nm->mkNode(OR, blockers); + } } Trace("model-blocker") << "...model blocker is " << blocker << std::endl; return blocker.toExpr(); |