diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-08-04 15:23:54 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-04 15:23:54 -0500 |
| commit | 24a40040a4a5f88f96eada87e46323ace729f06a (patch) | |
| tree | e2d74981a9f0d2ceb8bc973c619c71a3e099f2fe /src/smt/smt_engine.cpp | |
| parent | 0cbcf1f835f74c304e2ac3884143b7df9c7f75b6 (diff) | |
Modify the smt2 parser to use the Sygus grammar. (#4829)
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6d1e7ffbc..91ff522b5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1604,7 +1604,9 @@ void SmtEngine::declareSynthFun(const std::string& id, setUserAttribute("sygus-synth-grammar", func, attr_value, ""); } Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n"; - Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars); + // dumping SynthFunCommand from smt-engine is currently broken (please take at + // CVC4/cvc4-projects#211) + // Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars); // sygus conjecture is now stale setSygusConjectureStale(); } |