diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-12-01 20:12:24 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-12-01 20:12:24 +0000 |
| commit | a43d167fe29d882a4bdf1e1b9fa2be91310e4a99 (patch) | |
| tree | e30882470014fd94e2bffd5d4203bba44ff2c3f3 /Source/Model/ModelParser.cs | |
| parent | 2979a82b64ffddf7a3340cc494ff755766996d18 (diff) | |
Patch by Jeroen Ketema
Fix some of the interfacing with Z3 4.3.2 in SMTLib. In particular:
* It makes the useSmtOutputFormat usable
* It fixes parsing of bit vectors that occur in the models returned by Z3
Similar stuff might be broken in the other interfaces to Z3, but it shouldn’t
be more broken than it already was.
Diffstat (limited to 'Source/Model/ModelParser.cs')
| -rw-r--r-- | Source/Model/ModelParser.cs | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs index e456cbcd..3b9fbb6f 100644 --- a/Source/Model/ModelParser.cs +++ b/Source/Model/ModelParser.cs @@ -20,7 +20,8 @@ namespace Microsoft.Boogie internal System.IO.TextReader rd; string lastLine = ""; protected static char[] seps = new char[] { ' ' }; - protected static Regex bv = new Regex (@"\(_ BitVec (\d+)\)"); + protected static Regex bitVec = new Regex (@"\(_ BitVec (\d+)\)"); + protected static Regex bv = new Regex (@"\(_ bv(\d+) (\d+)\)"); protected void NewModel () { @@ -98,7 +99,8 @@ namespace Microsoft.Boogie { if (newLine == null) return null; - newLine = bv.Replace (newLine, "bv${1}"); + newLine = bitVec.Replace (newLine, "bv${1}"); + newLine = bv.Replace (newLine, "bv${1}[${2}]"); string line = newLine; int openParenCounter = CountOpenParentheses (newLine, 0); if (!newLine.Contains ("}")) { |