From: Tim King <taking@cs.nyu.edu>
Date: Wed, 14 Nov 2012 22:45:46 +0000 (+0000)
Subject: Beautifying smt_engine.cpp.
X-Git-Tag: cvc5-1.0.0~7599
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1ce18eac8d3479d9c02c623698e8abd2e26cfff3;p=cvc5.git

Beautifying smt_engine.cpp.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ad6bad43e..e1c30c6c7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -227,13 +227,13 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   Node d_divByZero;
 
-  /** 
+  /**
    * Maps from bit-vector width to divison-by-zero uninterpreted
-   * function symbols.  
+   * function symbols.
    */
   hash_map<unsigned, Node> d_BVDivByZero;
   hash_map<unsigned, Node> d_BVRemByZero;
-  
+
 
   /**
    * Function symbol used to implement uninterpreted
@@ -409,23 +409,25 @@ public:
   void addFormula(TNode n)
     throw(TypeCheckingException, LogicException);
 
-  /** 
+  /**
    * Return the uinterpreted function symbol corresponding to division-by-zero
-   * for this particular bit-wdith 
+   * for this particular bit-wdith
    * @param k should be UREM or UDIV
-   * @param width 
-   * 
-   * @return 
+   * @param width
+   *
+   * @return
    */
   Node getBVDivByZero(Kind k, unsigned width);
-  /** 
-   * Returns the node modeling the division-by-zero semantics of node n. 
-   * 
-   * @param n 
-   * 
-   * @return 
+
+  /**
+   * Returns the node modeling the division-by-zero semantics of node n.
+   *
+   * @param n
+   *
+   * @return
    */
   Node expandBVDivByZero(TNode n);
+
   /**
    * Expand definitions in n.
    */