Merge branch 'master' into evalStrCodeevalStrCode

3 files changed, 31 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5304fcab5..c4dbab1dd 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -840,6 +840,8 @@ set(regress_0_tests
   regress0/strings/type001.smt2
   regress0/strings/unsound-0908.smt2
   regress0/strings/unsound-repl-rewrite.smt2
+  regress0/sygus/array-grammar-select.sy
+  regress0/sygus/array-grammar-store.sy
   regress0/sygus/General_plus10.sy
   regress0/sygus/aig-si.sy
   regress0/sygus/c100.sy
diff --git a/test/regress/regress0/sygus/array-grammar-select.sy b/test/regress/regress0/sygus/array-grammar-select.sy
new file mode 100644
index 000000000..d216bbb24
--- /dev/null
+++ b/test/regress/regress0/sygus/array-grammar-select.sy
@@ -0,0 +1,15 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALIA)
+
+(synth-fun f
+  ((s (Array Int Int)) (t Int))
+  Int
+  )
+
+(declare-var x (Array Int Int))
+
+(constraint (= (= (select x 0) (select x 1)) (= (f x 0) (f x 1))))
+
+
+(check-synth)
diff --git a/test/regress/regress0/sygus/array-grammar-store.sy b/test/regress/regress0/sygus/array-grammar-store.sy
new file mode 100644
index 000000000..70525e83b
--- /dev/null
+++ b/test/regress/regress0/sygus/array-grammar-store.sy
@@ -0,0 +1,14 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ABV)
+
+(synth-fun f
+  ((s (Array (BitVec 4) (BitVec 4))) (t (BitVec 4)))
+  (Array (BitVec 4) (BitVec 4))
+  )
+
+(declare-var x (Array (BitVec 4) (BitVec 4)))
+
+(constraint (= (= (store x #b0000 #b0000) (store x #b0001 #b0000)) (= (f x #b0000) (f x #b0001))))
+
+(check-synth)