cmake: Disable C++ GNU extensions. (#3446)

Fixes #971.

1 files changed, 0 insertions, 19 deletions

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 8e60863fa..a9b786615 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -88,25 +88,6 @@ class CnfStream {
   /** Pointer to the proof corresponding to this CnfStream */
   CnfProof* d_cnfProof;
 
-  /**
-   * How many literals were already mapped at the top-level when we
-   * tried to convertAndAssert() something.  This
-   * achieves early detection of units and leads to fewer
-   * clauses.  It's motivated by the following pattern:
-   *
-   *   ASSERT  BIG FORMULA => x
-   *   (and then later...)
-   *   ASSERT  BIG FORMULA
-   *
-   * With the first assert, BIG FORMULA is clausified, and a literal
-   * is assigned for the top level so that the final clause for the
-   * implication is "lit => x".  But without "fortunate literal
-   * detection," when BIG FORMULA is later asserted, it is clausified
-   * separately, and "lit" is never asserted as a unit clause.
-   */
-  // KEEP_STATISTIC(IntStat, d_fortunateLiterals,
-  //               "prop::CnfStream::fortunateLiterals", 0);
-
   /** Remove nots from the node */
   TNode stripNot(TNode node) {
     while (node.getKind() == kind::NOT) {