Fix missing check for cardinality one in unconstrained simplifier (#4504)

Fixes #4482.

1 files changed, 4 insertions, 0 deletions

diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 7cf6a79bd..5d544ae57 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -236,6 +236,10 @@ void UnconstrainedSimplifier::processUnconstrained()
               break;
             }
           }
+          if (parent[0].getType().getCardinality().isOne())
+          {
+            break;
+          }
           if (parent[0].getType().isDatatype())
           {
             TypeNode tn = parent[0].getType();