summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/ProverInterface.cs
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-09-24 12:25:11 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-09-24 12:25:11 +0100
commit33afafa2bfdd4de19194734b395b2ff1da756f1e (patch)
tree3ed66902921925d9ea7cb69156da6fe53db9cfb1 /Source/Provers/SMTLib/ProverInterface.cs
parente599209547cabdd5c9663938edec016117e14280 (diff)
Remove dead method argument
Patch by Jeroen Ketema
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs10
1 files changed, 2 insertions, 8 deletions
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);