Fix Coverity issues (#4587)

This commit fixes the following Coverity issues:

- 1495606: uninitialized field
- 1495605: uninitialized field
- 1488953: uninitialized field
- 1495604: mismatched iterator

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 88974dc69965dbf717fce1b874ea7b244690eaec..325da8cdb603335382308249c56cbbbbf29895fe 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1119,7 +1119,7 @@ size_t SortHashFunction::operator()(const Sort& s) const
 /* Op                                                                     */
 /* -------------------------------------------------------------------------- */
 
-Op::Op() : d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {}
+Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {}
 
 Op::Op(const Solver* slv, const Kind k)
     : d_solver(slv), d_kind(k), d_expr(new CVC4::Expr())
@@ -1628,7 +1628,7 @@ Term::const_iterator::const_iterator(const Solver* slv,
 }
 
 Term::const_iterator::const_iterator(const const_iterator& it)
-    : d_orig_expr(nullptr)
+    : d_solver(nullptr), d_orig_expr(nullptr)
 {
   if (it.d_orig_expr != nullptr)
   {
@@ -1920,7 +1920,7 @@ std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl)
 
 /* DatatypeSelector --------------------------------------------------------- */
 
-DatatypeSelector::DatatypeSelector() { d_stor = nullptr; }
+DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {}
 
 DatatypeSelector::DatatypeSelector(const Solver* slv,
                                    const CVC4::DatatypeConstructorArg& stor)

diff --git a/src/theory/arith/nl/nl_monomial.cpp b/src/theory/arith/nl/nl_monomial.cpp
index e8e7aceba30c815f51d5839b082dadc9ec6cbd94..678a94819ce561f379738610375af8a9697c5c2d 100644 (file)
--- a/src/theory/arith/nl/nl_monomial.cpp
+++ b/src/theory/arith/nl/nl_monomial.cpp
@@ -276,7 +276,7 @@ Node MonomialDb::getContainsDiff(Node a, Node b) const
 {
   std::map<Node, std::map<Node, Node> >::const_iterator it =
       d_m_contain_mult.find(a);
-  if (it == d_m_contain_umult.end())
+  if (it == d_m_contain_mult.end())
   {
     return Node::null();
   }