From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 20 Mar 2018 18:38:28 +0000 (-0500)
Subject: Fix datatype dump regression. (#1672)
X-Git-Tag: cvc5-1.0.0~5231
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=252cd598a389adbb309019883e9a48d091452612;p=cvc5.git

Fix datatype dump regression. (#1672)
---

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 7200b813d..55956abaa 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -83,7 +83,8 @@ TESTS =	\
 	model-subterms-min.smt2 \
 	issue1433.smt2 \
         tuples-empty.smt2 \
-        tuples-multitype.smt2
+        tuples-multitype.smt2 \
+        datatype-dump.cvc
 
 # rec5 -- no longer support subrange types
 FAILING_TESTS = \
diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc b/test/regress/regress0/datatypes/datatype-dump.cvc
index 2f64579e3..8e2818106 100644
--- a/test/regress/regress0/datatypes/datatype-dump.cvc
+++ b/test/regress/regress0/datatypes/datatype-dump.cvc
@@ -1,14 +1,15 @@
 % This regression is the same as datatype.cvc but tests the
 % dumping infrastructure.
 %
-% COMMAND-LINE: --dump assertions
+% COMMAND-LINE: --dump raw-benchmark
 %
+% EXPECT: OPTION "incremental" false;
+% EXPECT: OPTION "logic" "ALL";
 % EXPECT: DATATYPE
 % EXPECT:   nat = succ(pred: nat) | zero
 % EXPECT: END;
 % EXPECT: x : nat;
-% EXPECT: ASSERT NOT(NOT(is_succ(x)) AND NOT(is_zero(x)));
-% EXPECT: CHECKSAT;
+% EXPECT: QUERY NOT(is_succ(x)) AND NOT(is_zero(x));
 % EXPECT: invalid
 %