Fix regressions in regress1 after #4613. (#4616)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 16 Jun 2020 01:18:01 +0000 (18:18 -0700)
committerGitHub <noreply@github.com>
Tue, 16 Jun 2020 01:18:01 +0000 (18:18 -0700)
test/regress/regress1/datatypes/error.cvc
test/regress/regress1/error.cvc

index 90c13c615d005c2852e9b322357689f62a3d20a4..5f3e31522e276fa2418e5496b01b89e1005533d6 100644 (file)
@@ -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;
index 986527f98695b1b1507f266b364f7001b4303c78..8d67ae372fc42285d4ee833ca5b49b7215bde7be 100644 (file)
@@ -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