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

Fixes #4482.

diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 7cf6a79bd35c5f3622cd70b1419af59ebc11b12b..5d544ae57284a1b5fc45820148daf6dacd749ef5 100644 (file)
--- 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();

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ea98cf8191db2d6580a82f0e40374785bcc2ee2a..506857479e66e9698f13022410383b31fa7368a9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -375,6 +375,7 @@ set(regress_0_tests
   regress0/cvc3.userdoc.05.cvc
   regress0/cvc3.userdoc.06.cvc
   regress0/cvc-rerror-print.cvc
+  regress0/datatypes/4482-unc-simp-one.smt2
   regress0/datatypes/Test1-tup-mp.cvc
   regress0/datatypes/boolean-equality.cvc
   regress0/datatypes/boolean-terms-datatype.cvc

diff --git a/test/regress/regress0/datatypes/4482-unc-simp-one.smt2 b/test/regress/regress0/datatypes/4482-unc-simp-one.smt2
new file mode 100644 (file)
index 0000000..265aeef
--- /dev/null
+++ b/test/regress/regress0/datatypes/4482-unc-simp-one.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun a () Tuple)
+(assert (distinct a mkTuple))
+(check-sat)