diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-10 15:48:05 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-10 15:48:05 -0600 |
| commit | e0009c822488a2c39f8907e37333409c1191d47b (patch) | |
| tree | bfc4c40a5d8789769ab5d4827aa9562986e0f475 /src/smt/check_models.cpp | |
| parent | cef8ceaf4cd81863171363fe54a97921361d1de9 (diff) | |
Do not mark extended functions as reduced based on decomposing contains (#5407)
Fixes #5381.
Diffstat (limited to 'src/smt/check_models.cpp')
| -rw-r--r-- | src/smt/check_models.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index a55f53f96..612084de2 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -174,6 +174,7 @@ void CheckModels::checkModel(Model* m, Notice() << "SmtEngine::checkModel(): checking assertion " << assertion << std::endl; Node n = assertion; + Notice() << "SmtEngine::checkModel(): -- rewritten form is " << Rewriter::rewrite(n) << std::endl; Node nr = Rewriter::rewrite(substitutions.apply(n)); if (nr.isConst() && nr.getConst<bool>()) { |