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 /test/regress/regress0 | |
| parent | e590612dc4421d45cacc451a7b8a162acd9c7943 (diff) | |
Enable and fix dump test (#7387)
Fixes #1649. The test was not enabled before and was still expecting
CVC-style output.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/datatypes/datatype-dump.cvc.smt2 | 13 |
1 files changed, 5 insertions, 8 deletions
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)))) )) |