Merge

1 files changed, 6 insertions, 2 deletions

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index ab2fa74f..526302db 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -485,14 +485,18 @@ namespace Microsoft.Boogie.Houdini {
 

     public bool MatchCandidate(Expr boogieExpr, out Variable candidateConstant) {

       candidateConstant = null;

-      IExpr antecedent;

+      IExpr antecedent, consequent;

       IExpr expr = boogieExpr as IExpr;

-      if (expr != null && ExprUtil.Match(expr, Prop.Implies, out antecedent)) {

+      if (expr != null && ExprUtil.Match(expr, Prop.Implies, out antecedent, out consequent)) {

         IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp;

         if (constantFunApp != null && houdiniConstants.Contains(constantFunApp.IdentifierExpr.Decl)) {

           candidateConstant = constantFunApp.IdentifierExpr.Decl;

           return true;

         }

+

+        var e = consequent as Expr;

+        if (e != null && MatchCandidate(e, out candidateConstant))

+          return true;

       }

       return false;

     }