diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-24 10:29:36 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-24 10:29:36 +0200 |
| commit | b09cdf3e0f407c69c8df8023b70c776d1b0a4589 (patch) | |
| tree | 9e1e0de8c02ecc300a2eae581b412e56072e0dde /src/theory/quantifiers/fun_def_process.cpp | |
| parent | 0bf9566178b30b81ee27ead42bcbfaa668f738e1 (diff) | |
Fix sygus parser for non-tokenized operators, reenable regression. Fix for --fmf-fun.
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.cpp')
| -rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index f47cb8f1e..cb379ec92 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -136,7 +136,7 @@ Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& co childChanged = c!=n[i] || childChanged; } if( childChanged ){ - nn = n; + nn = NodeManager::currentNM()->mkNode( n.getKind(), children ); } }else{ //simplify term |