Fix for codatatype constant rewrite, add regression.

1 files changed, 6 insertions, 2 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 4b60044d0..bd44f66a9 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -59,11 +59,15 @@ public:
         }
       }
       if( in.isConst() ){
+        Trace("datatypes-rewrite-debug") << "Normalizing constant " << in << std::endl;
         Node inn = normalizeConstant( in );
-        Assert( !inn.isNull() );
-        if( inn!=in ){
+        //constant may be a subterm of another constant, so cannot assume that this will succeed for codatatypes
+        //Assert( !inn.isNull() );
+        if( !inn.isNull() && inn!=in ){
           Trace("datatypes-rewrite") << "Normalized constant " << in << " -> " << inn << std::endl;
           return RewriteResponse(REWRITE_DONE, inn);
+        }else{
+          return RewriteResponse(REWRITE_DONE, in);
         }
       }
     }