Skip to content

Commit

Permalink
fix description
Browse files Browse the repository at this point in the history
  • Loading branch information
Martin Suda authored and quickbeam123 committed Dec 7, 2023
1 parent f43eb76 commit 5cb1320
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Shell/Options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1661,8 +1661,8 @@ void Options::init()
_unitResultingResolution = ChoiceOptionValue<URResolution>("unit_resulting_resolution","urr",URResolution::OFF,{"ec_only","off","on","full"});
_unitResultingResolution.description=
"Uses unit resulting resolution only to derive empty clauses (may be useful for splitting)."
" 'ec_only' only derives empty clauses, 'on' does everything (but implements a heuristic to skip deriving more than one empty clause)"
" 'full' ignores this heuristic is thus complete also under AVATAR.";
" 'ec_only' only derives empty clauses, 'on' does everything (but implements a heuristic to skip deriving more than one empty clause),"
" 'full' ignores this heuristic and is thus complete also under AVATAR.";
_lookup.insert(&_unitResultingResolution);
_unitResultingResolution.tag(OptionTag::INFERENCES);
_unitResultingResolution.onlyUsefulWith(ProperSaturationAlgorithm());
Expand Down

0 comments on commit 5cb1320

Please sign in to comment.