Fixing a bug with TheoryArith::ppAssert() and shared terms.

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;