From b85e8a3d3f66ca844dc9b4790cd549a8dd0739a7 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 10 Sep 2021 21:33:19 -0700 Subject: [PATCH] checkModel: Extend documentation. (#7177) Add comment that partial operators are one reason that the current assertion cannot be checked. --- src/smt/check_models.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.30.2