diff options
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 2 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/print-define-fun.sy | 7 |
3 files changed, 9 insertions, 1 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2405b3402..6cba1ce19 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1293,7 +1293,7 @@ void Smt2::mkSygusDatatype(api::DatatypeDecl& dt, // the given name. spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]); } - else if (!sop.isNull() && sop.getKind() == api::VARIABLE) + else if (!sop.isNull() && sop.getKind() == api::CONSTANT) { Debug("parser-sygus") << "--> Defined function " << ops[i] << std::endl; 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) |