diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-10-20 18:31:52 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-21 01:31:52 +0000 |
commit | 5ee9b4685a2aeceebeb109b9578be0562efbf700 (patch) | |
tree | a231ffb813653c1e2da5b38f24a9bd87a6f16b45 | |
parent | e590612dc4421d45cacc451a7b8a162acd9c7943 (diff) |
Enable and fix dump test (#7387)
Fixes #1649. The test was not enabled before and was still expecting
CVC-style output.
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/datatype-dump.cvc.smt2 | 13 |
2 files changed, 6 insertions, 8 deletions
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)))) )) |