diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/README | 7 | ||||
| -rw-r--r-- | test/regress/regress0/Makefile.am | 5 | ||||
| -rw-r--r-- | test/regress/regress0/arrayinuf_declare.smt2 | 4 | ||||
| -rw-r--r-- | test/regress/regress0/arrayinuf_error.smt2 | 4 | ||||
| -rw-r--r-- | test/regress/regress0/bug220.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/bug398.smt2 | 2 | ||||
| -rwxr-xr-x | test/regress/run_regression | 15 |
7 files changed, 26 insertions, 13 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] diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 067b5d381..e2d6664cd 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -46,6 +46,7 @@ SMT_TESTS = \ # Regression tests for SMT2 inputs SMT2_TESTS = \ + arrayinuf_declare.smt2 \ chained-equality.smt2 \ ite2.smt2 \ ite3.smt2 \ @@ -164,12 +165,14 @@ EXTRA_DIST = $(TESTS) \ if CVC4_BUILD_PROFILE_COMPETITION else TESTS += \ - error.cvc + error.cvc \ + arrayinuf_error.smt2 endif # and make sure to distribute it EXTRA_DIST += \ subranges.cvc \ + arrayinuf_error.smt2 \ error.cvc # synonyms for "check" in this directory diff --git a/test/regress/regress0/arrayinuf_declare.smt2 b/test/regress/regress0/arrayinuf_declare.smt2 new file mode 100644 index 000000000..5b73f2405 --- /dev/null +++ b/test/regress/regress0/arrayinuf_declare.smt2 @@ -0,0 +1,4 @@ +; EXIT: 0 +(set-logic QF_UF) +(declare-sort Array 1) +(declare-fun a ((Array Bool) Bool Bool) Bool) 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 diff --git a/test/regress/regress0/bug220.smt2 b/test/regress/regress0/bug220.smt2 index 117ee3be2..1520bcde0 100644 --- a/test/regress/regress0/bug220.smt2 +++ b/test/regress/regress0/bug220.smt2 @@ -1,2 +1,2 @@ -% EXIT: 0 +; EXIT: 0 (exit) diff --git a/test/regress/regress0/bug398.smt2 b/test/regress/regress0/bug398.smt2 index 0423d11a4..3e4a1faca 100644 --- a/test/regress/regress0/bug398.smt2 +++ b/test/regress/regress0/bug398.smt2 @@ -1,3 +1,3 @@ -% EXIT: 0 +; EXIT: 0 (set-logic QF_LRA) (define-fun x () Real (+ 4 1)) diff --git a/test/regress/run_regression b/test/regress/run_regression index ef2bb9a35..ec9e17057 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -114,19 +114,14 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then if [ -z "$expected_exit_status" ]; then expected_exit_status=0 fi - elif grep '^\(%\|;\) \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then - expected_output=`grep '^[%;] EXPECT: ' "$benchmark" | sed 's,^[%;] EXPECT: ,,'` - expected_error=`grep '^[%;] EXPECT-ERROR: ' "$benchmark" | sed 's,^[%;] EXPECT-ERROR: ,,'` - expected_exit_status=`grep -m 1 '^[%;] EXIT: ' "$benchmark" | perl -pe 's,^[%;] EXIT: ,,;s,\r,,'` - command_line=`grep '^[%;] COMMAND-LINE: ' "$benchmark" | sed 's,^[%;] COMMAND-LINE: ,,'` - # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle - # this frustrates our auto-language-detection - gettemp tmpbenchmark cvc4_benchmark.smt2.$$.XXXXXXXXXX - grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark" + elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then + expected_output=`grep '^; EXPECT: ' "$benchmark" | sed 's,^; EXPECT: ,,'` + expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'` + expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'` + command_line=`grep '^; COMMAND-LINE: ' "$benchmark" | sed 's,^; COMMAND-LINE: ,,'` if [ -z "$expected_exit_status" ]; then expected_exit_status=0 fi - benchmark=$tmpbenchmark elif grep '^ *( *set-info *:status *sat' "$benchmark" &>/dev/null; then expected_output=sat expected_exit_status=0 |