From: Tim King <taking@cs.nyu.edu>
Date: Wed, 23 Jan 2013 21:34:07 +0000 (-0500)
Subject: Adding substitution size cap.
X-Git-Tag: cvc5-1.0.0~7453
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9883548405f15ca8c18b7602092b186bc6934339;p=cvc5.git

Adding substitution size cap.
---

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 7f7ee3bb1..39ded7991 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -752,8 +752,8 @@ Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubst
       Assert(elim == Rewriter::rewrite(elim));
 
 
-      static const unsigned MAX_SUB_SIZE = 20;
-      if(false && right.size() > MAX_SUB_SIZE){
+      static const unsigned MAX_SUB_SIZE = 2;
+      if(right.size() > MAX_SUB_SIZE){
         Debug("simplify") << "TheoryArith::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl;
         Debug("simplify") << right.size() << endl;
       }else if(elim.hasSubterm(minVar)){