From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 16 Oct 2015 09:17:00 +0000 (+0200)
Subject: Fix for codatatype constant rewrite, add regression.
X-Git-Tag: cvc5-1.0.0~6205
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b2c093f53f446479d38e49a051e8bd6133bd4ae0;p=cvc5.git

Fix for codatatype constant rewrite, add regression.
---

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);
         }
       }
     }
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index fc110ed92..45a9d6f30 100644
--- 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
index 000000000..672acfa44
--- /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