diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-01 01:31:07 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-01 01:31:07 +0200 |
| commit | 91f40dee752910fca5d749656c0b6ee1bc1281aa (patch) | |
| tree | 4db131923ceabe2fff9f408fc39032bac973e399 /src/theory/quantifiers/fun_def_process.cpp | |
| parent | bf7f7d6960f6e03e90880dd3da9ff1bf00943cf3 (diff) | |
Make --fmf-fun and --macros-quant work in incremental mode. Add regressions.
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.cpp')
| -rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 32097d3eb..0197bda6b 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -44,10 +44,11 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { Message() << "Cannot define function " << f << " more than once." << std::endl; exit( 0 ); } - + Node bd = TermDb::getFunDefBody( assertions[i] ); Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl; if( !bd.isNull() ){ + d_funcs.push_back( f ); bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd ); //create a sort S that represents the inputs of the function |