diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-16 11:17:00 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-16 11:17:00 +0200 |
commit | b2c093f53f446479d38e49a051e8bd6133bd4ae0 (patch) | |
tree | 2eb28c524a30d3809c407a8418ceb4f98b41fb45 /src/theory | |
parent | 8914ff73f09a0e0b4c3bc40107c9345c8ea43760 (diff) |
Fix for codatatype constant rewrite, add regression.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 8 |
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); } } } |