diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-17 22:09:45 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-17 22:09:45 -0500 |
| commit | f1a4096e579b101642c5a47eb5c8e90476ccc81a (patch) | |
| tree | a4c9e048888b759d7bc99bbb5afb9ef879ef1c49 /src/smt/smt_engine.cpp | |
| parent | 1823d6d537a59d85a17f09f53c8128d934c420a3 (diff) | |
Sygus query generator (#2465)
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 38c9e7ee2..196da6b9c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1876,7 +1876,8 @@ void SmtEngine::setDefaults() { options::sygusExtRew.set(false); } } - if (options::sygusRewSynth() || options::sygusRewVerify()) + if (options::sygusRewSynth() || options::sygusRewVerify() + || options::sygusQueryGen()) { // rewrite rule synthesis implies that sygus stream must be true options::sygusStream.set(true); |