Enable and fix dump test (#7387)

Fixes #1649. The test was not enabled before and was still expecting
CVC-style output.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fca1543c41ffdc83242a25502de398e1a8f8c342..3ea588e01b3360416dd0f2a0ef6c1fcf3b3df2f4 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -479,6 +479,7 @@ set(regress_0_tests
   regress0/datatypes/coda_simp_model.smt2
   regress0/datatypes/conqueue-dt-enum-iloop.smt2
   regress0/datatypes/data-nested-codata.smt2
+  regress0/datatypes/datatype-dump.cvc.smt2
   regress0/datatypes/datatype.cvc.smt2
   regress0/datatypes/datatype0.cvc.smt2
   regress0/datatypes/datatype1.cvc.smt2

diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc.smt2 b/test/regress/regress0/datatypes/datatype-dump.cvc.smt2
index f1aae6bb1098d52d85f3959684c3470378ed5e20..7d5495fccba6e0906180f1856ebc3b67160e889c 100644 (file)
--- a/test/regress/regress0/datatypes/datatype-dump.cvc.smt2
+++ b/test/regress/regress0/datatypes/datatype-dump.cvc.smt2
@@ -1,14 +1,11 @@
 ; COMMAND-LINE: -o raw-benchmark
-; EXPECT: OPTION "incremental" false;
-; EXPECT: OPTION "logic" "ALL";
-; EXPECT: DATATYPE
-; EXPECT:   nat = succ(pred: nat) | zero
-; EXPECT: END;
-; EXPECT: x : nat;
-; EXPECT: QUERY NOT(is_succ(x)) AND NOT(is_zero(x));
+; EXPECT: (set-option :incremental false)
+; EXPECT: (set-logic ALL)
+; EXPECT: (declare-datatypes ((nat 0)) (((succ (pred nat)) (zero))))
+; EXPECT: (declare-fun x () nat)
+; EXPECT: (check-sat-assuming ( (not (and (not ((_ is succ) x)) (not ((_ is zero) x)))) ))
 ; EXPECT: sat
 (set-logic ALL)
-(set-option :incremental false)
 (declare-datatypes ((nat 0)) (((succ (pred nat)) (zero))))
 (declare-fun x () nat)
 (check-sat-assuming ( (not (and (not ((_ is succ) x)) (not ((_ is zero) x)))) ))