diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-16 16:41:29 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-16 16:41:29 -0800 |
| commit | 98962b4d3037c381fadc41e19f7ae9a1ddd82b7b (patch) | |
| tree | 12478b21a2b6456f7e3813edf4e28447457ff5d5 | |
| parent | ae2fb8ac9f22c9ad65a3d08dfe8319ea0160b0ea (diff) | |
bv::utils::mk(And|Or) Do not return true if size of vector is 0. (#1613)
| -rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 13 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_utils.h | 6 |
2 files changed, 12 insertions, 7 deletions
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 1c59ae2d4..2c543b3da 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -316,9 +316,16 @@ void CoreSolver::buildModel() return; } - Node lemma = utils::mkOr(equalities); - d_bv->lemma(lemma); - Debug("bv-core") << " lemma: " << lemma << "\n"; + if (equalities.size() == 0) + { + Debug("bv-core") << " lemma: true (no equalities)" << std::endl; + } + else + { + Node lemma = utils::mkOr(equalities); + d_bv->lemma(lemma); + Debug("bv-core") << " lemma: " << lemma << std::endl; + } return; } diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 5c1080901..7b08ef83f 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -125,8 +125,7 @@ template<bool ref_count> Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions) { std::set<TNode> all(conjunctions.begin(), conjunctions.end()); - - if (all.size() == 0) { return mkTrue(); } + Assert(all.size() > 0); /* All the same, or just one */ if (all.size() == 1) { return conjunctions[0]; } @@ -145,8 +144,7 @@ template<bool ref_count> Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes) { std::set<TNode> all(nodes.begin(), nodes.end()); - - if (all.size() == 0) { return mkTrue(); } + Assert(all.size() > 0); /* All the same, or just one */ if (all.size() == 1) { return nodes[0]; } |