summaryrefslogtreecommitdiff
path: root/Source/AbsInt
diff options
context:
space:
mode:
Diffstat (limited to 'Source/AbsInt')
-rw-r--r--Source/AbsInt/LoopInvariantsOnDemand.cs2
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/AbsInt/LoopInvariantsOnDemand.cs b/Source/AbsInt/LoopInvariantsOnDemand.cs
index 49958289..5bb5916d 100644
--- a/Source/AbsInt/LoopInvariantsOnDemand.cs
+++ b/Source/AbsInt/LoopInvariantsOnDemand.cs
@@ -55,6 +55,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
return VisitFunApp((AI.IFunApp)expr);
else if (expr is AI.IFunction)
return VisitFunction((AI.IFunction)expr);
+ else if (expr is AI.IUnknown)
+ return null;
else {
Contract.Assert(false);
throw new cce.UnreachableException();