diff options
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.cpp')
| -rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index fecefb8e1..0339b54f5 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -33,6 +33,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) { std::vector< int > fd_assertions; std::map< int, Node > subs_head; //first pass : find defined functions, transform quantifiers + NodeManager* nm = NodeManager::currentNM(); for( unsigned i=0; i<assertions.size(); i++ ){ Node n = QuantAttributes::getFunDefHead( assertions[i] ); if( !n.isNull() ){ @@ -62,9 +63,10 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) { //create functions f1...fn mapping from this sort to concrete elements for( unsigned j=0; j<n.getNumChildren(); j++ ){ TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() ); - std::stringstream ss; - ss << f << "_arg_" << j; - d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) ); + std::stringstream ssf; + ssf << f << "_arg_" << j; + d_input_arg_inj[f].push_back( + nm->mkSkolem(ssf.str(), typ, "op created during fun def fmf")); } //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn] |