Fix datatype dump regression. (#1672)

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 7200b813de7ec4b9c87afd4542c2cf7adf480c18..55956abaa03c17930196402e5b1334b4a0c1b5aa 100644 (file)
--- 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 2f64579e3790f1d9c17e474b7d0585790aa1ac21..8e281810607e1d7f6c1a5bb8c0f6000ae6173667 100644 (file)
--- 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
 %