diff options
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.cpp')
| -rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 22dac2225..a46aca3c8 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -46,6 +46,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { } Node bd = TermDb::getFunDefBody( assertions[i] ); + Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl; Assert( !bd.isNull() ); bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd ); |