diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-08 18:06:16 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-08 16:06:16 -0700 |
| commit | 1b6784fe52f4fb745262842e0406d6dd34053cb2 (patch) | |
| tree | 6c64a7485612f8af60631fde4dd827222d17215d /test/regress/regress0/sygus | |
| parent | 16b54708ff83a1bf6393203b79da6dc059fd2025 (diff) | |
Limit cases of sygus inference based on type (#3370)
This makes `--sygus-inference` a no-op for inputs where there is a free function whose sort cannot be handled in a sygus grammar.
It also fixes an issue where skolem variables were not being treated as functions-to-synthesize.
Fixes #3250 and fixes #3356.
Diffstat (limited to 'test/regress/regress0/sygus')
| -rw-r--r-- | test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2 | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2 b/test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2 new file mode 100644 index 000000000..b35b7253c --- /dev/null +++ b/test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --sygus-inference +; EXPECT: sat +(set-logic ALL) +(declare-sort S 1) +(define-sort SB () (S Bool)) +(declare-fun A () (S Bool)) +(declare-fun B () SB) +(assert (= A B)) +; do not do sygus inference due to uninterpreted sorts +(check-sat) +(exit) |