From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 30 Mar 2018 19:26:28 +0000 (-0500)
Subject: Disable regression (#1731)
X-Git-Tag: cvc5-1.0.0~5194
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cd41d9de391ea93736182e944c10b697d863c6a6;p=cvc5.git

Disable regression (#1731)
---

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index ec29f8350..7f333007a 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -329,7 +329,6 @@ REG0_TESTS = \
 	regress0/datatypes/cdt-non-canon-stream.smt2 \
 	regress0/datatypes/coda_simp_model.smt2 \
 	regress0/datatypes/conqueue-dt-enum-iloop.smt2 \
-	regress0/datatypes/datatype-dump.cvc \
 	regress0/datatypes/datatype.cvc \
 	regress0/datatypes/datatype0.cvc \
 	regress0/datatypes/datatype1.cvc \
@@ -1603,6 +1602,7 @@ REG4_TESTS = \
 # issue1048-arrays-int-real.smt2 -- different errors on debug and production.
 #
 # regress0/aufbv/bug348 does not seem to terminate with proofs
+# regress0/datatypes/datatype-dump.cvc (FIXME #1649)
 DISABLED_TESTS = \
 	regress0/arith/bug549.cvc \
 	regress0/arith/incorrect1.smt \