diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-09-24 12:25:11 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-09-24 12:25:11 +0100 |
| commit | 33afafa2bfdd4de19194734b395b2ff1da756f1e (patch) | |
| tree | 3ed66902921925d9ea7cb69156da6fe53db9cfb1 | |
| parent | e599209547cabdd5c9663938edec016117e14280 (diff) | |
Remove dead method argument
Patch by Jeroen Ketema
| -rw-r--r-- | Source/Model/Model.cs | 2 | ||||
| -rw-r--r-- | Source/ModelViewer/Main.cs | 4 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 10 |
3 files changed, 5 insertions, 11 deletions
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 154297aa..76b7cb4a 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -695,7 +695,7 @@ namespace Microsoft.Boogie foreach (var f in functions) f.Substitute(mapping);
}
- public static List<Model> ParseModels(System.IO.TextReader rd, string prover)
+ public static List<Model> ParseModels(System.IO.TextReader rd)
{
ModelParser p = new ParserZ3();
p.rd = rd;
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index c5685194..5fed89da 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -99,7 +99,7 @@ namespace Microsoft.Boogie.ModelViewer using (var rd = new StringReader(model))
{
- allModels = Model.ParseModels(rd, "").ToArray();
+ allModels = Model.ParseModels(rd).ToArray();
}
AddAndLoadModel(setModelIdTo);
@@ -112,7 +112,7 @@ namespace Microsoft.Boogie.ModelViewer if (!string.IsNullOrWhiteSpace(modelFileName) && File.Exists(modelFileName)) {
using (var rd = File.OpenText(modelFileName)) {
- allModels = Model.ParseModels(rd,"").ToArray();
+ allModels = Model.ParseModels(rd).ToArray();
}
AddAndLoadModel(setModelIdTo);
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 629c2478..e5cffd93 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -853,7 +853,7 @@ namespace Microsoft.Boogie.SMTLib // Concatenate all the arguments
string modelString = resp[0].Name;
// modelString = modelString.Substring(7, modelString.Length - 8); // remove "(model " and final ")"
- var models = Model.ParseModels(new StringReader("Error model: \n" + modelString), "");
+ var models = Model.ParseModels(new StringReader("Error model: \n" + modelString));
if (models == null || models.Count == 0)
{
HandleProverError("no model from prover: " + resp.ToString());
@@ -1629,14 +1629,8 @@ namespace Microsoft.Boogie.SMTLib try {
switch (options.Solver) {
case SolverKind.Z3:
- if (CommandLineOptions.Clo.UseSmtOutputFormat) {
- models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "");
- } else {
- models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "");
- }
- break;
case SolverKind.CVC4:
- models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "");
+ models = Model.ParseModels(new StringReader("Error model: \n" + modelStr));
break;
default:
Debug.Assert(false);
|