% 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;
% 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