diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-10-27 17:36:29 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-10-27 17:36:29 -0700 |
| commit | a8c04614ad34b4a36c1c739f8838fe4fd6232720 (patch) | |
| tree | 73c080b032638d7e046f7e1d18d5fa7a2273c181 /Source/VCGeneration/Context.cs | |
| parent | 51fe0a74abb863a3bb908e6fced5b9779446d065 (diff) | |
Boogie: Get rid of {:ignore} feature on axioms
Diffstat (limited to 'Source/VCGeneration/Context.cs')
| -rw-r--r-- | Source/VCGeneration/Context.cs | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs index 7cb9a404..bf27144b 100644 --- a/Source/VCGeneration/Context.cs +++ b/Source/VCGeneration/Context.cs @@ -158,11 +158,6 @@ public abstract class ProverContextContracts:ProverContext{ public override void AddAxiom(Axiom ax, string attributes) {//Contract.Requires(ax != null);
base.AddAxiom(ax, attributes);
- string ignore = ax.FindStringAttribute("ignore");
- if (ignore != null && genOptions.IsAnyProverCommandSupported(ignore)) {
- return;
- }
-
axiomConjuncts.Add(translator.Translate(ax.Expr));
}
|