New substitutions implementation - fixes performance issue seen in nonclausal

simplification for some benchmarks

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 1c507eb71..7e06297fb 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -653,7 +653,7 @@ void UnconstrainedSimplifier::processUnconstrained()
     }
     if (!currentSub.isNull()) {
       Assert(currentSub.isVar());
-      d_substitutions.addSubstitution(current, currentSub, false, false, false);
+      d_substitutions.addSubstitution(current, currentSub, false);
     }
     if (workList.empty()) {
       break;
@@ -673,7 +673,7 @@ void UnconstrainedSimplifier::processUnconstrained()
     left = delayQueueLeft.back();
     if (!d_substitutions.hasSubstitution(left)) {
       right = d_substitutions.apply(delayQueueRight.back());
-      d_substitutions.addSubstitution(delayQueueLeft.back(), right, true, true, false);
+      d_substitutions.addSubstitution(delayQueueLeft.back(), right);
     }
     delayQueueLeft.pop_back();
     delayQueueRight.pop_back();