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 /src/parser | |
| 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 'src/parser')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 2 |
1 files changed, 1 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; |