text: /*********************                                                        */
  /*! \file base_options_template.h
   ** \verbatim
   ** Top contributors (to current version):
   **   Morgan Deters, Tim King
   ** This file is part of the CVC4 project.
   ** Copyright (c) 2009-2016 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
   **
   ** \brief Contains code for handling command-line options.
   **
   ** Contains code for handling command-line options
   **/
  
  #include "cvc4_private.h"
  
  #ifndef __CVC4__OPTIONS__FP_H
  #define __CVC4__OPTIONS__FP_H
  
  #include "options/options.h"
  
  
  #line 26 "../../../../../src/options/base_options_template.h"
  
  #define CVC4_OPTIONS__FP__FOR_OPTION_HOLDER
  
  #line 30 "../../../../../src/options/base_options_template.h"
  
  namespace CVC4 {
  
  namespace options {
  
  
  
  #line 38 "../../../../../src/options/base_options_template.h"
  
  }/* CVC4::options namespace */
  
  
  
  #line 44 "../../../../../src/options/base_options_template.h"
  
  namespace options {
  
  
  
  #line 50 "../../../../../src/options/base_options_template.h"
  
  }/* CVC4::options namespace */
  
  }/* CVC4 namespace */
  
  #endif /* __CVC4__OPTIONS__FP_H */
  