Removing comments related to issues (#3232)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3c10516e45f83ff7b94cdd6d9f1aacd6e12e4926..562f2a89721efb7f5c335308b6ec29b2dae1b8b4 100644 (file)
--- 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 cb3189e81a1e398cd63a53f3736bfe4686297196..fcb5859d451ffc10406f6257fb75ed12074e3605 100644 (file)
--- 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 cabb17f48379ae2f0ea2d142885e63f2c4c7ebd1..b5cc16fc86f0f51fa6a52959d1d02e9a0eee0734 100644 (file)
--- 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 c4be410843efa7df6358a6f689ea78019dd39fb1..0aa6ea5cc57152db0b13b21f210d4be34d8af516 100644 (file)
--- 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;