diff options
Diffstat (limited to 'src/preprocessing/passes/ackermann.cpp')
-rw-r--r-- | src/preprocessing/passes/ackermann.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index a7b33ae26..af6cae796 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -276,9 +276,13 @@ void usortsToBitVectors(const LogicInfo& d_logic, for (size_t i = 0, size = assertions->size(); i < size; ++i) { Node old = (*assertions)[i]; - assertions->replace(i, usVarsToBVVars.apply((*assertions)[i])); - Trace("uninterpretedSorts-to-bv") - << " " << old << " => " << (*assertions)[i] << "\n"; + Node newA = usVarsToBVVars.apply((*assertions)[i]); + if (newA != old) + { + assertions->replace(i, newA); + Trace("uninterpretedSorts-to-bv") + << " " << old << " => " << (*assertions)[i] << "\n"; + } } } } |