diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-20 13:38:28 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-20 11:38:28 -0700 |
| commit | 252cd598a389adbb309019883e9a48d091452612 (patch) | |
| tree | 00e40ba673da0a22379684fc5c740b3423a923f3 /test | |
| parent | 425369ce6f2e355961954c399dfabe917320da52 (diff) | |
Fix datatype dump regression. (#1672)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
| -rw-r--r-- | 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 % |