summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/ConditionGeneration.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs4
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 209248ed..90ed5d5c 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -722,12 +722,12 @@ namespace VC {
public readonly List<Counterexample>/*!>!*/ examples = new List<Counterexample>();
public override void OnCounterexample(Counterexample ce, string/*?*/ reason) {
- Contract.Requires(ce != null);
+ //Contract.Requires(ce != null);
examples.Add(ce);
}
public override void OnUnreachableCode(Implementation impl) {
- Contract.Requires(impl != null);
+ //Contract.Requires(impl != null);
System.Console.WriteLine("found unreachable code:");
EmitImpl(impl, false);
// TODO report error about next to last in seq