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 1c59ae2d4b9702e6fd1d6294c89d6948e0d6275e..2c543b3dae8fd5bdf6f00a7d8cdf28a8a0334cce 100644 (file)
--- 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 5c10809015e713457ec2765bd7529e4b682f9c9d..7b08ef83f0e85b4b228ce145ca4bf598e17c4511 100644 (file)
--- 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]; }