added specific command line options to enable the SMTLIB2 output model parser for Z3. Use /proverOpt:SMTLIB2_MODEL=true

1 files changed, 6 insertions, 16 deletions

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 34d39863..7668b370 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -695,20 +695,20 @@ namespace Microsoft.Boogie
       foreach (var f in functions) f.Substitute(mapping);

     }

 

-	public static List<Model> ParseModels(System.IO.TextReader rd, string modelType)

+	public static List<Model> ParseModels(System.IO.TextReader rd, string prover)

 	{

 		ModelParser p;

-

-		switch (modelType)

+		

+		switch (prover)

 		{

-			case "Z3":

-			p = new ParserZ3();

+			case "Z3_SMTLIB2":

+			p = new ParserZ3_SMTLIB2();

 			break;

 			case "CVC4":

 			p = new ParserCVC4();

 			break;

 			default:

-			p = new ParserZ3_2();

+			p = new ParserZ3();

 			break;

 		}

 

@@ -717,15 +717,5 @@ namespace Microsoft.Boogie
 

 		return p.resModels;

 	}

-

-	public static List<Model> ParseModels(System.IO.TextReader rd)

-	{

-		ModelParser p = new ParserZ3_2();

-

-		p.rd = rd;

-		p.Run();

-

-		return p.resModels;

-	}

   }

 }