Minor fixes (#7691)

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index c3ceffc4ef8aa064eb7c18d9cb4502470517c164..7cd475cbb745cb5f8edab6e7b67836e0135e54b1 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1967,7 +1967,10 @@ void GetInstantiationsCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetInterpolCommand::GetInterpolCommand(const std::string& name, api::Term conj)
-    : d_name(name), d_conj(conj), d_resultStatus(false)
+    : d_name(name),
+      d_conj(conj),
+      d_sygus_grammar(nullptr),
+      d_resultStatus(false)
 {
 }
 GetInterpolCommand::GetInterpolCommand(const std::string& name,
@@ -2057,7 +2060,10 @@ void GetInterpolCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetAbductCommand::GetAbductCommand(const std::string& name, api::Term conj)
-    : d_name(name), d_conj(conj), d_resultStatus(false)
+    : d_name(name),
+      d_conj(conj),
+      d_sygus_grammar(nullptr),
+      d_resultStatus(false)
 {
 }
 GetAbductCommand::GetAbductCommand(const std::string& name,

diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/cut_log.cpp
index 28fd80acccf06cb9b65ab244c0192003a9247697..24a9136e8b7c8dcf754bd1619ff9af74943a6784 100644 (file)
--- a/src/theory/arith/cut_log.cpp
+++ b/src/theory/arith/cut_log.cpp
@@ -109,6 +109,7 @@ CutInfo::CutInfo(CutInfoKlass kl, int eid, int o)
       d_cutRhs(),
       d_cutVec(),
       d_mAtCreation(-1),
+      d_N(-1),
       d_rowId(-1),
       d_exactPrecision(nullptr),
       d_explanation(nullptr)

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index d8e35d8e540d1323081301caef2bf745e19ea240..972fac5a34d8f6506e6694c8d5f7e8d75ddba7ff 100644 (file)
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -684,8 +684,6 @@ void TheoryFp::postCheck(Effort level)
     Trace("fp-abstraction")
         << "TheoryFp::check(): checking abstractions" << std::endl;
     TheoryModel* m = getValuation().getModel();
-    bool lemmaAdded = false;
-
     for (const auto& [abstract, concrete] : d_abstractionMap)
     {
       Trace("fp-abstraction")
@@ -694,7 +692,7 @@ void TheoryFp::postCheck(Effort level)
       {  // Is actually used in the model
         Trace("fp-abstraction")
             << "TheoryFp::check(): ... relevant" << std::endl;
-        lemmaAdded |= refineAbstraction(m, abstract, concrete);
+        refineAbstraction(m, abstract, concrete);
       }
       else
       {

diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index beb02c1c57b70c78f2ef10ce787b179ae64dd13c..1dfcc044ebfa652736d26d6c87c0a3d1ebfce727 100644 (file)
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -500,8 +500,7 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
         return n;
       }
     }
-    else if (ik == BITVECTOR_UDIV || ik == BITVECTOR_UDIV
-             || ik == BITVECTOR_SDIV)
+    else if (ik == BITVECTOR_UDIV || ik == BITVECTOR_SDIV)
     {
       if (arg == 0)
       {