diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d10678bf6..83d8fb612 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2003,8 +2003,9 @@ void SmtEngine::setDefaults() { } // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm // is one that is specialized for returning a single solution. Non-basic - // sygus algorithms currently include the PBE solver, static template - // inference for invariant synthesis, and single invocation techniques. + // sygus algorithms currently include the PBE solver, UNIF+PI, static + // template inference for invariant synthesis, and single invocation + // techniques. bool reqBasicSygus = false; if (options::produceAbducts()) { @@ -2035,11 +2036,10 @@ void SmtEngine::setDefaults() { if (!options::sygusUnifPbe.wasSetByUser()) { options::sygusUnifPbe.set(false); - // also disable PBE-specific symmetry breaking unless PBE was enabled - if (!options::sygusSymBreakPbe.wasSetByUser()) - { - options::sygusSymBreakPbe.set(false); - } + } + if (options::sygusUnifPi.wasSetByUser()) + { + options::sygusUnifPi.set(options::SygusUnifPiMode::NONE); } if (!options::sygusInvTemplMode.wasSetByUser()) { |