From 98962b4d3037c381fadc41e19f7ae9a1ddd82b7b Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 16 Feb 2018 16:41:29 -0800
Subject: [PATCH] bv::utils::mk(And|Or) Do not return true if size of vector is
 0. (#1613)

---
 src/theory/bv/bv_subtheory_core.cpp | 13 ++++++++++---
 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]; }
-- 
2.30.2