diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-13 16:27:48 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-13 16:27:48 -0500 |
| commit | 3b36892dec58f945b7e724395c53a288f9d2d0ef (patch) | |
| tree | b0b6b066d0b618f518bedf094e8d38c2d123c471 /test/regress | |
| parent | b9a903cc9a13c7bcdd334eb38730e62858321f07 (diff) | |
Fix SyGuS define-fun printing from benchmarks coming from v1 parser (#4256)
A recent change made it so that defined functions would print as the anonymous lambda corresponding to their definition if the SyGuS v1 parser was used. This was caused by comparison with the wrong kind in the new API.
Notice that the v2 parser does not have this issue.
This also adds a regression to ensure this behavior is maintained by the SyGuS v2 parser.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/print-define-fun.sy | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 72621e5ab..7b675d60e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1007,6 +1007,7 @@ set(regress_0_tests regress0/sygus/parse-bv-let.sy regress0/sygus/pbe-pred-contra.sy regress0/sygus/pLTL-sygus-syntax-err.sy + regress0/sygus/print-define-fun.sy regress0/sygus/real-si-all.sy regress0/sygus/sygus-no-wf.sy regress0/sygus/sygus-uf.sy diff --git a/test/regress/regress0/sygus/print-define-fun.sy b/test/regress/regress0/sygus/print-define-fun.sy new file mode 100644 index 000000000..e6c7e4748 --- /dev/null +++ b/test/regress/regress0/sygus/print-define-fun.sy @@ -0,0 +1,7 @@ +; COMMAND-LINE: --lang=sygus2 +; EXPECT: unsat +; EXPECT: (define-fun g ((x Int)) Int (f 0)) +(set-logic LIA) +(define-fun f ((x Int)) Int (+ x 1)) +(synth-fun g ((x Int)) Int ((Start Int)) ((Start Int ((f 0))))) +(check-synth) |