diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-05 14:48:08 -0500 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-05 16:18:27 -0500 |
| commit | a06ad1d49a4b76c686f1b2eca64830b0f3eddc0a (patch) | |
| tree | 07f0258ca19230ddafcce8fe95674ace6fa77565 /test/regress/regress0/arrayinuf_error.smt2 | |
| parent | 2f13bdf81d0477b4ab807a118e493ea0c5357e2f (diff) | |
Array smtlib compliance tests
Diffstat (limited to 'test/regress/regress0/arrayinuf_error.smt2')
| -rw-r--r-- | test/regress/regress0/arrayinuf_error.smt2 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test/regress/regress0/arrayinuf_error.smt2 b/test/regress/regress0/arrayinuf_error.smt2 new file mode 100644 index 000000000..d029b2b6a --- /dev/null +++ b/test/regress/regress0/arrayinuf_error.smt2 @@ -0,0 +1,4 @@ +; EXPECT-ERROR: (error "Parse Error: arrayinuf_error.smt2:3.21: Symbol 'Array' not declared as a type") +(set-logic QF_UF) +(declare-fun a (Array Bool Bool)) +; EXIT: 1 |