// compiler directs the user to the template file instead of the
// generated one. We don't want the user to modify the generated one,
// since it'll get overwritten on a later build.
-#line 31 "${template}"
+#line 32 "${template}"
#ifdef CVC4_STATISTICS_ON
#define INC_STAT(kind) \
* @param options the earlyTypeChecking field is used to configure
* whether to do at Expr creation time.
*/
- explicit ExprManager(const Options&);
+ explicit ExprManager(const Options& options);
/**
* Destroys the expression manager. No will be deallocated at this point, so
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief #inclusion of this file marks a header as private and generates a
+ ** \brief #-inclusion of this file marks a header as private and generates a
** warning when the file is included improperly.
**
- ** #inclusion of this file marks a header as private and generates a
+ ** #-inclusion of this file marks a header as private and generates a
** warning when the file is included improperly.
**/
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief #inclusion of this file marks a header as private and generates a
+ ** \brief #-inclusion of this file marks a header as private and generates a
** warning when the file is included improperly.
**
- ** #inclusion of this file marks a header as private and generates a
+ ** #-inclusion of this file marks a header as private and generates a
** warning when the file is included improperly.
**/