Handle recursive singleton case for codatatypes, add regression. Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.

1 files changed, 9 insertions, 1 deletions

diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index d37aa1b7d..244cb303d 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Clark Barrett
  ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters, Tim King, Liana Hadarean, Peter Collingbourne
+ ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters, Tim King, Liana Hadarean, Peter Collingbourne, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -197,6 +197,14 @@ void UnconstrainedSimplifier::processUnconstrained()
               break;
             }
           }
+          if( parent[0].getType().isDatatype() ){
+            TypeNode tn = parent[0].getType();
+            const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+            if( dt.isRecursiveSingleton() ){
+              //domain size may be 1
+              break;
+            }
+          }
         case kind::BITVECTOR_COMP:
         case kind::LT:
         case kind::LEQ: