3 files changed, 17 insertions, 10 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index cdb6c77f3..e65369f96 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -63,6 +63,18 @@ void TheoryArith::preRegisterTerm(TNode n){
   d_internal->preRegisterTerm(n);
 }
 
+void TheoryArith::finishInit()
+{
+  TheoryModel* tm = d_valuation.getModel();
+  Assert(tm != nullptr);
+  if (getLogicInfo().isTheoryEnabled(THEORY_ARITH)
+      && getLogicInfo().areTranscendentalsUsed())
+  {
+    // witness is used to eliminate square root
+    tm->setUnevaluatedKind(kind::WITNESS);
+  }
+}
+
 Node TheoryArith::expandDefinition(Node node)
 {
   return d_internal->expandDefinition(node);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index f15db32a1..8672f7145 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -58,6 +58,8 @@ public:
    */
   void preRegisterTerm(TNode n) override;
 
+  void finishInit() override;
+
   Node expandDefinition(Node node) override;
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 0f2f4bbf4..7fdab2034 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1337,7 +1337,8 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o
     if (m.getVarList().singleton()){
       VarList vl = m.getVarList();
       Node var = vl.getNode();
-      if (var.getKind() == kind::VARIABLE){
+      if (var.isVar())
+      {
         // if vl.isIntegral then m.getConstant().isOne()
         if(!vl.isIntegral() || m.getConstant().isOne()){
           minVar = var;
@@ -1362,15 +1363,8 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o
             << minVar << ":" << elim << endl;
         Debug("simplify") << right.size() << endl;
       }
-      else if (expr::hasSubterm(elim, minVar))
-      {
-        Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute "
-                             "due to recursive pattern with sharing: "
-                          << minVar << ":" << elim << endl;
-      }
-      else if (!minVar.getType().isInteger() || right.isIntegral())
+      else if (d_containing.isLegalElimination(minVar, elim))
       {
-        Assert(!expr::hasSubterm(elim, minVar));
         // cannot eliminate integers here unless we know the resulting
         // substitution is integral
         Debug("simplify") << "TheoryArithPrivate::solve(): substitution "
@@ -1382,7 +1376,6 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o
       else
       {
         Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute "
-                             "b/c it's integer: "
                           << minVar << ":" << minVar.getType() << " |-> "
                           << elim << ":" << elim.getType() << endl;
       }