summaryrefslogtreecommitdiff
path: root/src/smt/check_models.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/check_models.cpp')
-rw-r--r--src/smt/check_models.cpp1
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>())
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback