diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-27 14:46:57 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-27 14:46:57 -0700 |
| commit | 7b4af4309de9ae134eac20af13a87f1036733e0d (patch) | |
| tree | e4f0a8d8ff3b16153a90620b2dc2b7937e7aac28 /Source/Provers/Z3/Prover.cs | |
| parent | ae44269a34b002797b2583b93a0041059b57cbda (diff) | |
Boogie: internal clean-up, removed BvHandling type, everything now behaves as if the old /bv:z were used
Diffstat (limited to 'Source/Provers/Z3/Prover.cs')
| -rw-r--r-- | Source/Provers/Z3/Prover.cs | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs index 8929e732..6a066f1f 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -156,11 +156,8 @@ namespace Microsoft.Boogie.Z3 if (opts.Inspector != null)
AddOption(result, "PROGRESS_SAMPLING_FREQ", "100");
- if (opts.Typed) {
- AddOption(result, "TYPE_CHECK", "true");
- if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native)
- AddOption(result, "BV_REFLECT", "true");
- }
+ AddOption(result, "TYPE_CHECK", "true");
+ AddOption(result, "BV_REFLECT", "true");
foreach (string opt in CommandLineOptions.Clo.Z3Options) {
Contract.Assert(opt != null);
|