diff options
author | 2014-12-01 20:12:24 +0000 | |
---|---|---|
committer | 2014-12-01 20:12:24 +0000 | |
commit | a43d167fe29d882a4bdf1e1b9fa2be91310e4a99 (patch) | |
tree | e30882470014fd94e2bffd5d4203bba44ff2c3f3 /Source | |
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')
-rw-r--r-- | Source/Model/ModelParser.cs | 6 | ||||
-rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 7 |
2 files changed, 10 insertions, 3 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 ("}")) { diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index a0d6ba86..250e04c9 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -207,7 +207,12 @@ namespace Microsoft.Boogie.SMTLib // options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false"); TODO: what does this do?
- options.AddWeakSmtOption("MODEL.V2", "true");
+ // Make sure we get something that is parsable as a bitvector
+ options.AddWeakSmtOption("pp.bv_literals", "false");
+ if (!CommandLineOptions.Clo.UseSmtOutputFormat)
+ {
+ options.AddWeakSmtOption("MODEL.V2", "true");
+ }
//options.AddWeakSmtOption("ASYNC_COMMANDS", "false"); TODO: is this needed?
if (!options.OptimizeForBv)
|