From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 21 Oct 2021 01:31:52 +0000 (-0700)
Subject: Enable and fix dump test (#7387)
X-Git-Tag: cvc5-1.0.0~1023
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5ee9b4685a2aeceebeb109b9578be0562efbf700;p=cvc5.git

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 fca1543c4..3ea588e01 100644
--- 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 f1aae6bb1..7d5495fcc 100644
--- 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)))) ))