From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 16 Jun 2020 01:18:01 +0000 (-0700)
Subject: Fix regressions in regress1 after #4613. (#4616)
X-Git-Tag: cvc5-1.0.0~3212
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e5f880a7bb603734a737e026ba64c035b0517468;p=cvc5.git

Fix regressions in regress1 after #4613. (#4616)
---

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