From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 24 Nov 2021 04:30:47 +0000 (-0800)
Subject: Minor fixes (#7691)
X-Git-Tag: cvc5-1.0.0~777
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=51d8131c7f0c84b6189bd746e420c8932d2da8c5;p=cvc5.git

Minor fixes (#7691)
---

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index c3ceffc4e..7cd475cbb 100644
--- 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 28fd80acc..24a9136e8 100644
--- 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 d8e35d8e5..972fac5a3 100644
--- 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 beb02c1c5..1dfcc044e 100644
--- 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)
       {