projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
attempt to improve CVC4's "parse error" message
[cvc5.git] / test / regress / regress0 / arrayinuf_error.smt2
1 ; EXPECT-ERROR: (error "Parse Error: arrayinuf_error.smt2:7.21: Symbol 'Array' not declared as a type
2 ; EXPECT-ERROR:
3 ; EXPECT-ERROR: (declare-fun a (Array Bool Bool))
4 ; EXPECT-ERROR: ^
5 ; EXPECT-ERROR: ")
6 (set-logic QF_UF)
7 (declare-fun a (Array Bool Bool))
8 ; EXIT: 1