From 7c0b92c30688d8c7830bf3611213e96026ecf1f5 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 20 May 2020 21:22:25 -0500
Subject: Fix missing check for cardinality one in unconstrained simplifier
 (#4504)

Fixes #4482.
---
 src/preprocessing/passes/unconstrained_simplifier.cpp | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/preprocessing/passes')

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();
-- 
cgit v1.2.3