From: Aina Niemetz Date: Sat, 11 Sep 2021 04:33:19 +0000 (-0700) Subject: checkModel: Extend documentation. (#7177) X-Git-Tag: cvc5-1.0.0~1231 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b85e8a3d3f66ca844dc9b4790cd549a8dd0739a7;p=cvc5.git checkModel: Extend documentation. (#7177) Add comment that partial operators are one reason that the current assertion cannot be checked. --- diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index d3a2dfefa..304d261a6 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -88,7 +88,8 @@ void CheckModels::checkModel(TheoryModel* m, // Otherwise, we did not succeed in showing the current assertion to be // true. This may either indicate that our model is wrong, or that we cannot // check it. The latter may be the case for several reasons. - // For example, quantified formulas are not checkable, although we assign + // One example is the occurrence of partial operators. Another example + // are quantified formulas, which are not checkable, although we assign // them to true/false based on the satisfying assignment. However, // quantified formulas can be modified during preprocess, so they may not // correspond to those in the satisfying assignment. Hence we throw