From ed87e0c1ccb0cb93cdedf5229c6a2b47af77743c Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 17 Feb 2014 18:59:39 -0500
Subject: Don't theory-preprocess under quantifiers; but DO theory-preprocess
 lemmas (resolves bug #548).

---
 src/theory/arith/theory_arith.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/theory/arith/theory_arith.cpp')

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 239385bfc..85d9d1f9b 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -52,7 +52,7 @@ void TheoryArith::addSharedTerm(TNode n){
 }
 
 Node TheoryArith::ppRewrite(TNode atom) {
-  CodeTimer timer(d_ppRewriteTimer);
+  CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
   return d_internal->ppRewrite(atom);
 }
 
-- 
cgit v1.2.3