diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-09 11:36:37 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-09 11:36:37 -0600 |
| commit | 8ada7b0ac4b3832d8fbf5e31080cb85df330049f (patch) | |
| tree | e58569b2544fe88daf6f41b1b6babbb63319f8be /src/theory/quantifiers/quantifiers_rewriter.cpp | |
| parent | 22b211647501a4dad5cec66c2ea6383ea8e7b7bd (diff) | |
Higher-order prep (#1338)
* Minor preparation for final higher-order merge.
* Format
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0ffed5243..45c418996 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -105,6 +105,10 @@ void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node activeMap[ n ] = true; } }else{ + if (n.hasOperator()) + { + computeArgs(args, activeMap, n.getOperator(), visited); + } for( int i=0; i<(int)n.getNumChildren(); i++ ){ computeArgs( args, activeMap, n[i], visited ); } |