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/regress1 | |
| 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/regress1')
| -rw-r--r-- | test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2 | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2 b/test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2 new file mode 100644 index 000000000..bb6a63490 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun a () Real) +(assert + (and + (and + (exists ((?b Real)) (forall ((?c Real)) (exists ((?d Real)) + (or (and (and (and (and (< (+ (+ (+ 0 (* 68.0 ?c)) 0) (* 33.0 a)) 0.0) (<= 0 2.0)) + (or (<= 0 (+ (* (+ (* 55.0 ?d) 0) (* 49.0 ?b)) 0)))))))))) + ) + ) +) + +(check-sat) |