From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 28 Aug 2019 23:18:52 +0000 (-0500)
Subject: Removing comments related to issues (#3232)
X-Git-Tag: cvc5-1.0.0~3988
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cc7546ff0a4e418de9a21c03ef12b1d5e8801bb8;p=cvc5.git

Removing comments related to issues (#3232)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3c10516e4..562f2a897 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3782,7 +3782,6 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
 
     // Check that SAT results generate a model correctly.
     if(options::checkModels()) {
-      // TODO (#1693) check model when unknown result?
       if (r.asSatisfiabilityResult().isSat() == Result::SAT)
       {
         checkModel();
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index cb3189e81..fcb5859d4 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -233,7 +233,6 @@ private: //for universe set
    * If the sets-ext option is not set and we have an extended operator, 
    * we throw an exception. This function is a no-op otherwise.
    *
-   * This is related to github issue #1076
    * TheorySets uses expandDefinition as an entry point to see if the input
    * contains extended operators.
    *
diff --git a/src/theory/theory.h b/src/theory/theory.h
index cabb17f48..b5cc16fc8 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -430,8 +430,7 @@ public:
    * possible, for example in handling under-specified operations
    * using partially defined functions.
    *
-   * TODO (github issue #1076): 
-   * some theories like sets use expandDefinition as a "context
+   * Some theories like sets use expandDefinition as a "context
    * independent preRegisterTerm".  This is required for cases where
    * a theory wants to be notified about a term before preprocessing
    * and simplification but doesn't necessarily want to rewrite it.
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index c4be41084..0aa6ea5cc 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -824,7 +824,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
 void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m)
 {
   // if we are incomplete, there is no guarantee on the model.
-  // thus, we do not check the model here. (related to #1693).
+  // thus, we do not check the model here.
   if (incomplete)
   {
     return;