summaryrefslogtreecommitdiff
path: root/src/smt/set_defaults.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/set_defaults.cpp')
-rw-r--r--src/smt/set_defaults.cpp15
1 files changed, 13 insertions, 2 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 229fdeec5..f4d885f4b 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -946,9 +946,20 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
? true
: false);
- Trace("smt") << "setting decision mode to " << decMode << std::endl;
opts.decision.decisionMode = decMode;
- opts.decision.decisionStopOnly = stoponly;
+ if (stoponly)
+ {
+ if (opts.decision.decisionMode == options::DecisionMode::JUSTIFICATION)
+ {
+ opts.decision.decisionMode = options::DecisionMode::STOPONLY;
+ }
+ else
+ {
+ Assert(opts.decision.decisionMode == options::DecisionMode::INTERNAL);
+ }
+ }
+ Trace("smt") << "setting decision mode to " << opts.decision.decisionMode
+ << std::endl;
}
if (options::incrementalSolving())
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback