From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 8 Dec 2011 19:23:45 +0000 (+0000)
Subject: Disable a BV rewriter statistic (after checking with Liana) that was static,
X-Git-Tag: cvc5-1.0.0~8363
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=67dc3b98a30a6ad2f93743f3313ba5f4149af389;p=cvc5.git

Disable a BV rewriter statistic (after checking with Liana) that was static,
and thus caused big problems with programs that create two SmtEngines in
one process.

If we need state like this in the rewriters, we'll need to make them
nonstatic.
---

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 68f75847f..32bbf973f 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -91,8 +91,13 @@ class RewriteRule {
     }
   };
 
-  /** Statistics about the rule */
-  static RuleStatistics* s_statictics;
+  /* Statistics about the rule */
+  // NOTE: Cannot have static fields like this, or else you can't have
+  // two SmtEngines in the process (the second-to-be-destroyed will
+  // have a dangling pointer and segfault).  If this statistic is needed,
+  // fix the rewriter by making it an instance per-SmtEngine (instead of
+  // static).
+  //static RuleStatistics* s_statistics;
 
   /** Actually apply the rewrite rule */
   static inline Node apply(Node node) {
@@ -102,14 +107,18 @@ class RewriteRule {
 public:
 
   RewriteRule() {
-    if (s_statictics == NULL) {
-      s_statictics = new RuleStatistics();
+    /*
+    if (s_statistics == NULL) {
+      s_statistics = new RuleStatistics();
     }
+    */
   }
 
   ~RewriteRule() {
-    delete s_statictics;
-    s_statictics = NULL;
+    /*
+    delete s_statistics;
+    s_statistics = NULL;
+    */
   }
 
   static inline bool applies(Node node) {
@@ -121,7 +130,7 @@ public:
     if (!checkApplies || applies(node)) {
       BVDebug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ")" << std::endl;
       Assert(checkApplies || applies(node));
-      ++ s_statictics->d_ruleApplications;
+      //++ s_statistics->d_ruleApplications;
       Node result = apply(node);
       BVDebug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;
       return result;
@@ -131,8 +140,10 @@ public:
   }
 };
 
+/*
 template<RewriteRuleId rule>
-typename RewriteRule<rule>::RuleStatistics* RewriteRule<rule>::s_statictics = NULL;
+typename RewriteRule<rule>::RuleStatistics* RewriteRule<rule>::s_statistics = NULL;
+*/
 
 /** Have to list all the rewrite rules to get the statistics out */
 struct AllRewriteRules {