diff options
Diffstat (limited to 'src/theory/quantifiers/skolemize.h')
| -rw-r--r-- | src/theory/quantifiers/skolemize.h | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index c8e6ec7dd..fbb79f5d2 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -89,10 +89,10 @@ class Skolemize * The skolem constants/functions we generate by this * skolemization are added to sk. * - * The arguments fvTypes and fvs are used if we are + * The argument fvs are used if we are * performing skolemization within a nested quantified * formula. In this case, skolem constants we introduce - * must be parameterized based on fvTypes and must be + * must be parameterized based on the types of fvs and must be * applied to fvs. * * The last two arguments sub and sub_vars are used for @@ -103,7 +103,6 @@ class Skolemize */ static Node mkSkolemizedBody(Node q, Node n, - std::vector<TypeNode>& fvTypes, std::vector<TNode>& fvs, std::vector<Node>& sk, Node& sub, |