diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress0/sygus/array-grammar-select.sy | 15 | ||||
-rw-r--r-- | test/regress/regress0/sygus/array-grammar-store.sy | 14 |
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) |