From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 5 Mar 2014 19:48:08 +0000 (-0500)
Subject: Array smtlib compliance tests
X-Git-Tag: cvc5-1.0.0~7046^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a06ad1d49a4b76c686f1b2eca64830b0f3eddc0a;p=cvc5.git

Array smtlib compliance tests
---

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