diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-10 16:44:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-10 16:44:02 -0500 |
| commit | f1d4d477d7cbfb6c8ba79232986a4135c5647e4a (patch) | |
| tree | 9ec138c6b901172e809fd5fb89e67e4a92ad2239 /src/smt | |
| parent | 817fe6d90c25dbdfe62c658add02efd51e2e29eb (diff) | |
Improve accuracy of stats for sygus sampler (#1755)
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index dd8a2e502..029fb84c9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1481,8 +1481,11 @@ void SmtEngine::setDefaults() { options::boolToBitvector.set(false); } - if(options::produceAssignments() && !options::produceModels()) { - Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl; + // cases where we need produce models + if (!options::produceModels() + && (options::produceAssignments() || options::sygusRewSynthCheck())) + { + Notice() << "SmtEngine: turning on produce-models" << endl; setOption("produce-models", SExpr("true")); } |