From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Sat, 17 Feb 2018 00:41:29 +0000 (-0800)
Subject: bv::utils::mk(And|Or) Do not return true if size of vector is 0. (#1613)
X-Git-Tag: cvc5-1.0.0~5279
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=98962b4d3037c381fadc41e19f7ae9a1ddd82b7b;p=cvc5.git

bv::utils::mk(And|Or) Do not return true if size of vector is 0. (#1613)
---

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]; }