summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/dynamic_rewrite.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/dynamic_rewrite.cpp')
-rw-r--r--src/theory/quantifiers/dynamic_rewrite.cpp9
1 files changed, 4 insertions, 5 deletions
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index 00e527aba..352d6892f 100644
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -1,10 +1,10 @@
/********************* */
-/*! \file dynamic_rewriter.cpp
+/*! \file dynamic_rewrite.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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
@@ -24,8 +24,7 @@ namespace theory {
namespace quantifiers {
DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe)
- : d_qe(qe),
- d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true),
+ : d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true),
d_rewrites(qe->getUserContext())
{
d_equalityEngine.addFunctionKind(kind::APPLY_UF);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback