summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes/synth_rew_rules.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing/passes/synth_rew_rules.cpp')
-rw-r--r--src/preprocessing/passes/synth_rew_rules.cpp7
1 files changed, 3 insertions, 4 deletions
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 7e687329b..3eb27c2f7 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -2,9 +2,9 @@
/*! \file synth_rew_rules.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
@@ -79,8 +79,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
{
Trace("srs-input-debug") << "...preprocess " << cur << std::endl;
visited[cur] = false;
- Kind k = cur.getKind();
- bool isQuant = k == FORALL || k == EXISTS || k == LAMBDA || k == CHOICE;
+ bool isQuant = cur.isClosure();
// we recurse on this node if it is not a quantified formula
if (!isQuant)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback