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/VCExpr | |
| 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/VCExpr')
| -rw-r--r-- | Source/VCExpr/SimplifyLikeLineariser.cs | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs index 58c6ad7a..848fafcb 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -56,12 +56,6 @@ namespace Microsoft.Boogie.VCExprAST { get;
}
- public virtual CommandLineOptions.BvHandling Bitvectors {
- get {
- return CommandLineOptions.BvHandling.None;
- }
- }
-
// variables representing formulas in let-bindings have to be
// printed in a different way than other variables
public virtual List<VCExprVar/*!*/>/*!*/ LetVariables {
@@ -89,19 +83,6 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Invariant(EmptyList != null);
}
-
- public bool NativeBv {
- get {
- return Bitvectors == CommandLineOptions.BvHandling.Z3Native;
- }
- }
-
- public bool IntBv {
- get {
- return Bitvectors == CommandLineOptions.BvHandling.ToInt;
- }
- }
-
////////////////////////////////////////////////////////////////////////////////////////
protected LineariserOptions(bool asTerm) {
|