From 5082cb8349efbb287084293cd4bc6c3fa5a34f26 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 7 May 2012 22:17:35 +0000 Subject: Fixing a bug with TheoryArith::ppAssert() and shared terms. --- src/theory/arith/theory_arith.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src') 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; -- cgit v1.2.3