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/Provers/SMTLib/Z3.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/Provers/SMTLib/Z3.cs')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 7 |
1 files changed, 6 insertions, 1 deletions
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)
|