diff options
Diffstat (limited to 'test/regress/regress0/sygus')
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/strings-concat-3-args.sy | 18 |
2 files changed, 20 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index a297cee81..6dfcb922a 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -65,7 +65,8 @@ TESTS = commutative.sy \ parse-bv-let.sy \ cegar1.sy \ triv-type-mismatch-si.sy \ - nia-max-square-ns.sy + nia-max-square-ns.sy \ + strings-concat-3-args.sy # sygus tests currently taking too long for make regress diff --git a/test/regress/regress0/sygus/strings-concat-3-args.sy b/test/regress/regress0/sygus/strings-concat-3-args.sy new file mode 100644 index 000000000..3c93c51d3 --- /dev/null +++ b/test/regress/regress0/sygus/strings-concat-3-args.sy @@ -0,0 +1,18 @@ +; EXPECT: unsat +; COMMAND-LINE: --no-dump-synth +(set-logic SLIA) +(synth-fun f ((x String)) String +((Start String (ntString)) + +(ntString String (x "" (str.++ ntStringConst ntString ntString))) + +(ntStringConst String ("a" "b" " ")) + +)) + +; can be solved with concat PBE strategy, although we currently are not (issue #1259) +; regardless, this is small enough to solve quickly +(constraint (= (f "def") "ab def")) + +(check-synth) + |