Skip to content

Commit

Permalink
Hide --solver-log option (#3798)
Browse files Browse the repository at this point in the history
Hide --solver-log option

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
keyboardDrummer authored Mar 27, 2023
1 parent f709c2b commit c0bfb79
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 1 deletion.
6 changes: 5 additions & 1 deletion Source/DafnyCore/Options/CommonOptionBag.cs
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,11 @@ datatype with a single non-ghost constructor that has a single

public static readonly Option<uint> SolverResourceLimit = new("--resource-limit", @"Specify the maximum resource limit (rlimit) value to pass to Z3. Multiplied by 1000 before sending to Z3.");
public static readonly Option<string> SolverPlugin = new("--solver-plugin", @"Specify a plugin to use to solve verification conditions (instead of an external Z3 process).");
public static readonly Option<string> SolverLog = new("--solver-log", @"Specify a file to use to log the SMT-Lib text sent to the solver.");

public static readonly Option<string> SolverLog =
new("--solver-log", @"Specify a file to use to log the SMT-Lib text sent to the solver.") {
IsHidden = true
};
public static readonly Option<bool> JsonDiagnostics = new("--json-diagnostics", @"Deprecated. Return diagnostics in a JSON format.") {
IsHidden = true
};
Expand Down
1 change: 1 addition & 0 deletions docs/dev/news/solverLog.fix
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
The --solver-log option is now hidden from help unless --help-internal is used.

0 comments on commit c0bfb79

Please sign in to comment.