diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-27 14:22:08 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-27 14:22:08 -0700 |
| commit | ae44269a34b002797b2583b93a0041059b57cbda (patch) | |
| tree | 3ec4a7a8ca3477298f93feb1267d854062a26417 /Source/Provers | |
| parent | 6be1fd5fa2617602d0a86e95d656018b172ef8d2 (diff) | |
Boogie: Eliminated the /bv option. Only native bitvectors are supported now. The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/Isabelle/Prover.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Provers/Isabelle/Prover.cs b/Source/Provers/Isabelle/Prover.cs index 60a8de22..8bf6bbf0 100644 --- a/Source/Provers/Isabelle/Prover.cs +++ b/Source/Provers/Isabelle/Prover.cs @@ -192,7 +192,7 @@ namespace Microsoft.Boogie.Isabelle { public readonly bool AllTypes;
public IsabelleContext(string outputFilename, bool allTypes)
- : base(new VCExpressionGenerator(), new VCGenerationOptions(new List<string/*!*/>(new string/*!*/[] { "bvInt", "bvDefSem", "bvint", "bvz", "external" }))) {
+ : base(new VCExpressionGenerator(), new VCGenerationOptions(new List<string/*!*/> { "bvInt", "bvDefSem", "bvint", "bvz", "external" })) {
Contract.Requires(outputFilename != null);
this.OutputFilename = outputFilename;
|