Skip to content

Commit

Permalink
Make the error reporter for checking if Z3 is available, more consist…
Browse files Browse the repository at this point in the history
…ent (#5086)

Fixes #5067
### Description
Make the error reporter for checking if Z3 is available, more consistent
between the IDE and various CLI commands

### How has this been tested?
Updated CLI and IDE tests

<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 Feb 20, 2024
1 parent 67daee7 commit 3d4277d
Show file tree
Hide file tree
Showing 32 changed files with 3,318 additions and 3,241 deletions.
1 change: 1 addition & 0 deletions Source/DafnyCore.Test/DooFileTest.cs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ public void RoundTripCurrentVersion() {
var options = DafnyOptions.Default;
options.ApplyDefaultOptionsWithoutSettingsDefault();
var program = ParseProgram("module MyModule { function TheAnswer(): int { 42 } }", options);
options.ProcessSolverOptions(program.Reporter, Token.Cli);
var dooFile = new DooFile(program);

var path = Path.GetTempFileName();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -33,11 +33,9 @@ public IdPattern(Cloner cloner, IdPattern original) : base(cloner.Tok(original.T
Id = original.Id;
Arguments = original.Arguments?.Select(cloner.CloneExtendedPattern).ToList();
HasParenthesis = original.HasParenthesis;
Type = cloner.CloneType(original.Type);
if (cloner.CloneResolvedFields) {
BoundVar = cloner.CloneIVariable(original.BoundVar, false);
Type = original.Type;
} else {
Type = new InferredTypeProxy();
}
}

Expand All @@ -54,7 +52,7 @@ public IdPattern(IToken tok, String id, Type type, List<ExtendedPattern> argumen
Contract.Requires(id != null);
Contract.Requires(arguments != null); // Arguments can be empty, but shouldn't be null
this.Id = id;
this.Type = type == null ? new InferredTypeProxy() : type;
this.Type = type ?? new InferredTypeProxy();
this.Arguments = arguments;
this.IsGhost = isGhost;
}
Expand Down
Loading

0 comments on commit 3d4277d

Please sign in to comment.