diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-07 22:17:35 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-07 22:17:35 +0000 |
commit | 5082cb8349efbb287084293cd4bc6c3fa5a34f26 (patch) | |
tree | 2a0e6d5244c4d1dde828d53de4252f7ba5d59e57 /src/theory | |
parent | 9f18a444d5c926cffa0532995a3a50cf74a98769 (diff) |
Fixing a bug with TheoryArith::ppAssert() and shared terms.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index f24b8f411..c7072de72 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -570,9 +570,11 @@ Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubst // x = (p - ax - c) * -1/a // Add the substitution if not recursive Assert(elim == Rewriter::rewrite(elim)); - Assert(!elim.hasSubterm(minVar)); - if (!minVar.getType().isInteger() || right.isIntegral()) { + if(elim.hasSubterm(minVar)){ + Debug("simplify") << "TheoryArith::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl; + }else if (!minVar.getType().isInteger() || right.isIntegral()) { + Assert(!elim.hasSubterm(minVar)); // cannot eliminate integers here unless we know the resulting // substitution is integral Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl; |