Array smtlib compliance tests

5 files changed, 14 insertions, 3 deletions

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))