diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-07-09 22:12:51 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-09 22:12:51 +0100 |
| commit | 0ad93c637c97672fa71c380f9112ea1b7d6572d8 (patch) | |
| tree | 81796eee129a7763e3930c3da31c5b4c4aaac5b0 /Source/Model/ModelParser.cs | |
| parent | e8e4c58f700242eab9e951e01c8a2ee3cafd89de (diff) | |
added specific command line options to enable the SMTLIB2 output model parser for Z3. Use /proverOpt:SMTLIB2_MODEL=true
Diffstat (limited to 'Source/Model/ModelParser.cs')
| -rw-r--r-- | Source/Model/ModelParser.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs index bd3be773..9a455662 100644 --- a/Source/Model/ModelParser.cs +++ b/Source/Model/ModelParser.cs @@ -89,7 +89,7 @@ namespace Microsoft.Boogie abstract internal void Run(); } - class ParserZ3_2 : ModelParser + class ParserZ3 : ModelParser { List<object> GetFunctionTokens(string newLine) { @@ -597,7 +597,7 @@ namespace Microsoft.Boogie } } - internal class ParserZ3 : ParserSMT + internal class ParserZ3_SMTLIB2 : ParserSMT { protected override void ParseArray(ref int i) { |