Fix for codatatype constant rewrite, add regression.

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 4b60044d06272e90e612fadf9642b0a7b7ff0cb1..bd44f66a944cbdabf7277b58a7eefbc38045d566 100644 (file)
--- 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);
         }
       }
     }

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index fc110ed92cf64661ae3c1f74a99434466025fc2c..45a9d6f307fdf32568653265c2c52dd88c8e9321 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -66,7 +66,8 @@ TESTS =       \
        is_test.smt2 \
        manos-model.smt2 \
        bug625.smt2 \
-       cdt-model-cade15.smt2
+       cdt-model-cade15.smt2 \
+       sc-cdt1.smt2
 
 FAILING_TESTS = \
        datatype-dump.cvc

diff --git a/test/regress/regress0/datatypes/sc-cdt1.smt2 b/test/regress/regress0/datatypes/sc-cdt1.smt2
new file mode 100644 (file)
index 0000000..672acfa
--- /dev/null
+++ b/test/regress/regress0/datatypes/sc-cdt1.smt2
@@ -0,0 +1,19 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-sort term 0)
+(declare-codatatypes () (
+    (llist_tree (lnil_tree )
+        (lcons_tree (_select_llist_tree_0 tree)
+        (_select_llist_tree_1 llist_tree)))
+    (tree (leaf (_select_tree_0 term))
+        (node (_select_tree_1 llist_tree)))
+))
+(declare-fun nun_sk_2 () term)
+(declare-fun nun_sk_1 () term)
+(declare-fun nun_sk_0 () tree)
+(assert
+    (= nun_sk_0
+        (node
+         (lcons_tree (leaf nun_sk_1)
+          (lcons_tree (leaf nun_sk_2) (lcons_tree nun_sk_0 lnil_tree))))))
+(check-sat)
\ No newline at end of file