diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-06-15 18:18:01 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-15 18:18:01 -0700 |
commit | e5f880a7bb603734a737e026ba64c035b0517468 (patch) | |
tree | bce3e2437714852e1b7163a9662d56bf30a0ca93 | |
parent | df98bc96168869e1615bc0756bde3b2c5dba160e (diff) |
Fix regressions in regress1 after #4613. (#4616)
-rw-r--r-- | test/regress/regress1/datatypes/error.cvc | 3 | ||||
-rw-r--r-- | test/regress/regress1/error.cvc | 4 |
2 files changed, 3 insertions, 4 deletions
diff --git a/test/regress/regress1/datatypes/error.cvc b/test/regress/regress1/datatypes/error.cvc index 90c13c615..5f3e31522 100644 --- a/test/regress/regress1/datatypes/error.cvc +++ b/test/regress/regress1/datatypes/error.cvc @@ -1,6 +1,5 @@ % REQUIRES: no-competition -% EXPECT-ERROR: CVC4 Error: -% EXPECT-ERROR: Parse Error: foo already declared in this datatype +% EXPECT-ERROR: (error "Parse Error: foo already declared in this datatype") % EXIT: 1 DATATYPE single_ctor = foo(bar:REAL) | foo(bar2:REAL) END; diff --git a/test/regress/regress1/error.cvc b/test/regress/regress1/error.cvc index 986527f98..8d67ae372 100644 --- a/test/regress/regress1/error.cvc +++ b/test/regress/regress1/error.cvc @@ -1,8 +1,8 @@ % REQUIRES: no-competition % ERROR-SCRUBBER: sed -e '/^[[:space:]]*$/d' -% EXPECT-ERROR: CVC4 Error: -% EXPECT-ERROR: Parse Error: error.cvc:7.8: Symbol 'BOOL' not declared as a type +% EXPECT-ERROR: (error "Parse Error: error.cvc:7.8: Symbol 'BOOL' not declared as a type % EXPECT-ERROR: p : BOOL; % EXPECT-ERROR: ^ +% EXPECT-ERROR: ") p : BOOL; % EXIT: 1 |