From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 22 Jan 2013 23:03:46 +0000 (-0500)
Subject: fix for theory preprocessing cache on clang, perhaps others.
X-Git-Tag: cvc5-1.0.0~7391^2~30
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=deeef8b39989203ae4f2e4a39d80e68730412382;p=cvc5.git

fix for theory preprocessing cache on clang, perhaps others.
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c0aa58647..2ea0e866f 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -740,8 +740,7 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa
 }
 
 // Recursively traverse a term and call the theory rewriter on its sub-terms
-Node TheoryEngine::ppTheoryRewrite(TNode term)
-{
+Node TheoryEngine::ppTheoryRewrite(TNode term) {
   NodeMap::iterator find = d_ppCache.find(term);
   if (find != d_ppCache.end()) {
     return (*find).second;
@@ -826,7 +825,8 @@ Node TheoryEngine::preprocess(TNode assertion) {
 
     // If this is an atom, we preprocess its terms with the theory ppRewriter
     if (Theory::theoryOf(current) != THEORY_BOOL) {
-      d_ppCache[current] = ppTheoryRewrite(current);
+      Node ppRewritten = ppTheoryRewrite(current);
+      d_ppCache[current] = ppRewritten;
       Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]);
       continue;
     }