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/README | |
| parent | 2f13bdf81d0477b4ab807a118e493ea0c5357e2f (diff) | |
Array smtlib compliance tests
Diffstat (limited to 'test/regress/README')
| -rw-r--r-- | test/regress/README | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/README b/test/regress/README index bef93b140..58cd2f2e7 100644 --- a/test/regress/README +++ b/test/regress/README @@ -39,6 +39,7 @@ QUERY TRUE; syntax error; % EXIT: 1 +[Outdated: please also see edit below as an addendum.] Use of % gestures in CVC format is natural, as these are comments and ignored by the CVC presentation language lexer. In SMT and SMT2 formats, you can do the same, putting % gestures in the file. However, the run_regression script @@ -54,3 +55,9 @@ is left verbatim (and never processed to remove the % EXPECT: lines) by the run_regression script. -- Morgan Deters <mdeters@cs.nyu.edu> Thu, 01 Jul 2010 13:36:53 -0400 + +[Edit 2014/03/14: No support for '%' in .smt2 files any +longer. Please use ';' or create separate .expect files. Very few test +were using this "feature" and was causing issues because temp file +name changed the expected error output string. '%' works for .smt files +--Kshitij] |