summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-01-22 18:03:46 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-01-22 18:03:46 -0500
commitdeeef8b39989203ae4f2e4a39d80e68730412382 (patch)
tree0c181d338f360e84f644c950acff0e3900c6c530 /src/theory/theory_engine.cpp
parentff8ead3db3e5fa90839c82cc38215df3c3ef73c1 (diff)
fix for theory preprocessing cache on clang, perhaps others.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp6
1 files changed, 3 insertions, 3 deletions
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback