From 252cd598a389adbb309019883e9a48d091452612 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 20 Mar 2018 13:38:28 -0500
Subject: [PATCH] Fix datatype dump regression. (#1672)

---
 test/regress/regress0/datatypes/Makefile.am       | 3 ++-
 test/regress/regress0/datatypes/datatype-dump.cvc | 7 ++++---
 2 files changed, 6 insertions(+), 4 deletions(-)

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
 %
 
-- 
2.30.2